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(solver): assert true and ¬false

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 21:42:28 -06:00
parent e08bb7b5ac
commit f76f6bb0d9
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/Solver.ml
View file

@ -72,6 +72,12 @@ let create ?size ?(config=Config.empty) ~theories () : t =
} in } in
(* now add the theories *) (* now add the theories *)
Theory_combine.add_theory_l th_combine theories; Theory_combine.add_theory_l th_combine theories;
(* assert [true] and [not false] *)
let tst = tst self in
Sat_solver.assume self.solver [
[Lit.atom @@ Term.true_ tst];
[Lit.atom ~sign:false @@ Term.false_ tst];
] Proof_default;
self self
(** {2 Sat Solver} *) (** {2 Sat Solver} *)