Give access to the trail

src/core/external.ml

@@ -17,6 +17,9 @@ type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = {
       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 *)
+  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
+  (** Iter thorugh the formulas and terms in order of decision/propagation
+      (starting from the first propagation, to the last propagation). *)
   model: unit -> ('term * 'term) list;
   (** Returns the model found if the formula is satisfiable. *)
 }
@@ -54,7 +57,19 @@ module Make
     | Unsat of (St.clause,Proof.proof) unsat_state
 
   let mk_sat () : (_,_) sat_state =
-    { model=S.model; eval=S.eval; eval_level=S.eval_level }
+    let t = S.trail () in
+    let iter f f' =
+      Vec.iter (function
+          | St.Atom a -> f a.St.lit
+          | St.Lit l -> f' l.St.term
+        ) t
+    in
+    {
+      eval = S.eval;
+      eval_level = S.eval_level;
+      iter_trail = iter;
+      model = S.model;
+    }
 
   let mk_unsat () : (_,_) unsat_state =
     let unsat_conflict () = match S.unsat_conflict () with

src/core/internal.ml

@@ -1179,11 +1179,16 @@ module Make
       List.iter aux l
     | Some _ -> ()
 
+
+  (* Unsafe access to internal data *)
+
   let hyps () = env.clauses_hyps
 
   let history () = env.clauses_learnt
 
   let temp () = env.clauses_temp
 
+  let trail () = env.elt_queue
+
 end
 

src/core/internal.mli

@@ -16,8 +16,6 @@ module Make
   exception Unsat
   exception UndecidedLit
 
-  module Proof : Res.S with module St = St
-
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.
       @return () if the current set of clauses is satisfiable
@@ -51,16 +49,10 @@ module Make
       that can potentially be backtracked.
       @raise UndecidedLit if the literal is not decided *)
 
-  val hyps : unit -> St.clause Vec.t
-  (** Returns the vector of assumptions used by the solver. May be slightly different
-      from the clauses assumed because of top-level simplification of clauses. *)
 
-  val temp : unit -> St.clause Vec.t
+  (** {2 Proofs and Models} *)
-  (** Returns the clauses coreesponding to the local assumptions.
-      All clauses in this vec are assured to be unit clauses. *)
 
-  val history : unit -> St.clause Vec.t
+  module Proof : Res.S with module St = St
-  (** Returns the history of learnt clauses, with no guarantees on order. *)
 
   val unsat_conflict : unit -> St.clause option
   (** Returns the unsat clause found at the toplevel, if it exists (i.e if
@@ -69,5 +61,28 @@ module Make
   val model : unit -> (St.term * St.term) list
   (** Returns the model found if the formula is satisfiable. *)
 
+
+  (** {2 Internal data}
+      These functions expose some internal data stored by the solver, as such
+      great care should be taken to ensure not to mess with the values returned. *)
+
+  val trail : unit -> St.t Vec.t
+  (** Returns the current trail.
+      *DO NOT MUTATE* *)
+
+  val hyps : unit -> St.clause Vec.t
+  (** Returns the vector of assumptions used by the solver. May be slightly different
+      from the clauses assumed because of top-level simplification of clauses.
+      *DO NOT MUTATE* *)
+
+  val temp : unit -> St.clause Vec.t
+  (** Returns the clauses coreesponding to the local assumptions.
+      All clauses in this vec are assured to be unit clauses.
+      *DO NOT MUTATE* *)
+
+  val history : unit -> St.clause Vec.t
+  (** Returns the history of learnt clauses, with no guarantees on order.
+      *DO NOT MUTATE* *)
+
 end
 

src/core/solver_intf.ml

@@ -15,6 +15,9 @@ type ('term, 'form) sat_state = {
       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 *)
+  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
+  (** Iter thorugh the formulas and terms in order of decision/propagation
+      (starting from the first propagation, to the last propagation). *)
   model: unit -> ('term * 'term) list;
   (** Returns the model found if the formula is satisfiable. *)
 }