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

try to fix boolean terms not decided by SAT solver

Browse source
This commit is contained in:
Simon Cruanes 2021-08-21 14:00:31 -04:00
parent 075e251aed
commit 0668f28ac7
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -599,13 +599,14 @@ module Make(A : ARG)
(* preprocess literals, making them ready for being added to the solver *) (* preprocess literals, making them ready for being added to the solver *)
let rec preprocess_lit_ self lit : Lit.t * dproof = let rec preprocess_lit_ self lit : Lit.t * dproof =
Solver_internal.preprocess_lit_ let lit, proof =
Solver_internal.preprocess_lit_
~add_clause:(fun lits proof -> ~add_clause:(fun lits proof ->
(* recursively add these sub-literals, so they're also properly processed *) (* recursively add these sub-literals, so they're also properly processed *)
Stat.incr self.si.count_preprocess_clause; Stat.incr self.si.count_preprocess_clause;
let pr_l = ref [] in let pr_l = ref [] in
let lits = let lits =
List.map CCList.map
(fun lit -> (fun lit ->
let a, pr = preprocess_lit_ self lit in let a, pr = preprocess_lit_ self lit in
(* FIXME if not (P.is_trivial_refl pr) then ( *) (* FIXME if not (P.is_trivial_refl pr) then ( *)
@ -617,6 +618,9 @@ module Make(A : ARG)
let emit_proof p = List.iter (fun dp -> dp p) !pr_l; in let emit_proof p = List.iter (fun dp -> dp p) !pr_l; in
Sat_solver.add_clause self.solver lits emit_proof) Sat_solver.add_clause self.solver lits emit_proof)
self.si lit self.si lit
in
Sat_solver.add_lit self.solver lit;
lit, proof
(* FIXME: should we just add the proof instead? *) (* FIXME: should we just add the proof instead? *)
let[@inline] preprocess_lit' self lit : Lit.t = let[@inline] preprocess_lit' self lit : Lit.t =
@ -627,6 +631,7 @@ module Make(A : ARG)
let rec mk_lit_t (self:t) ?sign (t:term) : lit * dproof = let rec mk_lit_t (self:t) ?sign (t:term) : lit * dproof =
let lit = Lit.atom ?sign self.si.tst t in let lit = Lit.atom ?sign self.si.tst t in
let lit, proof = preprocess_lit_ self lit in let lit, proof = preprocess_lit_ self lit in
Sat_solver.add_lit self.solver lit;
add_bool_subterms_ self (Lit.term lit); add_bool_subterms_ self (Lit.term lit);
lit, proof lit, proof