feat: rename slice to acts, add some functions in it

- add literal
- add term
- eval literal

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;
+    acts_iter_assumptions=acts_iter st ~full:false st.th_head;
-    push = slice_push st;
+    acts_eval_lit= acts_eval_lit st;
-    propagate = slice_propagate st;
+    acts_mk_lit=acts_mk_lit st;
-    raise_conflict=slice_raise 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;
+    acts_iter_assumptions=acts_iter st ~full:true st.th_head;
-    push = slice_push st;
+    acts_eval_lit= acts_eval_lit st;
-    propagate = slice_propagate st;
+    acts_mk_lit=acts_mk_lit st;
-    raise_conflict=slice_raise 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 *)

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 = {
+type ('term, 'formula, 'proof) acts = ('term, 'formula, 'proof) Solver_intf.acts = {
-  iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
+  acts_iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
-  push : ?keep:bool -> 'formula list -> 'proof -> unit;
+  acts_eval_lit: 'formula -> lbool;
-  raise_conflict: 'b. 'formula list -> 'proof -> 'b;
+  acts_mk_lit: 'formula -> unit;
-  propagate : 'formula -> ('term, 'formula, 'proof) reason -> 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

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 = {
+type ('term, 'formula, 'proof) acts = {
-  iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
+  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
+  val make_term : t -> term -> unit
-  (** Add a new litteral (i.e term) to the solver. This term will
+  (** 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. *)
 

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 = 
+    let trail_ (acts:(Msat.void,_,_) Msat.acts) = 
-      acts.iter_assumptions
+      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 ()
             )
         )