From 15d86d7c62c78a3c2af040816bb100b8021ef619 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 18 Jul 2021 19:18:42 -0400 Subject: [PATCH] refactor(sat): use first-class modules instead of records --- src/msat-solver/Sidekick_msat_solver.ml | 48 ++++++++----- src/sat/Sidekick_sat.ml | 30 ++------ src/sat/Solver.ml | 76 +++++++++++--------- src/sat/Solver_intf.ml | 94 +++++++++++++------------ 4 files changed, 124 insertions(+), 124 deletions(-) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index aa35c35a..03963f12 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -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} diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index 9ffa03ad..873fb9b7 100644 --- a/src/sat/Sidekick_sat.ml +++ b/src/sat/Sidekick_sat.ml @@ -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 diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 07609129..c341673b 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -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] diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 69a2b911..afe2dfc6 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -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