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

port fix for bug introduced in 1946a5e7

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 23:25:44 -04:00
parent 6a4947a25c
commit 663f291bd5
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 39 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

67
src/smt/solver_internal.ml
View file

@ -79,6 +79,9 @@ let simplify_t self (t : Term.t) : _ option = Simplify.normalize self.simp t
let simp_t self (t : Term.t) : Term.t * _ = Simplify.normalize_t self.simp t let simp_t self (t : Term.t) : Term.t * _ = Simplify.normalize_t self.simp t
let add_simplifier (self : t) f : unit = Simplify.add_hook self.simp f let add_simplifier (self : t) f : unit = Simplify.add_hook self.simp f
let[@inline] has_delayed_actions self =
not (Queue.is_empty self.delayed_actions)
let on_th_combination self f = let on_th_combination self f =
self.on_th_combination <- f :: self.on_th_combination self.on_th_combination <- f :: self.on_th_combination
@ -490,37 +493,45 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
check_cc_with_acts_ self acts; check_cc_with_acts_ self acts;
(match check_th_combination_ self acts lits with let new_work = has_delayed_actions self in
| Ok m -> self.last_model <- Some m
| Error { lits; semantic } ->
(* bad model, we add a clause to remove it *)
Log.debugf 5 (fun k ->
k "(@[solver.th-comb.conflict@ :lits (@[%a@])@ :same-val (@[%a@])@])"
(Util.pp_list Lit.pp) lits
(Util.pp_list @@ Fmt.Dump.(triple bool Term.pp_debug Term.pp_debug))
semantic);
let c1 = List.rev_map Lit.neg lits in (* do actual theory combination if nothing changed by pure "final check" *)
let c2 = if not new_work then (
semantic match check_th_combination_ self acts lits with
|> List.rev_map (fun (sign, t, u) -> | Ok m -> self.last_model <- Some m
let eqn = Term.eq self.tst t u in | Error { lits; semantic } ->
let lit = Lit.atom ~sign:(not sign) eqn in (* bad model, we add a clause to remove it *)
(* make sure to consider the new lit *) Log.debugf 5 (fun k ->
add_lit self acts lit; k
lit) "(@[solver.th-comb.conflict@ :lits (@[%a@])@ :same-val \
in (@[%a@])@])"
(Util.pp_list Lit.pp) lits
(Util.pp_list
@@ Fmt.Dump.(triple bool Term.pp_debug Term.pp_debug))
semantic);
let c = List.rev_append c1 c2 in let c1 = List.rev_map Lit.neg lits in
let pr = let c2 =
Proof_trace.add_step self.proof @@ fun () -> Proof_core.lemma_cc c semantic
in |> List.rev_map (fun (sign, t, u) ->
let eqn = Term.eq self.tst t u in
let lit = Lit.atom ~sign:(not sign) eqn in
(* make sure to consider the new lit *)
add_lit self acts lit;
lit)
in
Log.debugf 20 (fun k -> let c = List.rev_append c1 c2 in
k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])" let pr =
(Util.pp_list Lit.pp) c); Proof_trace.add_step self.proof @@ fun () -> Proof_core.lemma_cc c
(* will add a delayed action *) in
add_clause_temp self acts c pr);
Log.debugf 20 (fun k ->
k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])"
(Util.pp_list Lit.pp) c);
(* will add a delayed action *)
add_clause_temp self acts c pr
);
Perform_delayed_th.top self acts Perform_delayed_th.top self acts
) else ( ) else (