Added uninterpreted functions to mcsat solver

src/core/internal.ml

@@ -494,7 +494,8 @@ module Make
       l.assigned <- Some value;
       l.l_level <- lvl;
       Vec.push env.elt_queue (of_lit l);
-      ()
+      Log.debugf 20 "Enqueue (%d): %a"
+        (fun k -> k (Vec.size env.elt_queue) pp_lit l)
 
   (* evaluate an atom for MCsat, if it's not assigned
      by boolean propagation/decision *)

src/core/solver_types.ml

@@ -282,14 +282,14 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   let pp_assign out = function
     | None -> ()
-    | Some t -> Format.fprintf out " ->@ %a" E.Term.print t
+    | Some t -> Format.fprintf out " ->@ @[<hov>%a@]" E.Term.print t
 
   let pp_lit out v =
-    Format.fprintf out "%d [lit:%a%a]"
+    Format.fprintf out "%d [lit:@[<hov>%a%a@]]"
       (v.lid+1) E.Term.print v.term pp_assign v.assigned
 
   let pp_atom out a =
-    Format.fprintf out "%s%d%s[atom:%a]@ "
+    Format.fprintf out "%s%d%s[atom:@[<hov>%a@]]@ "
       (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
 
   let pp_atoms_vec out vec =

src/main.ml

@@ -189,9 +189,12 @@ let () =
     exit 4
   | Type_sat.Typing_error (msg, t)
   | Type_smt.Typing_error (msg, t) ->
+    let b = Printexc.get_backtrace () in
     let loc = match t.Dolmen.Term.loc with
       | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0
     in
     Format.fprintf Format.std_formatter "While typing:@\n%a@\n%a: typing error\n%s@."
-      Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg
+      Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg;
+    if Printexc.backtrace_status () then
+      Format.fprintf Format.std_formatter "%s@." b
 

src/mcsat/theory_mcsat.ml

@@ -3,15 +3,16 @@
 
 module E = Eclosure.Make(Expr_smt.Term)
 module H = Backtrack.Hashtbl(Expr_smt.Term)
+module M = Hashtbl.Make(Expr_smt.Term)
 
 (* Type definitions *)
 
 type proof = unit
 type term = Expr_smt.Term.t
 type formula = Expr_smt.Atom.t
-
 type level = Backtrack.Stack.level
 
+exception Absurd of Expr_smt.Atom.t list
 
 (* Backtracking *)
 
@@ -32,23 +33,97 @@ let assign t =
   | _, None -> t
   | _, Some (_, v) -> v
 
-(* Uninterpreted functions and predicates *)
-
-let map = H.create stack
+(* Propositional constants *)
 
 let true_ = Expr_smt.(Term.of_id (Id.ty "true" Ty.prop))
 let false_ = Expr_smt.(Term.of_id (Id.ty "false" Ty.prop))
 
+(* Uninterpreted functions and predicates *)
+
+let map = H.create stack
+let watch = M.create 4096
+let interpretation = H.create stack
+
+let pop_watches t =
+  try
+    let l = M.find watch t in
+    M.remove watch t;
+    l
+  with Not_found ->
+    []
+
+let add_job j x =
+  let l = try M.find watch x with Not_found -> [] in
+  M.add watch x (j :: l)
+
+let update_job x ((t, watchees) as job) =
+  try
+    let y = List.find (fun y -> not (H.mem map y)) watchees in
+    add_job job y
+  with Not_found ->
+    add_job job x;
+    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 l' = List.map (fun x -> fst (H.find map x)) l in
+        let u = Expr_smt.Term.apply f tys l' in
+        begin try
+            let t', u_v = H.find interpretation u in
+            if not (Expr_smt.Term.equal t_v u_v) then begin
+              match t' with
+              | { Expr_smt.term = Expr_smt.App (_, _, r) } when is_prop ->
+                let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in
+                if Expr_smt.(Term.equal u_v true_) then begin
+                  let res = Expr_smt.Atom.pred t ::
+                            Expr_smt.Atom.neg (Expr_smt.Atom.pred t') :: eqs in
+                  raise (Absurd res)
+                end else begin
+                  let res = Expr_smt.Atom.pred t' ::
+                            Expr_smt.Atom.neg (Expr_smt.Atom.pred t) :: eqs in
+                  raise (Absurd res)
+                end
+              | { Expr_smt.term = Expr_smt.App (_, _, r) } ->
+                let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in
+                let res = Expr_smt.Atom.eq t t' :: eqs in
+                raise (Absurd res)
+              | _ -> assert false
+            end
+          with Not_found ->
+            H.add interpretation u (t, t_v);
+        end
+      | _ -> assert false
+    end
+
+let rec update_watches x = function
+  | [] -> ()
+  | job :: r ->
+    begin
+      try
+        update_job x job;
+      with exn ->
+        List.iter (fun j -> add_job j x) r;
+        raise exn
+    end;
+    update_watches x r
+
+let add_watch t l =
+  update_job t (t, l)
+
 let add_assign t v lvl =
-  H.add map t (v, lvl)
+  H.add map t (v, lvl);
+  update_watches t (pop_watches t)
 
 (* Assignemnts *)
 
 let rec iter_aux f = function
   | { Expr_smt.term = Expr_smt.Var _ } as t ->
+    Log.debugf 10 "Adding %a as assignable" (fun k -> k Expr_smt.Term.print t);
     f t
   | { Expr_smt.term = Expr_smt.App (_, _, l) } as t ->
+    if l <> [] then add_watch t (t :: l);
     List.iter (iter_aux f) l;
+    Log.debugf 10 "Adding %a as assignable" (fun k -> k Expr_smt.Term.print t);
     f t
 
 let iter_assignable f = function
@@ -113,6 +188,8 @@ let assume s =
     done;
     Plugin_intf.Sat
   with
+  | Absurd l ->
+    Plugin_intf.Unsat (l, ())
   | E.Unsat (a, b, l) ->
     let c = Expr_smt.Atom.eq a b :: List.map Expr_smt.Atom.neg (chain_eq l) in
     Plugin_intf.Unsat (c, ())

tests/unsat/test-012.smt2

@@ -0,0 +1,2 @@
+(assert (and (= a b) (not (= (f a) (f b)))))
+(check-sat)