[feature] New functions new_lit and new_atom

src/core/external.ml

@@ -118,6 +118,9 @@ module Make
 
   let get_tag cl = St.(cl.tag)
 
+  let new_lit = S.new_lit
+  let new_atom = S.new_atom
+
   (* Dimacs & iCNF export *)
   let export_vec name fmt vec =
     Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.pp_dimacs) vec

src/core/internal.ml

@@ -233,6 +233,21 @@ module Make
       Iheap.insert f_weight env.order v.vid;
       iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
 
+  (* Add new litterals/atoms on which to decide on, even if there is no
+     clause that constrains it.
+     We could maybe check if they have already has been decided before
+     inserting them into the heap, if it appears that it helps performance. *)
+  let new_lit t =
+    let l = add_term t in
+    insert_var_order (E_lit l)
+
+  let new_atom p =
+    let a = atom p in
+    (* This is necessary to ensure that the var will not be dropped
+       during the next backtrack. *)
+    a.var.used <- a.var.used + 1;
+    insert_var_order (E_var a.var)
+
   (* Rather than iterate over all the heap when we want to decrease all the
      variables/literals activity, we instead increase the value by which
      we increase the activity of 'interesting' var/lits. *)

src/core/internal.mli

@@ -33,6 +33,16 @@ module Make
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
+  val new_lit : St.term -> unit
+  (** Add a new litteral (i.e term) to the solver. This term will
+      be decided on at some point during solving, wether it appears
+      in clauses or not. *)
+
+  val new_atom : St.formula -> unit
+  (** Add a new atom (i.e propositional formula) to the solver.
+      This formula will be decided on at some point during solving,
+      wether it appears in clauses or not. *)
+
   val push : unit -> unit
   (** Create a decision level for local assumptions.
       @raise Unsat if a conflict is detected in the current state. *)

src/core/solver_intf.ml

@@ -76,6 +76,16 @@ module type S = sig
   val solve : ?assumptions:atom list -> unit -> res
   (** Try and solves the current set of assumptions. *)
 
+  val new_lit : St.term -> unit
+  (** Add a new litteral (i.e term) to the solver. This term will
+      be decided on at some point during solving, wether it appears
+      in clauses or not. *)
+
+  val new_atom : atom -> unit
+  (** Add a new atom (i.e propositional formula) to the solver.
+      This formula will be decided on at some point during solving,
+      wether it appears in clauses or not. *)
+
   val unsat_core : Proof.proof -> St.clause list
   (** Returns the unsat core of a given proof. *)