feat: add Value.t to the mcsat interface

it can be useful to separate terms from pure values.

src/core/Internal.ml

@@ -15,11 +15,13 @@ module Make(Plugin : PLUGIN)
 = struct
   module Term = Plugin.Term
   module Formula = Plugin.Formula
+  module Value = Plugin.Value
 
   type term = Term.t
   type formula = Formula.t
   type theory = Plugin.t
   type lemma = Plugin.proof
+  type value = Value.t
 
   (* MCSAT literal *)
   type lit = {
@@ -28,7 +30,7 @@ module Make(Plugin : PLUGIN)
     mutable l_level : int;
     mutable l_idx: int;
     mutable l_weight : float;
-    mutable assigned : term option;
+    mutable assigned : value option;
   }
 
   type var = {
@@ -144,7 +146,7 @@ module Make(Plugin : PLUGIN)
       | None ->
         Format.fprintf fmt ""
       | Some t ->
-        Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level Term.pp t
+        Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level Value.pp t
 
     let pp out v = Term.pp out v.term
     let debug out v =
@@ -1197,7 +1199,7 @@ module Make(Plugin : PLUGIN)
     )
 
   (* MCsat semantic assignment *)
-  let enqueue_assign st l value lvl =
+  let enqueue_assign st (l:lit) (value:value) lvl =
     match l.assigned with
     | Some _ ->
       Log.debugf error
@@ -1664,7 +1666,7 @@ module Make(Plugin : PLUGIN)
 
   let[@inline] acts_mk_term st t : unit = make_term st t
 
-  let[@inline] current_slice st : (_,_,_) Solver_intf.acts = {
+  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;
@@ -1676,7 +1678,7 @@ module Make(Plugin : PLUGIN)
   }
 
   (* full slice, for [if_sat] final check *)
