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

fix: ensure all functions in SMT solver preprocess their literals

Browse source
This commit is contained in:
Simon Cruanes 2021-12-16 13:49:43 -05:00
parent 4ac2eb25a6
commit 3ab1ddfea8
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -710,6 +710,17 @@ module Make(A : ARG)
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.preprocess_lit_ ~steps self.si pacts lit
(* preprocess clause, return new proof *)
let preprocess_clause_ (self:t)
(c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step =
let steps = ref [] in
let c = IArray.map (preprocess_lit_ self ~steps) c in
let pr =
P.lemma_rw_clause pr
~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof
in
c, pr
(* make a literal from a term, ensuring it is properly preprocessed *)
let mk_lit_t (self:t) ?sign (t:term) : lit =
let pacts = preprocess_acts_of_solver_ self in
@ -768,7 +779,8 @@ module Make(A : ARG)
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
(* add [c], without preprocessing its literals *)
let add_clause_nopreproc_ (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
Stat.incr self.count_clause;
Log.debugf 50 (fun k->
k "(@[solver.add-clause@ %a@])"
@ -777,6 +789,12 @@ module Make(A : ARG)
Sat_solver.add_clause_a self.solver (c:> lit array) proof;
Profile.exit pb
let add_clause_nopreproc_l_ self c p = add_clause_nopreproc_ self (IArray.of_list c) p
let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
let c, proof = preprocess_clause_ self c proof in
add_clause_nopreproc_ self c proof
let add_clause_l self c p = add_clause self (IArray.of_list c) p
let assert_terms self c =