simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: add is_valid_literal filter to add_term_rec

Browse source
This commit is contained in:
Simon Cruanes 2019-10-02 18:15:06 -05:00
parent 7fe6f07c0b
commit 7552808c33
4 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
sidekick-bin.opam
View file

@ -7,7 +7,7 @@ author: ["Simon Cruanes" "Guillaume Bury"]
maintainer: ["simon.cruanes.2007@m4x.org"] maintainer: ["simon.cruanes.2007@m4x.org"]
build: [ build: [
["dune" "build" "@install" "-p" name "-j" jobs] ["dune" "build" "@install" "-p" name "-j" jobs]
["dune" "build" "@doc" "-p" name] {with-doc} ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
# ["dune" "runtest" "-p" name] {with-test} # ["dune" "runtest" "-p" name] {with-test}
] ]
depends: [ depends: [
@ -15,7 +15,7 @@ depends: [
"containers" "containers"
"iter" "iter"
"zarith" "zarith"
"sidekick" "sidekick" { = version }
"menhir" "menhir"
"msat" { >= "0.8" < "0.9" } "msat" { >= "0.8" < "0.9" }
"ocaml" { >= "4.03" } "ocaml" { >= "4.03" }

2
sidekick.opam
View file

@ -7,7 +7,7 @@ author: ["Simon Cruanes" "Guillaume Bury"]
maintainer: ["simon.cruanes.2007@m4x.org"] maintainer: ["simon.cruanes.2007@m4x.org"]
build: [ build: [
["dune" "build" "@install" "-p" name "-j" jobs] ["dune" "build" "@install" "-p" name "-j" jobs]
["dune" "build" "@doc" "-p" name] {with-doc} ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
# ["dune" "runtest" "-p" name] {with-test} # ["dune" "runtest" "-p" name] {with-test}
] ]
depends: [ depends: [

6
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -6,7 +6,12 @@ module IM = Util.Int_map
module type ARG = sig module type ARG = sig
include Sidekick_core.TERM_PROOF include Sidekick_core.TERM_PROOF
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) Sidekick_core.CC_view.t val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) Sidekick_core.CC_view.t
val is_valid_literal : Term.t -> bool
(** Is this a valid boolean literal? (e.g. is it a closed term, not inside
a quantifier) *)
end end
module type S = Sidekick_core.SOLVER module type S = Sidekick_core.SOLVER
@ -458,6 +463,7 @@ module Make(A : ARG)
(fun t -> match A.cc_view t with (fun t -> match A.cc_view t with
| Sidekick_core.CC_view.Not _ -> false (* will process the subterm just later *) | Sidekick_core.CC_view.Not _ -> false (* will process the subterm just later *)
| _ -> true) | _ -> true)
|> Iter.filter (fun t -> A.is_valid_literal t)
|> Iter.iter |> Iter.iter
(fun sub -> (fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" T.pp sub); Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" T.pp sub);

1
src/smtlib/Process.ml
View file

@ -397,6 +397,7 @@ module Solver_arg = struct
include Sidekick_base_term include Sidekick_base_term
let cc_view = Term.cc_view let cc_view = Term.cc_view
let is_valid_literal _ = true
module Proof = struct module Proof = struct
type t = Default type t = Default
let default=Default let default=Default