simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-26 11:24:50 -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 238226500a
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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