simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-25 02:46:42 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(core): add push_decision, for model-based th combination

Browse source
This commit is contained in:
Simon Cruanes 2020-11-17 18:23:16 -05:00
parent 60fe3506d5
commit 9839e5a36b
2 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/core/Sidekick_core.ml
View file

@ -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 *)

10
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -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)