[breaking] Ceaner interface for mcsat propagations

src/core/internal.ml

@@ -328,13 +328,13 @@ module Make
               partition_aux trues unassigned falses (cl :: history) (i + 1)
             (* A var false at level 0 can be eliminated from the clause,
                but we need to kepp in mind that we used another clause to simplify it. *)
-            | Some (Semantic 0) ->
+            | Some Semantic ->
               partition_aux trues unassigned falses history (i + 1)
             (* Semantic propagations at level 0 are, well not easy to deal with,
                this shouldn't really happen actually (because semantic propagations
                at level 0 should come with a proof). *)
             (* TODO: get a proof of the propagation. *)
-            | None | Some (Decision | Semantic _ ) -> assert false
+            | None | Some Decision -> assert false
             (* The var must have a reason, and it cannot be a decision/assumption,
                since its level is 0. *)
           end else
@@ -498,6 +498,14 @@ module Make
     Log.debugf debug "Enqueue (%d): %a"
       (fun k->k (Vec.size env.elt_queue) pp_atom a)
 
+  let enqueue_semantic a terms =
+    let l = List.map St.add_term terms in
+    let lvl = List.fold_left (fun acc {l_level; _} ->
+        assert (l_level > 0); max acc l_level) 0 l in
+    assert (lvl > 0);
+    Iheap.grow_to_at_least env.order (St.nb_elt ());
+    enqueue_bool a lvl Semantic
+
   (* MCsat semantic assignment *)
   let enqueue_assign l value lvl =
     match l.assigned with
@@ -519,9 +527,9 @@ module Make
     if a.is_true || a.neg.is_true then None
     else match Plugin.eval a.lit with
       | Plugin_intf.Unknown -> None
-      | Plugin_intf.Valued (b, lvl) ->
+      | Plugin_intf.Valued (b, l) ->
         let atom = if b then a else a.neg in
-        enqueue_bool atom ~level:lvl (Semantic lvl);
+        enqueue_semantic atom l;
         Some b
 
   (* conflict analysis: find the list of atoms of [l] that have the
@@ -632,7 +640,7 @@ module Make
       | 0, _ ->
         cond := false;
         learnt := p.neg :: (List.rev !learnt)
-      | n, Some Semantic _ ->
+      | n, Some Semantic ->
         assert (n > 0);
         learnt := p.neg :: !learnt
       | n, Some Bcp cl ->
@@ -884,8 +892,8 @@ module Make
     match Vec.get env.elt_queue i with
     | Atom a ->
       Plugin_intf.Lit a.lit
-    | Lit {l_level; term; assigned = Some v} ->
+    | Lit {term; assigned = Some v} ->
-      Plugin_intf.Assign (term, v, l_level)
+      Plugin_intf.Assign (term, v)
     | Lit _ -> assert false
 
   let slice_push (l:formula list) (lemma:proof): unit =
@@ -896,10 +904,9 @@ module Make
        be done *)
     Stack.push c env.clauses_to_add
 
-  let slice_propagate f lvl =
+  let slice_propagate f l =
     let a = atom f in
