From 9839e5a36bc0327ce30856df436758b526869942 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 17 Nov 2020 18:23:16 -0500 Subject: [PATCH] feat(core): add `push_decision`, for model-based th combination --- src/core/Sidekick_core.ml | 6 ++++++ src/msat-solver/Sidekick_msat_solver.ml | 10 +++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index d0953a42..7ef211bd 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -401,6 +401,12 @@ module type SOLVER_INTERNAL = sig val raise_conflict : t -> actions -> lit list -> proof -> 'a (** Give a conflict clause to the solver *) + val push_decision : t -> actions -> lit -> unit + (** Ask the SAT solver to decide the given literal in an extension of the + current trail. This is useful for theory combination. + If the SAT solver backtracks, this (potential) decision is removed + and forgotten. *) + val propagate: t -> actions -> lit -> (unit -> lit list) -> unit (** Propagate a boolean using a unit clause. [expl => lit] must be a theory lemma, that is, a T-tautology *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index b5036682..3330099d 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -202,6 +202,10 @@ module Make(A : ARG) let add_preprocess self f = self.preprocess <- f :: self.preprocess + let push_decision (_self:t) (acts:actions) (lit:lit) : unit = + let sign = Lit.sign lit in + acts.Msat.acts_add_decision_lit (Lit.abs lit) sign + let[@inline] raise_conflict self acts c : 'a = Stat.incr self.count_conflict; acts.Msat.acts_raise_conflict c P.default @@ -279,6 +283,10 @@ module Make(A : ARG) let cc_add_term self t = CC.add_term (cc self) t let cc_find self n = CC.find (cc self) n + let cc_are_equal self t1 t2 = + let n1 = cc_add_term self t1 in + let n2 = cc_add_term self t2 in + N.equal (cc_find self n1) (cc_find self n2) let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e let cc_merge_t self acts t1 t2 e = cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e @@ -578,7 +586,7 @@ module Make(A : ARG) let add_clause (self:t) (c:Atom.t IArray.t) : unit = Stat.incr self.count_clause; - Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c); + Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c); Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default let add_clause_l self c = add_clause self (IArray.of_list c)