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

fix(smt): improve theory combination a bit

Browse source
This commit is contained in:
Simon Cruanes 2022-02-04 16:40:55 -05:00
parent ab74b1a792
commit d11b9d585c
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/lra/sidekick_arith_lra.ml
View file

@ -363,7 +363,6 @@ module Make(A : ARG) : S with module A = A = struct
end end
| LRA_op _ | LRA_mult _ -> | LRA_op _ | LRA_mult _ ->
let steps = ref [] in
let le = as_linexp t in let le = as_linexp t in
(* [t] is [le_comb + le_const], where [le_comb] is a linear expression (* [t] is [le_comb + le_const], where [le_comb] is a linear expression

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

@ -304,6 +304,7 @@ module Make(A : ARG)
let[@inline] ty_st t = t.ty_st let[@inline] ty_st t = t.ty_st
let[@inline] proof self = self.proof let[@inline] proof self = self.proof
let stats t = t.stat let stats t = t.stat
let[@inline] has_delayed_actions self = not (Queue.is_empty self.delayed_actions)
let registry self = self.registry let registry self = self.registry
let simplifier self = self.simp let simplifier self = self.simp
@ -543,8 +544,6 @@ module Make(A : ARG)
CC.pop_levels (cc self) n; CC.pop_levels (cc self) n;
pop_lvls_ n self.th_states pop_lvls_ n self.th_states
exception E_loop_exit
(* handle a literal assumed by the SAT solver *) (* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (acts:theory_actions) (lits:Lit.t Iter.t) : unit = let assert_lits_ ~final (self:t) (acts:theory_actions) (lits:Lit.t Iter.t) : unit =
Log.debugf 2 Log.debugf 2
@ -558,19 +557,23 @@ module Make(A : ARG)
(* transmit to theories. *) (* transmit to theories. *)
CC.check cc acts; CC.check cc acts;
if final then ( if final then (
try let continue = ref true in
while true do while !continue do
let fcheck = ref true in
while !fcheck do
(* TODO: theory combination *) (* TODO: theory combination *)
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
Perform_delayed_th.top self acts; if has_delayed_actions self then (
CC.check cc acts; Perform_delayed_th.top self acts;
Perform_delayed_th.top self acts; ) else (
if not @@ CC.new_merges cc then ( fcheck := false
raise_notrace E_loop_exit )
);
done; done;
with E_loop_exit -> CC.check cc acts;
() if not (CC.new_merges cc) && not (has_delayed_actions self) then (
continue := false;
);
done;
) else ( ) else (
List.iter (fun f -> f self acts lits) self.on_partial_check; List.iter (fun f -> f self acts lits) self.on_partial_check;
Perform_delayed_th.top self acts; Perform_delayed_th.top self acts;