-    Iheap.grow_to_at_least env.order (St.nb_elt ());
+    enqueue_semantic a l
-    enqueue_bool a lvl (Semantic lvl)
 
   let current_slice (): (_,_,_) Plugin_intf.slice = {
     Plugin_intf.start = env.th_head;
@@ -986,9 +993,9 @@ module Make
         new_decision_level();
         let current_level = decision_level () in
         enqueue_bool atom current_level Decision
-      | Plugin_intf.Valued (b, lvl) ->
+      | Plugin_intf.Valued (b, l) ->
         let a = if b then atom else atom.neg in
-        enqueue_bool a lvl (Semantic lvl)
+        enqueue_semantic a l
 
   and pick_branch_lit () =
     match env.next_decision with

src/core/plugin_intf.ml

@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type eval_res =
+type 'term eval_res =
-  | Valued of bool * int
   | Unknown
+  | Valued of bool * ('term list)
 (** The type of evaluation results, either the given formula cannot be
     evaluated, or it can thanks to assignment. In that case, the level
     of the evaluation is the maximum of levels of assignemnts needed
@@ -30,7 +30,7 @@ type ('formula, 'proof) res =
 
 type ('term, 'formula) assumption =
   | Lit of 'formula
-  | Assign of 'term * 'term * int (* Assign(x, alpha) *)
+  | Assign of 'term * 'term
 (** Asusmptions made by the core SAT solver. Can be either a formula, or an assignment.
     Assignemnt are given a level. *)
 
@@ -39,7 +39,7 @@ type ('term, 'formula, 'proof) slice = {
   length : int;
   get : int -> ('term, 'formula) assumption;
   push : 'formula list -> 'proof -> unit;
-  propagate : 'formula -> int -> unit;
+  propagate : 'formula -> 'term list -> unit;
 }
 (** The type for a slice of litterals to assume/propagate in the theory.
     [get] operations should only be used for integers [ start <= i < start + length].
@@ -86,7 +86,7 @@ module type S = sig
   val iter_assignable : (term -> unit) -> formula -> unit
   (** An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms) *)
 
-  val eval : formula -> eval_res
+  val eval : formula -> term eval_res
   (** Returns the evaluation of the formula in the current assignment *)
 
 end

src/core/solver_types.ml

@@ -68,7 +68,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   and reason =
     | Decision
     | Bcp of clause
-    | Semantic of int
+    | Semantic
 
   and premise =
     | Hyp
@@ -272,8 +272,8 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       Format.fprintf fmt "@@%d" n
     | n, Some Bcp c ->
       Format.fprintf fmt "->%d/%s" n c.name
-    | n, Some Semantic lvl ->
+    | n, Some Semantic ->
-      Format.fprintf fmt "::%d/%d" n lvl
+      Format.fprintf fmt "::%d" n
 
   let pp_level fmt a =
     pp_reason fmt (a.var.v_level, a.var.reason)

src/core/solver_types_intf.ml

@@ -75,8 +75,7 @@ module type S = sig
   and reason =
     | Decision        (** The atom has been decided by the sat solver *)
     | Bcp of clause   (** The atom has been propagated by the given clause *)
-    | Semantic of int (** The atom has been propagated by the theory at the given level.
+    | Semantic        (** The atom has been propagated by the theory at the given level. *)
-                          TODO: remove the int argument, as we should use the atom's level*)
   (** Reasons of propagation/decision of atoms. *)
 
   and premise =

src/mcsat/plugin_mcsat.ml

@@ -40,7 +40,7 @@ let false_ = Expr_smt.(Term.of_id (Id.ty "false" Ty.prop))
 
 (* Uninterpreted functions and predicates *)
 
-let map = H.create stack
+let map : Expr_smt.term H.t = H.create stack
 let watch = M.create 4096
 let interpretation = H.create stack
 
@@ -65,8 +65,8 @@ let update_job x ((t, watchees) as job) =
     begin match t with
       | { Expr_smt.term = Expr_smt.App (f, tys, l) } ->
         let is_prop = Expr_smt.(Ty.equal t.t_type Ty.prop) in
-        let t_v, _ = H.find map t in
+        let t_v = H.find map t in
-        let l' = List.map (fun x -> fst (H.find map x)) l in
+        let l' = List.map (H.find map) l in
         let u = Expr_smt.Term.apply f tys l' in
         begin try
             let t', u_v = H.find interpretation u in
@@ -110,8 +110,8 @@ let rec update_watches x = function
 let add_watch t l =
   update_job t (t, l)
 
-let add_assign t v lvl =
+let add_assign t v =
-  H.add map t (v, lvl);
+  H.add map t v;
   update_watches t (pop_watches t)
 
 (* Assignemnts *)
@@ -137,11 +137,11 @@ let iter_assignable f = function
 let eval = function
   | { Expr_smt.atom = Expr_smt.Pred t } ->
     begin try
-        let v, lvl = H.find map t in
+        let v = H.find map t in
         if Expr_smt.Term.equal v true_ then
-          Plugin_intf.Valued (true, lvl)
+          Plugin_intf.Valued (true, [t])
         else if Expr_smt.Term.equal v false_ then
-          Plugin_intf.Valued (false, lvl)
+          Plugin_intf.Valued (false, [t])
         else
           Plugin_intf.Unknown
       with Not_found ->
@@ -149,12 +149,12 @@ let eval = function
     end
   | { Expr_smt.atom = Expr_smt.Equal (a, b); sign } ->
     begin try
-        let v_a, a_lvl = H.find map a in
+        let v_a = H.find map a in
-        let v_b, b_lvl = H.find map b in
+        let v_b = H.find map b in
         if Expr_smt.Term.equal v_a v_b then
-          Plugin_intf.Valued(sign, max a_lvl b_lvl)
+          Plugin_intf.Valued(sign, [a; b])
         else
-          Plugin_intf.Valued(not sign, max a_lvl b_lvl)
+          Plugin_intf.Valued(not sign, [a; b])
       with Not_found ->
         Plugin_intf.Unknown
     end
@@ -171,8 +171,8 @@ let assume s =
   try
     for i = s.start to s.start + s.length - 1 do
       match s.get i with
-      | Assign (t, v, lvl) ->
+      | Assign (t, v) ->
-        add_assign t v lvl;
+        add_assign t v;
         E.add_tag uf t v
       | Lit f ->
         begin match f with
@@ -182,7 +182,7 @@ let assume s =
             E.add_neq uf u v
           | { Expr_smt.atom = Expr_smt.Pred p; sign } ->
             let v = if sign then true_ else false_ in
-            add_assign p v ~-1
+            add_assign p v
         end
     done;
     Plugin_intf.Sat