From 563e9027e1f7ea415c86c813f654a110ddacbb8a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 27 Jul 2016 16:40:36 +0200 Subject: [PATCH] first draft of replacing push/pop by assumptions --- src/core/external.ml | 70 +++++--- src/core/internal.ml | 318 ++++++++++------------------------ src/core/internal.mli | 30 +--- src/core/solver_intf.ml | 69 +++----- src/core/solver_types.ml | 15 +- src/core/solver_types_intf.ml | 4 +- src/main.ml | 16 +- 7 files changed, 182 insertions(+), 340 deletions(-) diff --git a/src/core/external.ml b/src/core/external.ml index c5c49729..bf9d8c94 100644 --- a/src/core/external.ml +++ b/src/core/external.ml @@ -6,6 +6,29 @@ Copyright 2016 Simon Cruanes module type S = Solver_intf.S +type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = { + eval: 'form -> bool; + (** Returns the valuation of a formula in the current state + of the sat solver. + @raise UndecidedLit if the literal is not decided *) + eval_level: 'form -> bool * int; + (** Return the current assignement of the literals, as well as its + decision level. If the level is 0, then it is necessary for + the atom to have this value; otherwise it is due to choices + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) + model: unit -> ('term * 'term) list; + (** Returns the model found if the formula is satisfiable. *) +} + +type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = { + unsat_conflict : unit -> 'clause; + (** Returns the unsat clause found at the toplevel *) + get_proof : unit -> 'proof; + (** returns a persistent proof of the empty clause from the Unsat result. *) +} + + module Make (St : Solver_types.S) (Th : Plugin_intf.S with type term = St.term @@ -25,36 +48,35 @@ module Make type clause = St.clause type proof = Proof.proof - type res = Sat | Unsat + type res = + | Sat of (St.term,St.formula) sat_state + | Unsat of (St.clause,Proof.proof) unsat_state - let assume ?tag l = - try S.assume ?tag l - with S.Unsat -> () + let assume ?tag l = S.assume ?tag l - let solve () = + let mk_sat () : _ sat_state = + { model=S.model; eval=S.eval; eval_level=S.eval_level } + + let mk_unsat () : _ unsat_state = + let unsat_conflict () = match S.unsat_conflict () with + | None -> assert false + | Some c -> c + in + let get_proof () = + let c = unsat_conflict() in + S.Proof.prove_unsat c + in + { unsat_conflict; get_proof; } + + let solve ?assumptions () = try - S.solve (); - Sat - with S.Unsat -> Unsat - - let eval = S.eval - let eval_level = S.eval_level - - let get_proof () = - match S.unsat_conflict () with - | None -> assert false - | Some c -> S.Proof.prove_unsat c + S.solve ?assumptions (); + Sat (mk_sat()) + with S.Unsat -> + Unsat (mk_unsat()) let unsat_core = S.Proof.unsat_core let get_tag cl = St.(cl.tag) - (* Push/pop operations *) - type level = S.level - let base_level = S.base_level - let current_level = S.current_level - let push = S.push - let pop = S.pop - let reset = S.reset - end diff --git a/src/core/internal.ml b/src/core/internal.ml index c4dd2233..a366a7fb 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -22,16 +22,6 @@ module Make exception Restart exception Conflict of clause - (* a push/pop state *) - type user_level = { - (* User levels always refer to decision_level 0 *) - ul_elt_lvl : int; (* Number of atoms in trail at decision level 0 *) - ul_th_lvl : int; (* Number of atoms known by the theory at decision level 0 *) - ul_th_env : Plugin.level; (* Theory state at level 0 *) - ul_clauses : int; (* number of clauses *) - ul_learnt : int; (* number of learnt clauses *) - } - (* Singleton type containing the current state *) type env = { @@ -49,7 +39,7 @@ module Make mutable unsat_conflict : clause option; - (* conflict clause at decision level 0, if any *) + (* conflict clause at [base_level], if any *) mutable next_decision : atom option; (* When the last conflict was a semantic one, this stores the next decision to make *) @@ -61,8 +51,6 @@ module Make (* decision levels in [trail] *) th_levels : Plugin.level Vec.t; (* theory states corresponding to elt_levels *) - user_levels : user_level Vec.t; - (* user-defined levels, for {!push} and {!pop} *) mutable th_head : int; (* Start offset in the queue {!elt_queue} of @@ -71,6 +59,10 @@ module Make (* Start offset in the queue {!elt_queue} of unit facts to propagate, within the trail *) + mutable base_level: int; + (* the decision level under which we cannot backtrack, that is, + the one after we pushed local assumptions *) + (* invariant: - during propagation, th_head <= elt_head - then, once elt_head reaches length elt_queue, Th.assume is @@ -140,14 +132,7 @@ module Make elt_queue = Vec.make 601 (of_atom dummy_atom); elt_levels = Vec.make 601 (-1); th_levels = Vec.make 100 Plugin.dummy; - - user_levels = Vec.make 20 { - ul_elt_lvl = 0; - ul_th_lvl = 0; - ul_learnt = 0; - ul_clauses = 0; - ul_th_env = Plugin.dummy; - }; + base_level = 0; order = Iheap.init 0; @@ -193,49 +178,6 @@ module Make | Some _ -> true | None -> false - (* Level for push/pop operations *) - type level = int - - (* Push/Pop *) - let current_level () = Vec.size env.user_levels - - let push () : level = - if is_unsat () then - (* When unsat, pushing does nothing, since adding more assumptions - can not make the proof disappear. *) - current_level () - else begin - (* The assumptions are sat, or at least not yet detected unsat, - we need to save enough to be able to restore the current decision - level 0. *) - let res = current_level () in - (* To restore decision level 0, we need the solver queue, and theory state. *) - let ul_elt_lvl, ul_th_lvl = - if Vec.is_empty env.elt_levels then - env.elt_head, env.th_head - else ( - let l = Vec.get env.elt_levels 0 in - l, l - ) - and ul_th_env = - if Vec.is_empty env.th_levels - then Plugin.current_level () - else Vec.get env.th_levels 0 - in - (* Keep in mind what are the current assumptions. *) - let ul_clauses = Vec.size env.clauses_hyps in - let ul_learnt = Vec.size env.clauses_learnt in - Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt;}; - res - end - - (* To store info for level 0, it is easier to push at module - initialisation, when there are no assumptions. *) - let base_level = - let l = push () in - assert (l = 0); - l - (* Iteration over subterms. When incrementing activity, we want to be able to iterate over all subterms of a formula. However, the function provided by the theory @@ -345,8 +287,8 @@ module Make if a.neg.is_true then begin (* If a variable is false, we need to see why it is false. *) match a.var.reason with - | None | Some Decision -> assert false - (* The var must have a reason, and it cannot be a decision, since we are + | None | Some Decision | Some Assumption -> assert false + (* The var must have a reason, and it cannot be a decision/assumption, since we are at level 0. *) | Some (Bcp cl) -> atoms, cl :: history (* The variable has been set to false because of another clause, @@ -598,10 +540,10 @@ module Make a UIP ("Unique Implication Point") precond: the atom list is sorted by decreasing decision level *) let backtrack_lvl ~is_uip : atom list -> int = function - | [] -> 0 + | [] -> env.base_level | [a] -> assert is_uip; - 0 + env.base_level | a :: b :: r -> if is_uip then ( (* backtrack below [a], so we can propagate [not a] *) @@ -609,7 +551,7 @@ module Make b.var.v_level ) else ( assert (a.var.v_level = b.var.v_level); - max (a.var.v_level - 1) 0 + max (a.var.v_level - 1) env.base_level ) (* result of conflict analysis, containing the learnt clause and some @@ -644,7 +586,7 @@ module Make try while true do let lvl, atoms = max_lvl_atoms !c in - if lvl = 0 then raise Exit; + if lvl = env.base_level then raise Exit; match atoms with | [] | [_] -> is_uip := true; @@ -670,7 +612,7 @@ module Make c := res | _ -> assert false end - | None | Some Decision | Some Semantic _ -> () + | None | Some Decision | Some Assumption | Some Semantic _ -> () end done; assert false with Exit -> @@ -692,7 +634,7 @@ module Make (* conflict analysis for SAT Same idea as the mcsat analyze function (without semantic propagations), except we look the the Last UIP (TODO: check ?), and do it in an imperative - and eficient manner. *) + and efficient manner. *) let analyze_sat c_clause : conflict_res = let pathC = ref 0 in let learnt = ref [] in @@ -707,14 +649,14 @@ module Make while !cond do begin match !c.cpremise with | History _ -> clause_bump_activity !c - | Hyp _ | Lemma _ -> () + | Hyp | Lemma _ -> () end; history := !c :: !history; (* visit the current predecessors *) for j = 0 to Array.length !c.atoms - 1 do let q = !c.atoms.(j) in - assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *) - if q.var.v_level = 0 then begin + assert (q.is_true || q.neg.is_true && q.var.v_level >= env.base_level); (* unsure? *) + if q.var.v_level <= env.base_level then begin assert (q.neg.is_true); match q.var.reason with | Some Bcp cl -> history := cl :: !history @@ -723,7 +665,7 @@ module Make if not q.var.seen then begin q.var.seen <- true; seen := q :: !seen; - if q.var.v_level > 0 then begin + if q.var.v_level > env.base_level then begin var_bump_activity q.var; if q.var.v_level >= decision_level () then begin incr pathC @@ -799,7 +741,8 @@ module Make let add_boolean_conflict (confl:clause): unit = env.next_decision <- None; env.conflicts <- env.conflicts + 1; - if decision_level() = 0 || Array_util.for_all (fun a -> a.var.v_level = 0) confl.atoms then + if decision_level() = 0 + || Array_util.for_all (fun a -> a.var.v_level <= env.base_level) confl.atoms then report_unsat confl; (* Top-level conflict *) let cr = analyze confl in cancel_until cr.cr_backtrack_lvl; @@ -809,9 +752,8 @@ module Make the clause is false in the current trail *) let add_clause ?(force=false) (init:clause) : unit = Log.debugf 90 "Adding clause:@[%a@]" (fun k -> k St.pp_clause init); - assert (init.c_level <= current_level ()); let vec = match init.cpremise with - | Hyp _ -> env.clauses_hyps + | Hyp -> env.clauses_hyps | Lemma _ -> env.clauses_learnt | History _ -> assert false in @@ -862,8 +804,7 @@ module Make env.nb_init_clauses <- nbc; while not (Stack.is_empty env.clauses_to_add) do let c = Stack.pop env.clauses_to_add in - if c.c_level <= current_level () then - add_clause c + add_clause c done end @@ -1119,41 +1060,6 @@ module Make let check_vec vec = Vec.iter check_clause vec - (* fixpoint of propagation and decisions until a model is found, or a - conflict is reached *) - let solve (): unit = - if is_unsat () then raise Unsat; - let n_of_conflicts = ref (to_float env.restart_first) in - let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in - try - while true do - begin try - search (to_int !n_of_conflicts) (to_int !n_of_learnts) - with - | Restart -> - n_of_conflicts := !n_of_conflicts *. env.restart_inc; - n_of_learnts := !n_of_learnts *. env.learntsize_inc - | Sat -> - assert (env.elt_head = Vec.size env.elt_queue); - Plugin.if_sat (full_slice ()); - flush_clauses(); - if is_unsat () then raise Unsat - else if env.elt_head = Vec.size env.elt_queue (* sanity check *) - && env.elt_head = St.nb_elt () - (* this is the important test to know if the search is finished *) - then raise Sat - end - done - with - | Sat -> () - - let assume ?tag cnf = - List.iter (fun l -> - let atoms = List.rev_map atom l in - let c = make_clause ?tag (fresh_hname ()) atoms (Hyp (current_level ())) in - Stack.push c env.clauses_to_add - ) cnf - let eval_level lit = let var, negated = make_boolean_var lit in if not var.pa.is_true && not var.na.is_true @@ -1168,10 +1074,6 @@ module Make let eval lit = fst (eval_level lit) - let hyps () = env.clauses_hyps - - let history () = env.clauses_learnt - let unsat_conflict () = env.unsat_conflict let model () : (term * term) list = @@ -1182,119 +1084,77 @@ module Make | Atom _ -> acc) [] env.elt_queue - (* Backtrack to decision_level 0, with trail_lim && theory env specified *) - let reset_until push_lvl (ul: user_level) = - Log.debug 1 "Resetting to decision level 0 (pop/forced)"; - env.th_head <- ul.ul_th_lvl ; - env.elt_head <- ul.ul_elt_lvl; - for c = env.elt_head to Vec.size env.elt_queue - 1 do - match Vec.get env.elt_queue c with - | Lit l -> - l.assigned <- None; - l.l_level <- -1; - insert_var_order (elt_of_lit l) - | Atom a -> - begin match a.var.reason with - | Some Bcp { c_level } when c_level > push_lvl -> - a.is_true <- false; - a.neg.is_true <- false; - a.var.v_level <- -1; - a.var.reason <- None; - insert_var_order (elt_of_var a.var) - | _ -> - if a.var.v_level = 0 then begin - (* [a] is still true, so we move it to the current top position - of the trail, as if it was propagated again *) - Vec.set env.elt_queue env.elt_head (of_atom a); - env.elt_head <- env.elt_head + 1 - end else begin - a.is_true <- false; - a.neg.is_true <- false; - a.var.v_level <- -1; - a.var.reason <- None; - insert_var_order (elt_of_var a.var) - end - end - done; - Plugin.backtrack ul.ul_th_env; (* recover the right theory env *) - Vec.shrink env.elt_queue ((Vec.size env.elt_queue) - env.elt_head); - Vec.clear env.elt_levels; - Vec.clear env.th_levels; - assert (Vec.size env.elt_levels = Vec.size env.th_levels); - assert (env.elt_head = Vec.size env.elt_queue); + (* push a series of assumptions to the stack *) + let push_assumptions = + List.iter + (fun lit -> + let a = atom lit in + if a.is_true then () + else if a.neg.is_true then ( + (* conflict between assumptions: UNSAT *) + let c = make_clause (fresh_hname ()) [a] Hyp in + add_boolean_conflict c; + assert false (* should raise Unsat *) + ) else ( + (* make a decision, propagate *) + new_decision_level(); + let level = decision_level() in + assert (env.base_level = level-1); + env.base_level <- level; + enqueue_bool a ~level Assumption; + match propagate () with + | Some confl -> (* Conflict *) + add_boolean_conflict confl; + assert false (* should raise Unsat *) + | None -> () + )) + + (* clear assumptions *) + let pop_assumptions (): unit = + cancel_until 0; + env.base_level <- 0; () - let pop l: unit = - (* Check sanity of pop *) - if l > current_level () then invalid_arg "cannot pop to level, it is too high" - else if l < current_level () then begin - - (* Filter the current buffer of clauses to remove potential assumptions - with too high a user level, - or else, with later pushes, these assumptions might be added. *) - let cl = ref [] in - Stack.iter (fun c -> - if c.c_level <= l then cl := c :: !cl) env.clauses_to_add; - Stack.clear env.clauses_to_add; - List.iter (fun c -> Stack.push c env.clauses_to_add) !cl; - - (* Get back the user level *) - let ul = Vec.get env.user_levels l in - Vec.shrink env.user_levels (max 0 (Vec.size env.user_levels - l - 1)); - - (* It is quite hard to check wether unsat status can be kept, so in doubt, we remove it *) - env.unsat_conflict <- None; - - (* Backtrack to the level 0 with appropriate settings *) - reset_until l ul; - - (* Log current assumptions for debugging purposes *) - Log.debugf 99 "@[Current trail:@ %a@]" - (fun k-> - let pp out () = - for i = 0 to Vec.size env.elt_queue - 1 do - Format.fprintf out "%s%s%d -- %a@," - (if i = ul.ul_elt_lvl then "*" else " ") - (if i = ul.ul_th_lvl then "*" else " ") - i (fun fmt e -> - match e with - | Lit l -> St.pp_lit fmt l - | Atom a -> St.pp_atom fmt a) - (Vec.get env.elt_queue i) - done - in - k pp ()); - - (* Clear hypothesis not valid anymore *) - for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do - let c = Vec.get env.clauses_hyps i in - assert (c.c_level > l); - detach_clause c - done; - Vec.shrink env.clauses_hyps (Vec.size env.clauses_hyps - ul.ul_clauses); - - (* Refresh the known tautologies simplified because of clauses that have been removed *) - let s = Stack.create () in - let new_sz = ref ul.ul_learnt in - for i = ul.ul_learnt to Vec.size env.clauses_learnt - 1 do - let c = Vec.get env.clauses_learnt i in - if c.c_level > l then begin - detach_clause c; - match c.cpremise with - | Lemma _ -> Stack.push c s - | History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s - | _ -> () (* Only simplified clauses can have a level > 0 *) - end else begin - Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c); - Vec.set env.clauses_learnt !new_sz c; - incr new_sz + (* fixpoint of propagation and decisions until a model is found, or a + conflict is reached *) + let solve ?(assumptions=[]) (): unit = + if env.base_level > 0 then pop_assumptions(); + if is_unsat () then raise Unsat; + let n_of_conflicts = ref (to_float env.restart_first) in + let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in + push_assumptions assumptions; + assert (env.base_level <= List.length assumptions); + try + while true do + begin try + search (to_int !n_of_conflicts) (to_int !n_of_learnts) + with + | Restart -> + n_of_conflicts := !n_of_conflicts *. env.restart_inc; + n_of_learnts := !n_of_learnts *. env.learntsize_inc + | Sat -> + assert (env.elt_head = Vec.size env.elt_queue); + Plugin.if_sat (full_slice ()); + flush_clauses(); + if is_unsat () then raise Unsat + else if env.elt_head = Vec.size env.elt_queue (* sanity check *) + && env.elt_head = St.nb_elt () + (* this is the important test to know if the search is finished *) + then raise Sat end - done; - Vec.shrink env.clauses_learnt (Vec.size env.clauses_learnt - !new_sz); - Stack.iter (add_clause ~force:true) s - end + done + with Sat -> () - let reset () = pop base_level + let assume ?tag cnf = + List.iter + (fun l -> + let atoms = List.rev_map atom l in + let c = make_clause ?tag (fresh_hname ()) atoms Hyp in + Stack.push c env.clauses_to_add) + cnf + let hyps () = env.clauses_hyps + + let history () = env.clauses_learnt end diff --git a/src/core/internal.mli b/src/core/internal.mli index 189f1d80..df91f3d7 100644 --- a/src/core/internal.mli +++ b/src/core/internal.mli @@ -18,9 +18,14 @@ module Make module Proof : Res.S with module St = St - val solve : unit -> unit + val solve : + ?assumptions:St.formula list -> + unit -> + unit (** Try and solves the current set of assumptions. @return () if the current set of clauses is satisfiable + @param assumptions list of additional local assumptions to make, + removed after the callback returns a value @raise Unsat if a toplevel conflict is found *) val assume : ?tag:int -> St.formula list list -> unit @@ -53,28 +58,5 @@ module Make val model : unit -> (St.term * St.term) list (** Returns the model found if the formula is satisfiable. *) - - - (** {2 Backtracking facilities} *) - - type level - (** Abstract notion of assumption level. *) - - val base_level : level - (** Level with no assumption at all, corresponding to the empty solver *) - - val current_level : unit -> level - (** The current level *) - - val push : unit -> level - (** Create a new level that extends the previous one. *) - - val pop : level -> unit - (** Go back to the given level, forgetting every assumption added since. - @raise Invalid_argument if the current level is below the argument *) - - val reset : unit -> unit - (** Return to level {!base_level} *) - end diff --git a/src/core/solver_intf.ml b/src/core/solver_intf.ml index 3b9ede7a..d90b5d58 100644 --- a/src/core/solver_intf.ml +++ b/src/core/solver_intf.ml @@ -4,6 +4,28 @@ Copyright 2016 Guillaume Bury Copyright 2016 Simon Cruanes *) +type ('term, 'form) sat_state = { + eval: 'form -> bool; + (** Returns the valuation of a formula in the current state + of the sat solver. + @raise UndecidedLit if the literal is not decided *) + eval_level: 'form -> bool * int; + (** Return the current assignement of the literals, as well as its + decision level. If the level is 0, then it is necessary for + the atom to have this value; otherwise it is due to choices + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) + model: unit -> ('term * 'term) list; + (** Returns the model found if the formula is satisfiable. *) +} + +type ('clause, 'proof) unsat_state = { + unsat_conflict : unit -> 'clause; + (** Returns the unsat clause found at the toplevel *) + get_proof : unit -> 'proof; + (** returns a persistent proof of the empty clause from the Unsat result. *) +} + module type S = sig (** {2 Internal modules} @@ -19,7 +41,9 @@ module type S = sig type atom = St.formula (** The type of atoms given by the module argument for formulas *) - type res = Sat | Unsat + type res = + | Sat of (St.term,St.formula) sat_state + | Unsat of (St.clause,Proof.proof) unsat_state (** Result type for the solver *) exception UndecidedLit @@ -32,26 +56,8 @@ module type S = sig (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) - val solve : unit -> res - (** Try and solves the current set of assumptions. - @return () if the current set of clauses is satisfiable - @raise Unsat if a toplevel conflict is found *) - - val eval : atom -> bool - (** Returns the valuation of a formula in the current state - of the sat solver. - @raise UndecidedLit if the literal is not decided *) - - val eval_level : atom -> bool * int - (** Return the current assignement of the literals, as well as its - decision level. If the level is 0, then it is necessary for - the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. - @raise UndecidedLit if the literal is not decided *) - - val get_proof : unit -> Proof.proof - (** If the last call to [solve] returned [Unsat], then returns a persistent - proof of the empty clause. *) + val solve : ?assumptions:atom list -> unit -> res + (** Try and solves the current set of assumptions. *) val unsat_core : Proof.proof -> St.clause list (** Returns the unsat core of a given proof. *) @@ -59,26 +65,5 @@ module type S = sig val get_tag : St.clause -> int option (** Recover tag from a clause, if any *) - (** {2 Push/Pop operations} *) - - type level - (** Abstract notion of assumption level. *) - - val base_level : level - (** Level with no assumption at all, corresponding to the empty solver *) - - val current_level : unit -> level - (** The current level *) - - val push : unit -> level - (** Create a new level that extends the previous one. *) - - val pop : level -> unit - (** Go back to the given level, forgetting every assumption added since. - @raise Invalid_argument if the current level is below the argument *) - - val reset : unit -> unit - (** Rest the state of the solver, i.e return to level {!base_level} *) - end diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index b0122364..50adf37a 100644 --- a/src/core/solver_types.ml +++ b/src/core/solver_types.ml @@ -58,7 +58,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct name : string; tag : int option; atoms : atom array; - c_level : int; mutable cpremise : premise; mutable activity : float; mutable attached : bool; @@ -69,9 +68,10 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct | Decision | Bcp of clause | Semantic of int + | Assumption and premise = - | Hyp of int + | Hyp | Lemma of proof | History of clause list @@ -106,7 +106,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct atoms = [| |]; activity = -1.; attached = false; - c_level = -1; visited = false; cpremise = History [] } @@ -187,18 +186,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let make_clause ?tag name ali premise = let atoms = Array.of_list ali in - let level = - match premise with - | Hyp lvl -> lvl - | Lemma _ -> 0 - | History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l - in { name = name; tag = tag; atoms = atoms; attached = false; visited = false; - c_level = level; activity = 0.; cpremise = premise} @@ -275,6 +267,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct | n, Some Decision -> sprintf "@@%d" n | n, Some Bcp c -> sprintf "->%d/%s" n c.name | n, Some Semantic lvl -> sprintf "::%d/%d" n lvl + | n, Some Assumption -> sprintf "!%d" n let value a = if a.is_true then sprintf "[T%s]" (level a) @@ -282,7 +275,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct else "[]" let pp_premise out = function - | Hyp _ -> Format.fprintf out "hyp" + | Hyp -> Format.fprintf out "hyp" | Lemma _ -> Format.fprintf out "th_lemma" | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 66cb0544..72556c0a 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -53,7 +53,6 @@ module type S = sig name : string; tag : int option; atoms : atom array; - c_level : int; mutable cpremise : premise; mutable activity : float; mutable attached : bool; @@ -64,9 +63,10 @@ module type S = sig | Decision | Bcp of clause | Semantic of int + | Assumption and premise = - | Hyp of int + | Hyp | Lemma of proof | History of clause list diff --git a/src/main.ml b/src/main.ml index 04e1c9c2..866c29c0 100644 --- a/src/main.ml +++ b/src/main.ml @@ -234,16 +234,16 @@ let main () = let res = Smt.solve () in Gc.delete_alarm al; begin match res with - | Smt.Sat -> + | Smt.Sat sat -> let t = Sys.time () in if !p_check then - if not (List.for_all (List.exists Smt.eval) cnf) then + if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then raise Incorrect_model; print "Sat (%f/%f)" t (Sys.time () -. t) - | Smt.Unsat -> + | Smt.Unsat us -> let t = Sys.time () in if !p_check then begin - let p = Smt.get_proof () in + let p = us.Solver_intf.get_proof () in Smt.Proof.check p; print_proof p; if !p_unsat_core then @@ -256,16 +256,16 @@ let main () = let res = Mcsat.solve () in Gc.delete_alarm al; begin match res with - | Mcsat.Sat -> + | Mcsat.Sat sat -> let t = Sys.time () in if !p_check then - if not (List.for_all (List.exists Mcsat.eval) cnf) then + if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then raise Incorrect_model; print "Sat (%f/%f)" t (Sys.time () -. t) - | Mcsat.Unsat -> + | Mcsat.Unsat us -> let t = Sys.time () in if !p_check then begin - let p = Mcsat.get_proof () in + let p = us.Solver_intf.get_proof () in Mcsat.Proof.check p; print_mcproof p; if !p_unsat_core then