diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 74c89bb7..fb60d0bc 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -873,7 +873,7 @@ module Make(Plugin : PLUGIN) clause that constrains it. We could maybe check if they have already has been decided before inserting them into the heap, if it appears that it helps performance. *) - let new_lit st t = + let make_term st t = let l = Lit.make st.st t in if l.l_level < 0 then ( insert_var_order st (E_lit l) @@ -1608,19 +1608,19 @@ module Make(Plugin : PLUGIN) Solver_intf.Assign (term, v) | Lit _ -> assert false - let slice_push st ?(keep=false) (l:formula list) (lemma:lemma): unit = + let acts_add_clause st ?(keep=false) (l:formula list) (lemma:lemma): unit = let atoms = List.rev_map (create_atom st) l in let c = Clause.make atoms (Lemma lemma) in if not keep then Clause.set_learnt c true; Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c); Vec.push st.clauses_to_add c - let slice_raise st (l:formula list) proof : 'a = + let acts_raise st (l:formula list) proof : 'a = let atoms = List.rev_map (create_atom st) l in let c = Clause.make atoms (Lemma proof) in raise_notrace (Th_conflict c) - let slice_propagate (st:t) f = function + let acts_propagate (st:t) f = function | Solver_intf.Eval l -> let a = mk_atom st f in enqueue_semantic st a l @@ -1641,7 +1641,7 @@ module Make(Plugin : PLUGIN) invalid_arg "Msat.Internal.slice_propagate" ) - let[@specialise] slice_iter st ~full head f : unit = + let[@specialise] acts_iter st ~full head f : unit = for i = (if full then 0 else head) to Vec.size st.trail-1 do let e = match Vec.get st.trail i with | Atom a -> @@ -1653,21 +1653,38 @@ module Make(Plugin : PLUGIN) f e done - let[@inline] current_slice st : (_,_,_) Solver_intf.slice = { + let acts_eval_lit st (f:formula) : Solver_intf.lbool = + let a = create_atom st f in + if Atom.is_true a then Solver_intf.L_true + else if Atom.is_false a then Solver_intf.L_false + else Solver_intf.L_undefined + + let[@inline] acts_mk_lit st f : unit = + ignore (create_atom st f : atom) + + let[@inline] acts_mk_term st t : unit = make_term st t + + let[@inline] current_slice st : (_,_,_) Solver_intf.acts = { Solver_intf. - iter_assumptions=slice_iter st ~full:false st.th_head; - push = slice_push st; - propagate = slice_propagate st; - raise_conflict=slice_raise st; + 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_mk_term=acts_mk_term st; + acts_add_clause = acts_add_clause st; + acts_propagate = acts_propagate st; + acts_raise_conflict=acts_raise st; } (* full slice, for [if_sat] final check *) - let[@inline] full_slice st : (_,_,_) Solver_intf.slice = { + let[@inline] full_slice st : (_,_,_) Solver_intf.acts = { Solver_intf. - iter_assumptions=slice_iter st ~full:true st.th_head; - push = slice_push st; - propagate = slice_propagate st; - raise_conflict=slice_raise st; + 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_mk_term=acts_mk_term st; + acts_add_clause = acts_add_clause st; + acts_propagate = acts_propagate st; + acts_raise_conflict=acts_raise st; } (* Assert that the conflict is indeeed a conflict *) diff --git a/src/core/Msat.ml b/src/core/Msat.ml index be7f6ce4..e9d36153 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -11,6 +11,11 @@ module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT module type PROOF = Solver_intf.PROOF +(** Empty type *) +type void = (unit,bool) Solver_intf.gadt_eq + +type lbool = Solver_intf.lbool = L_true | L_false | L_undefined + type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = { eval : 'form -> bool; eval_level : 'form -> bool * int; @@ -36,11 +41,14 @@ type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.re | Eval of 'term list | Consequence of 'formula list * 'proof -type ('term, 'formula, 'proof) slice = ('term, 'formula, 'proof) Solver_intf.slice = { - iter_assumptions: (('term,'formula) assumption -> unit) -> unit; - push : ?keep:bool -> 'formula list -> 'proof -> unit; - raise_conflict: 'b. 'formula list -> 'proof -> 'b; - propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; +type ('term, 'formula, 'proof) acts = ('term, 'formula, 'proof) Solver_intf.acts = { + acts_iter_assumptions: (('term,'formula) assumption -> unit) -> unit; + acts_eval_lit: 'formula -> lbool; + acts_mk_lit: 'formula -> unit; + acts_mk_term: 'term -> unit; + acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit; + acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; + acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; } type negated = Solver_intf.negated = Negated | Same_sign diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index fdb7675a..816636e0 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -82,24 +82,38 @@ type ('term, 'formula, 'proof) reason = *) (** The type of reasons for propagations of a formula [f]. *) +type lbool = L_true | L_false | L_undefined +(** Valuation of an atom *) + (* TODO: find a way to use atoms instead of formulas here *) -type ('term, 'formula, 'proof) slice = { - iter_assumptions: (('term,'formula) assumption -> unit) -> unit; +type ('term, 'formula, 'proof) acts = { + acts_iter_assumptions: (('term,'formula) assumption -> unit) -> unit; (** Traverse the new assumptions on the boolean trail. *) - push: ?keep:bool -> 'formula list -> 'proof -> unit; + acts_eval_lit: 'formula -> lbool; + (** Obtain current value of the given literal *) + + acts_mk_lit: 'formula -> unit; + (** Map the given formula to a literal, which will be decided by the + SAT solver. *) + + acts_mk_term: 'term -> unit; + (** Map the given term (and its subterms) to decision variables, + for the MCSAT solver to decide. *) + + acts_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. *) - raise_conflict: 'b. 'formula list -> 'proof -> 'b; + acts_raise_conflict: 'b. '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. *) - propagate: 'formula -> ('term, 'formula, 'proof) reason -> unit; + acts_propagate: 'formula -> ('term, '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} *) } @@ -174,12 +188,12 @@ module type PLUGIN_CDCL_T = sig val pop_levels : t -> int -> unit (** Pop [n] levels of the theory *) - val partial_check : t -> (void, Formula.t, proof) slice -> unit + val partial_check : t -> (void, Formula.t, proof) acts -> unit (** Assume the formulas in the slice, possibly using the [slice] to push new formulas to be propagated or to raising a conflict or to add new lemmas. *) - val final_check : t -> (void, Formula.t, proof) slice -> unit + val final_check : t -> (void, Formula.t, proof) acts -> unit (** Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; @@ -200,12 +214,12 @@ module type PLUGIN_MCSAT = sig val pop_levels : t -> int -> unit (** Pop [n] levels of the theory *) - val partial_check : t -> (Term.t, Formula.t, proof) slice -> unit + val partial_check : t -> (Term.t, Formula.t, proof) acts -> unit (** Assume the formulas in the slice, possibly using the [slice] to push new formulas to be propagated or to raising a conflict or to add new lemmas. *) - val final_check : t -> (Term.t, Formula.t, proof) slice -> unit + val final_check : t -> (Term.t, Formula.t, proof) acts -> unit (** Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; @@ -418,8 +432,8 @@ module type S = sig The assumptions are just used for this call to [solve], they are not saved in the solver's state. *) - val new_lit : t -> term -> unit - (** Add a new litteral (i.e term) to the solver. This term will + val make_term : t -> term -> unit + (** Add a new term (i.e. decision variable) to the solver. This term will be decided on at some point during solving, wether it appears in clauses or not. *) diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml index d69026eb..22b66a69 100644 --- a/src/sudoku/sudoku_solve.ml +++ b/src/sudoku/sudoku_solve.ml @@ -177,7 +177,7 @@ end = struct (fun c -> F.make true x y (Cell.make (c+1))) in Log.debugf 4 (fun k->k "(@[add-clause@ %a@])" pp_c_ c); - acts.push ~keep:true c (); + acts.acts_add_clause ~keep:true c (); )) (* check constraints *) @@ -198,7 +198,7 @@ end = struct assert (x1<>x2 || y1<>y2); let c = [F.make false x1 y1 c1; F.make false x2 y2 c2] in logs_conflict ("all-diff." ^ kind) c; - acts.raise_conflict c () + acts.acts_raise_conflict c () )) in all_diff "rows" Grid.rows; @@ -206,8 +206,8 @@ end = struct all_diff "squares" Grid.squares; () - let trail_ acts = - acts.iter_assumptions + let trail_ (acts:(Msat.void,_,_) Msat.acts) = + acts.acts_iter_assumptions |> Sequence.map (function | Assign _ -> assert false @@ -228,7 +228,7 @@ end = struct (* conflict: at most one value *) let c = [F.make false x y c; F.make false x y c'] in logs_conflict "at-most-one" c; - acts.raise_conflict c () + acts.acts_raise_conflict c () ) )