diff --git a/src/core/internal.ml b/src/core/internal.ml index db29c488..18dfb011 100644 --- a/src/core/internal.ml +++ b/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 *) diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index 3ce9a01d..9eed6bf0 100644 --- a/src/core/solver_types.ml +++ b/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 " ->@ @[%a@]" E.Term.print t let pp_lit out v = - Format.fprintf out "%d [lit:%a%a]" + Format.fprintf out "%d [lit:@[%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:@[%a@]]@ " (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit let pp_atoms_vec out vec = diff --git a/src/main.ml b/src/main.ml index 0dbc9031..bc40bb32 100644 --- a/src/main.ml +++ b/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 diff --git a/src/mcsat/theory_mcsat.ml b/src/mcsat/theory_mcsat.ml index 8ff16e8f..46b718ae 100644 --- a/src/mcsat/theory_mcsat.ml +++ 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, ()) diff --git a/tests/unsat/test-012.smt2 b/tests/unsat/test-012.smt2 new file mode 100644 index 00000000..1a2946b1 --- /dev/null +++ b/tests/unsat/test-012.smt2 @@ -0,0 +1,2 @@ +(assert (and (= a b) (not (= (f a) (f b))))) +(check-sat)