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

refactor(sat): use first-class modules instead of records

Browse source
This commit is contained in:
Simon Cruanes 2021-07-18 19:18:42 -04:00
parent 041e83139d
commit 15d86d7c62
4 changed files with 124 additions and 124 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -88,11 +88,13 @@ module Make(A : ARG)
module P = P
module Lit = Lit
type t = msat_acts
let[@inline] raise_conflict a lits pr =
a.Sidekick_sat.acts_raise_conflict lits pr
let[@inline] propagate a lit ~reason =
let[@inline] raise_conflict (a:t) lits pr =
let (module A) = a in
A.raise_conflict lits pr
let[@inline] propagate (a:t) lit ~reason =
let (module A) = a in
let reason = Sidekick_sat.Consequence reason in
a.Sidekick_sat.acts_propagate lit reason
A.propagate lit reason
end
end
@ -241,23 +243,27 @@ module Make(A : ARG)
let on_model_gen self f = self.mk_model <- f :: self.mk_model
let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
let (module A) = acts in
let sign = Lit.sign lit in
acts.Sidekick_sat.acts_add_decision_lit (Lit.abs lit) sign
A.add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self acts c proof : 'a =
let[@inline] raise_conflict self (acts:actions) c proof : 'a =
let (module A) = acts in
Stat.incr self.count_conflict;
acts.Sidekick_sat.acts_raise_conflict c proof
A.raise_conflict c proof
let[@inline] propagate self acts p ~reason : unit =
let[@inline] propagate self (acts:actions) p ~reason : unit =
let (module A) = acts in
Stat.incr self.count_propagate;
acts.Sidekick_sat.acts_propagate p (Sidekick_sat.Consequence reason)
A.propagate p (Sidekick_sat.Consequence reason)
let[@inline] propagate_l self acts p cs proof : unit =
propagate self acts p ~reason:(fun()->cs,proof)
let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit =
let add_sat_clause_ self (acts:actions) ~keep lits (proof:P.t) : unit =
let (module A) = acts in
Stat.incr self.count_axiom;
acts.Sidekick_sat.acts_add_clause ~keep lits proof
A.add_clause ~keep lits proof
let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
@ -375,7 +381,9 @@ module Make(A : ARG)
let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit =
add_sat_clause_ self acts ~keep:true lits proof
let add_lit _self acts lit : unit = acts.Sidekick_sat.acts_mk_lit lit
let[@inline] add_lit _self (acts:actions) lit : unit =
let (module A) = acts in
A.mk_lit lit
let add_lit_t self acts ?sign t =
let lit = mk_lit self acts ?sign t in
@ -454,8 +462,10 @@ module Make(A : ARG)
);
()
let[@inline] iter_atoms_ acts : _ Iter.t =
fun f -> acts.Sidekick_sat.acts_iter_assumptions f
let[@inline] iter_atoms_ (acts:actions) : _ Iter.t =
fun f ->
let (module A) = acts in
A.iter_assumptions f
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) =
@ -906,22 +916,22 @@ module Make(A : ARG)
let r = Sat_solver.solve ~assumptions (solver self) in
Stat.incr self.count_solve;
match r with
| Sat_solver.Sat st ->
| Sat_solver.Sat (module SAT) ->
Log.debug 1 "sidekick.msat-solver: SAT";
let _lits f = st.iter_trail f in
let _lits f = SAT.iter_trail f in
(* TODO: theory combination *)
let m = mk_model self _lits in
do_on_exit ();
Sat m
| Sat_solver.Unsat us ->
| Sat_solver.Unsat (module UNSAT) ->
let proof = lazy (
try
let pr = us.get_proof () in
let pr = UNSAT.get_proof () in
if check then Sat_solver.Proof.check pr;
Some (Pre_proof.make pr (List.rev self.si.t_defs))
with Sidekick_sat.Solver_intf.No_proof -> None
) in
let unsat_core = lazy (us.Sidekick_sat.unsat_assumptions ()) in
let unsat_core = lazy (UNSAT.unsat_assumptions ()) in
do_on_exit ();
Unsat {proof; unsat_core}

30
src/sat/Sidekick_sat.ml
View file

