From ced266663e4b886568842b90b10b6f62d526e414 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 25 Jan 2019 22:01:50 -0600 Subject: [PATCH] refactor: change backtracking API (push/pop_levels) --- src/core/Internal.ml | 22 ++++++++++------------ src/core/Solver_intf.ml | 30 ++++++++++++------------------ 2 files changed, 22 insertions(+), 30 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index b26b7e51..2eb2695f 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -736,8 +736,6 @@ module Make(Plugin : PLUGIN) elt_levels : int Vec.t; (* decision levels in [trail] *) - th_levels : Plugin.level Vec.t; - (* theory states corresponding to elt_levels *) mutable assumptions: atom Vec.t; (* current assumptions *) @@ -796,7 +794,6 @@ module Make(Plugin : PLUGIN) trail = Vec.create (); elt_levels = Vec.create(); - th_levels = Vec.create(); assumptions= Vec.create(); order = H.create(); @@ -1040,7 +1037,7 @@ module Make(Plugin : PLUGIN) assert (st.th_head = Vec.size st.trail); assert (st.elt_head = Vec.size st.trail); Vec.push st.elt_levels (Vec.size st.trail); - Vec.push st.th_levels (Plugin.current_level st.th); (* save the current theory state *) + Plugin.push_level st.th; () (* Attach/Detach a clause. @@ -1108,13 +1105,13 @@ module Make(Plugin : PLUGIN) ) done; (* Recover the right theory state. *) - Plugin.backtrack st.th (Vec.get st.th_levels lvl); + let n = decision_level st - lvl in + assert (n>0); + Plugin.pop_levels st.th n; (* Resize the vectors according to their new size. *) Vec.shrink st.trail !head; Vec.shrink st.elt_levels lvl; - Vec.shrink st.th_levels lvl; ); - assert (Vec.size st.elt_levels = Vec.size st.th_levels); () let pp_unsat_cause out = function @@ -1974,6 +1971,8 @@ module Make(Plugin : PLUGIN) check_vec st.clauses_hyps && check_vec st.clauses_learnt + let[@inline] theory st = st.th + (* Unsafe access to internal data *) let hyps env = env.clauses_hyps @@ -2112,16 +2111,15 @@ module Make_pure_sat(F: Solver_intf.FORMULA) = end type t = unit type proof = Solver_intf.void - type level = unit - let current_level () = () + let push_level () = () + let pop_levels _ _ = () let assume () _ = () let if_sat () _ = () - let backtrack () _ = () let eval () _ = Solver_intf.Unknown let assign () t = t let mcsat = false let iter_assignable () _ _ = () - let mcsat = false - end) + let mcsat = false +end) [@@inline][@@specialise] diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index a51fee18..f4059814 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -168,12 +168,11 @@ module type PLUGIN_CDCL_T = sig type proof - type level - (** The type for levels to allow backtracking. *) + val push_level : t -> unit + (** Create a new backtrack level *) - val current_level : t -> level - (** Return the current level of the theory (either the empty/beginning state, or the - last level returned by the [assume] function). *) + val pop_levels : t -> int -> unit + (** Pop [n] levels of the theory *) val assume : t -> (void, Formula.t, proof) slice -> unit (** Assume the formulas in the slice, possibly pushing new formulas to be @@ -184,10 +183,6 @@ module type PLUGIN_CDCL_T = sig If no new clause is pushed, then proof search ends and 'sat' is returned; if lemmas are added, search is resumed; if a conflict clause is added, search backtracks and then resumes. *) - - val backtrack : t -> level -> unit - (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the - same state as when it returned the value [l], *) end (** Signature for theories to be given to the Model Constructing Solver. *) @@ -197,12 +192,12 @@ module type PLUGIN_MCSAT = sig include EXPR - type level - (** The type for levels to allow backtracking. *) - val current_level : t -> level - (** Return the current level of the theory (either the empty/beginning state, or the - last level returned by the [assume] function). *) + val push_level : t -> unit + (** Create a new backtrack level *) + + val pop_levels : t -> int -> unit + (** Pop [n] levels of the theory *) val assume : t -> (Term.t, Formula.t, proof) slice -> unit (** Assume the formulas in the slice, possibly pushing new formulas to be @@ -214,10 +209,6 @@ module type PLUGIN_MCSAT = sig if lemmas are added, search is resumed; if a conflict clause is added, search backtracks and then resumes. *) - val backtrack : t -> level -> unit - (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the - same state as when it returned the value [l], *) - val assign : t -> Term.t -> Term.t (** Returns an assignment value for the given term. *) @@ -393,6 +384,9 @@ module type S = sig @param size the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses. *) + val theory : t -> theory + (** Access the theory state *) + (** {2 Types} *) (** Result type for the solver *)