-  let[@inline] full_slice st : (_,_,_) Solver_intf.acts = {
+  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;
@@ -1905,7 +1907,7 @@ module Make(Plugin : PLUGIN)
 
   let[@inline] unsat_conflict st = st.unsat_at_0
 
-  let model (st:t) : (term * term) list =
+  let model (st:t) : (term * value) list =
     let opt = function Some a -> a | None -> assert false in
     Vec.fold
       (fun acc e -> match e with
@@ -2000,7 +2002,7 @@ module Make(Plugin : PLUGIN)
 
   (* Result type *)
   type res =
-    | Sat of (term,atom) Solver_intf.sat_state
+    | Sat of (term,atom,value) Solver_intf.sat_state
     | Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state
 
   let pp_all st lvl status =
@@ -2014,7 +2016,7 @@ module Make(Plugin : PLUGIN)
           (Vec.pp ~sep:"" Clause.debug) (history st)
       )
 
-  let mk_sat (st:t) : (_,_) Solver_intf.sat_state =
+  let mk_sat (st:t) : _ Solver_intf.sat_state =
     pp_all st 99 "SAT";
     let t = trail st in
     let iter f f' =
@@ -2094,15 +2096,18 @@ module Make(Plugin : PLUGIN)
 end
 [@@inline][@@specialise]
 
-module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) =
+  module Void_ = struct
-  Make(struct
-    include Plugin
-    module Term = struct
     type t = Solver_intf.void
     let equal _ _ = assert false
     let hash _ =  assert false
     let pp _ _ = assert false
   end
+
+module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) =
+  Make(struct
+    include Plugin
+    module Term = Void_
+    module Value = Void_
     let eval _ _ = Solver_intf.Unknown
     let assign _ t = t
     let mcsat = false
@@ -2120,12 +2125,8 @@ module Make_mcsat(Plugin : Solver_intf.PLUGIN_MCSAT) =
 module Make_pure_sat(F: Solver_intf.FORMULA) =
   Make(struct
   module Formula = F
-  module Term = struct
+  module Term = Void_
-    type t = Solver_intf.void
+  module Value = Void_
-    let equal _ _ = true
-    let hash _ = 1
-    let pp out _ = Format.pp_print_string out "()"
-  end
   type t = unit
   type proof = Solver_intf.void
   let push_level () = ()

src/core/Msat.ml

@@ -16,11 +16,11 @@ 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 = {
+type ('term, 'form, 'value) sat_state = ('term, 'form, 'value) Solver_intf.sat_state = {
   eval : 'form -> bool;
   eval_level : 'form -> bool * int;
   iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
-  model : unit -> ('term * 'term) list;
+  model : unit -> ('term * 'value) list;
 }
 
 type ('atom,'clause, 'proof) unsat_state = ('atom,'clause, 'proof) Solver_intf.unsat_state = {
@@ -33,16 +33,16 @@ type 'clause export = 'clause Solver_intf.export = {
   history : 'clause Vec.t;
 }
 
-type ('term, 'formula) assumption = ('term, 'formula) Solver_intf.assumption =
+type ('term, 'formula, 'value) assumption = ('term, 'formula, 'value) Solver_intf.assumption =
-  | Lit of 'formula
+  | Lit of 'formula  (** The given formula is asserted true by the solver *)
-  | Assign of 'term * 'term (** The first term is assigned to the second *)
+  | Assign of 'term * 'value (** The term is assigned to the value *)
 
 type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason =
   | Eval of 'term list
   | Consequence of 'formula list * 'proof
 
-type ('term, 'formula, 'proof) acts = ('term, 'formula, 'proof) Solver_intf.acts = {
+type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = {
-  acts_iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
+  acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
   acts_eval_lit: 'formula -> lbool;
   acts_mk_lit: 'formula -> unit;
   acts_mk_term: 'term -> unit;

src/core/Solver_intf.ml

@@ -13,7 +13,7 @@ Copyright 2016 Simon Cruanes
 
 type 'a printer = Format.formatter -> 'a -> unit
 
-type ('term, 'form) sat_state = {
+type ('term, 'form, 'value) sat_state = {
   eval: 'form -> bool;
   (** Returns the valuation of a formula in the current state
       of the sat solver.
@@ -27,7 +27,7 @@ type ('term, 'form) sat_state = {
   iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
   (** Iter thorugh the formulas and terms in order of decision/propagation
       (starting from the first propagation, to the last propagation). *)
-  model: unit -> ('term * 'term) list;
+  model: unit -> ('term * 'value) list;
   (** Returns the model found if the formula is satisfiable. *)
 }
 (** The type of values returned when the solver reaches a SAT state. *)
@@ -68,9 +68,9 @@ type 'term eval_res =
     - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
 *)
 
-type ('term, 'formula) assumption =
+type ('term, 'formula, 'value) assumption =
   | Lit of 'formula  (** The given formula is asserted true by the solver *)
-  | Assign of 'term * 'term (** The first term is assigned to the second *)
+  | Assign of 'term * 'value (** The term is assigned to the value *)
 (** Asusmptions made by the core SAT solver. *)
 
 type ('term, 'formula, 'proof) reason =
@@ -86,8 +86,8 @@ 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) acts = {
+type ('term, 'formula, 'value, 'proof) acts = {
-  acts_iter_assumptions: (('term,'formula) assumption -> unit) -> unit;
+  acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
   (** Traverse the new assumptions on the boolean trail. *)
 
   acts_eval_lit: 'formula -> lbool;
@@ -164,7 +164,22 @@ module type EXPR = sig
 
     val hash : t -> int
     (** Hashing function for terms. Should be such that two terms equal according
-        to {!val:Expr_intf.S.equal} have the same hash. *)
+        to {!equal} have the same hash. *)
+
+    val pp : t printer
+    (** Printing function used among other for debugging. *)
+  end
+
+  module Value : sig
+    type t
+    (** The type of semantic values (domain elements) *)
+
+    val equal : t -> t -> bool
+    (** Equality over values. *)
+
+    val hash : t -> int
+    (** Hashing function for values. Should be such that two terms equal according
+        to {!equal} have the same hash. *)
 
     val pp : t printer
     (** Printing function used among other for debugging. *)
@@ -188,12 +203,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) acts -> unit
+  val partial_check : t -> (void, Formula.t, void, 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) acts -> unit
+  val final_check : t -> (void, Formula.t, void, 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;
@@ -207,25 +222,24 @@ module type PLUGIN_MCSAT = sig
 
   include EXPR
 
-
   val push_level : t -> unit
   (** Create a new backtrack level *)
 
   val pop_levels : t -> int -> unit
   (** Pop [n] levels of the theory *)
 
-  val partial_check : t -> (Term.t, Formula.t, proof) acts -> unit
+  val partial_check : t -> (Term.t, Formula.t, Value.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) acts -> unit
+  val final_check : t -> (Term.t, Formula.t, Value.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;
       if a conflict clause is added, search backtracks and then resumes. *)
 
-  val assign : t -> Term.t -> Term.t
+  val assign : t -> Term.t -> Value.t
   (** Returns an assignment value for the given term. *)
 
   val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit
@@ -407,7 +421,7 @@ module type S = sig
 
   (** Result type for the solver *)
   type res =
-    | Sat of (term,atom) sat_state (** Returned when the solver reaches SAT, with a model *)
+    | Sat of (term,atom,Value.t) sat_state (** Returned when the solver reaches SAT, with a model *)
     | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
 
   exception UndecidedLit

src/sudoku/sudoku_solve.ml

@@ -206,7 +206,7 @@ end = struct
       all_diff "squares" Grid.squares;
       ()
 
-    let trail_ (acts:(Msat.void,_,_) Msat.acts) = 
+    let trail_ (acts:_ Msat.acts) = 
       acts.acts_iter_assumptions
       |> Sequence.map
         (function