@ -10,34 +10,14 @@ module type PROOF = Solver_intf.PROOF
type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
type 'form sat_state = 'form Solver_intf.sat_state = {
eval : 'form -> bool;
eval_level : 'form -> bool * int;
iter_trail : ('form -> unit) -> unit;
}
type ('atom,'clause, 'proof) unsat_state = ('atom,'clause, 'proof) Solver_intf.unsat_state = {
unsat_conflict : unit -> 'clause;
get_proof : unit -> 'proof;
unsat_assumptions: unit -> 'atom list;
}
type 'clause export = 'clause Solver_intf.export = {
hyps : 'clause Vec.t;
history : 'clause Vec.t;
}
module type SAT_STATE = Solver_intf.SAT_STATE
type 'form sat_state = 'form Solver_intf.sat_state
type ('formula, 'proof) reason = ('formula, 'proof) Solver_intf.reason =
| Consequence of (unit -> 'formula list * 'proof)
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts = {
acts_iter_assumptions: ('formula -> unit) -> unit;
acts_eval_lit: 'formula -> lbool;
acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;
acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b;
acts_propagate : 'formula -> ('formula, 'proof) reason -> unit;
acts_add_decision_lit: 'formula -> bool -> unit;
}
module type ACTS = Solver_intf.ACTS
type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts
type negated = Solver_intf.negated = Negated | Same_sign

76
src/sat/Solver.ml
View file

@ -1519,28 +1519,34 @@ module Make(Plugin : PLUGIN)
let[@inline] acts_mk_lit st ?default_pol f : unit =
ignore (mk_atom ?default_pol st f : atom)
let[@inline] current_slice st : _ Solver_intf.acts = {
Solver_intf.
acts_iter_assumptions=acts_iter st ~full:false st.th_head;
acts_eval_lit= acts_eval_lit st;
acts_mk_lit=acts_mk_lit st;
acts_add_clause = acts_add_clause st;
acts_propagate = acts_propagate st;
acts_raise_conflict=acts_raise st;
acts_add_decision_lit=acts_add_decision_lit st;
}
let[@inline] current_slice st : _ Solver_intf.acts =
let module M = struct
type nonrec proof = lemma
type nonrec formula = formula
let iter_assumptions=acts_iter st ~full:false st.th_head
let eval_lit= acts_eval_lit st
let mk_lit=acts_mk_lit st
let add_clause = acts_add_clause st
let propagate = acts_propagate st
let raise_conflict c pr=acts_raise st c pr
let add_decision_lit=acts_add_decision_lit st
end in
(module M)
(* full slice, for [if_sat] final check *)
let[@inline] full_slice st : _ Solver_intf.acts = {
Solver_intf.
acts_iter_assumptions=acts_iter st ~full:true st.th_head;
acts_eval_lit= acts_eval_lit st;
acts_mk_lit=acts_mk_lit st;
acts_add_clause = acts_add_clause st;
acts_propagate = acts_propagate st;
acts_raise_conflict=acts_raise st;
acts_add_decision_lit=acts_add_decision_lit st;
}
let[@inline] full_slice st : _ Solver_intf.acts =
let module M = struct
type nonrec proof = lemma
type nonrec formula = formula
let iter_assumptions=acts_iter st ~full:true st.th_head
let eval_lit= acts_eval_lit st
let mk_lit=acts_mk_lit st
let add_clause = acts_add_clause st
let propagate = acts_propagate st
let raise_conflict c pr=acts_raise st c pr
let add_decision_lit=acts_add_decision_lit st
end in
(module M)
(* Assert that the conflict is indeeed a conflict *)
let check_is_conflict_ (c:Clause.t) : unit =
@ -1826,14 +1832,13 @@ module Make(Plugin : PLUGIN)
let mk_sat (st:t) : Formula.t Solver_intf.sat_state =
pp_all st 99 "SAT";
let t = trail st in
let iter_trail f =
Vec.iter (fun a -> f (Atom.formula a)) t
in
let[@inline] eval f = eval st (mk_atom st f) in
let[@inline] eval_level f = eval_level st (mk_atom st f) in
{ Solver_intf.
eval; eval_level; iter_trail;
}
let module M = struct
type formula = Formula.t
let iter_trail f = Vec.iter (fun a -> f (Atom.formula a)) t
let[@inline] eval f = eval st (mk_atom st f)
let[@inline] eval_level f = eval_level st (mk_atom st f)
end in
(module M)
let mk_unsat (st:t) (us: unsat_cause) : _ Solver_intf.unsat_state =
pp_all st 99 "UNSAT";
@ -1866,7 +1871,15 @@ module Make(Plugin : PLUGIN)
let c = unsat_conflict () in
Proof.prove c
in
{ Solver_intf.unsat_conflict; get_proof; unsat_assumptions; }
let module M = struct
type nonrec atom = atom
type clause = Clause.t
type proof = Proof.t
let get_proof = get_proof
let unsat_conflict = unsat_conflict
let unsat_assumptions = unsat_assumptions
end in
(module M)
let add_clause_a st c lemma : unit =
try
@ -1901,11 +1914,6 @@ module Make(Plugin : PLUGIN)
with UndecidedLit -> false
let[@inline] eval_atom _st a : Solver_intf.lbool = eval_atom_ a
let export (st:t) : clause Solver_intf.export =
let hyps = hyps st in
let history = history st in
{Solver_intf.hyps; history; }
end
[@@inline][@@specialise]

94
src/sat/Solver_intf.ml
View file

@ -13,38 +13,49 @@ Copyright 2016 Simon Cruanes
type 'a printer = Format.formatter -> 'a -> unit
type 'form sat_state = {
eval: 'form -> bool;
module type SAT_STATE = sig
type formula
val eval : formula -> bool
(** Returns the valuation of a formula in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
eval_level: 'form -> bool * int;
val eval_level : formula -> bool * int
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
iter_trail : ('form -> unit) -> unit;
val iter_trail : (formula -> unit) -> unit
(** Iter through the formulas in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
}
end
type 'form sat_state = (module SAT_STATE with type formula = 'form)
(** The type of values returned when the solver reaches a SAT state. *)
type ('atom, 'clause, 'proof) unsat_state = {
unsat_conflict : unit -> 'clause;
(** Returns the unsat clause found at the toplevel *)
get_proof : unit -> 'proof;
(** returns a persistent proof of the empty clause from the Unsat result. *)
unsat_assumptions: unit -> 'atom list;
(** Subset of assumptions responsible for "unsat" *)
}
(** The type of values returned when the solver reaches an UNSAT state. *)
module type UNSAT_STATE = sig
type atom
type clause
type proof
type 'clause export = {
hyps: 'clause Vec.t;
history: 'clause Vec.t;
}
(** Export internal state *)
val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *)
val get_proof : unit -> proof
(** returns a persistent proof of the empty clause from the Unsat result. *)
val unsat_assumptions: unit -> atom list
(** Subset of assumptions responsible for "unsat" *)
end
type ('atom, 'clause, 'proof) unsat_state =
(module UNSAT_STATE with type atom = 'atom
and type clause = 'clause
and type proof = 'proof)
(** The type of values returned when the solver reaches an UNSAT state. *)
type negated =
| Negated (** changed sign *)
@ -52,22 +63,8 @@ type negated =
(** This type is used during the normalisation of formulas.
See {!val:Expr_intf.S.norm} for more details. *)
type 'term eval_res =
| Unknown (** The given formula does not have an evaluation *)
| Valued of bool * ('term list) (** The given formula can be evaluated to the given bool.
The list of terms to give is the list of terms that
were effectively used for the evaluation. *)
(** The type of evaluation results for a given formula.
For instance, let's suppose we want to evaluate the formula [x * y = 0], the
following result are correct:
- [Unknown] if neither [x] nor [y] are assigned to a value
- [Valued (true, [x])] if [x] is assigned to [0]
- [Valued (true, [y])] if [y] is assigned to [0]
- [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
*)
type ('formula, 'proof) reason =
| Consequence of (unit -> 'formula list * 'proof)
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
(** [Consequence (l, p)] means that the formulas in [l] imply the propagated
formula [f]. The proof should be a proof of the clause "[l] implies [f]".
@ -91,39 +88,46 @@ type ('formula, 'proof) reason =
type lbool = L_true | L_false | L_undefined
(** Valuation of an atom *)
(* TODO: find a way to use atoms instead of formulas here *)
type ('formula, 'proof) acts = {
acts_iter_assumptions: ('formula -> unit) -> unit;
module type ACTS = sig
type formula
type proof
val iter_assumptions: (formula -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
acts_eval_lit: 'formula -> lbool;
val eval_lit: formula -> lbool
(** Obtain current value of the given literal *)
acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
val mk_lit: ?default_pol:bool -> formula -> unit
(** Map the given formula to a literal, which will be decided by the
SAT solver. *)
acts_add_clause: ?keep:bool -> 'formula list -> 'proof -> unit;
val add_clause: ?keep:bool -> formula list -> proof -> unit
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
*)
acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b;
val raise_conflict: formula list -> proof -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
acts_propagate: 'formula -> ('formula, 'proof) reason -> unit;
val propagate: formula -> (formula, proof) reason -> unit
(** Propagate a formula, i.e. the theory can evaluate the formula to be true
(see the definition of {!type:eval_res} *)
acts_add_decision_lit: 'formula -> bool -> unit;
val add_decision_lit: formula -> bool -> unit
(** Ask the SAT solver to decide on the given formula with given sign
before it can answer [SAT]. The order of decisions is still unspecified.
Useful for theory combination. This will be undone on backtracking. *)
}
end
(* TODO: find a way to use atoms instead of formulas here *)
type ('formula, 'proof) acts =
(module ACTS with type formula = 'formula
and type proof = 'proof)
(** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof
@ -418,7 +422,5 @@ module type S = sig
val eval_atom : t -> atom -> lbool
(** Evaluate atom in current state *)
val export : t -> clause export
end