From 64694b524d8b03db82a16ef78a6364bd45710625 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 25 Nov 2016 12:07:23 +0100 Subject: [PATCH] [breaking] Ceaner interface for mcsat propagations --- src/core/internal.ml | 31 +++++++++++++++++++------------ src/core/plugin_intf.ml | 10 +++++----- src/core/solver_types.ml | 6 +++--- src/core/solver_types_intf.ml | 3 +-- src/mcsat/plugin_mcsat.ml | 30 +++++++++++++++--------------- 5 files changed, 43 insertions(+), 37 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index 766f69e6..2fddf578 100644 --- a/src/core/internal.ml +++ b/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} -> - Plugin_intf.Assign (term, v, l_level) + | Lit {term; assigned = Some v} -> + 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_bool a lvl (Semantic lvl) + enqueue_semantic a l 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 diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml index 8400959f..6ed3e8c8 100644 --- a/src/core/plugin_intf.ml +++ b/src/core/plugin_intf.ml @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -type eval_res = - | Valued of bool * int +type 'term eval_res = | 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 diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index aa32b2ea..7d4fe172 100644 --- a/src/core/solver_types.ml +++ b/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 -> - Format.fprintf fmt "::%d/%d" n lvl + | n, Some Semantic -> + Format.fprintf fmt "::%d" n let pp_level fmt a = pp_reason fmt (a.var.v_level, a.var.reason) diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index ba627886..d2cbd691 100644 --- a/src/core/solver_types_intf.ml +++ b/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. - TODO: remove the int argument, as we should use the atom's level*) + | Semantic (** The atom has been propagated by the theory at the given level. *) (** Reasons of propagation/decision of atoms. *) and premise = diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml index 2f17975b..06c09c2e 100644 --- a/src/mcsat/plugin_mcsat.ml +++ b/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 l' = List.map (fun x -> fst (H.find map x)) l in + let t_v = H.find map t 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 = - H.add map t (v, lvl); +let add_assign t v = + 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_b, b_lvl = H.find map b in + let v_a = H.find map a 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) -> - add_assign t v lvl; + | Assign (t, v) -> + 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