From 928622b5115e3c2247de196a6b8ab9c715ccd047 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 24 Jan 2017 10:55:52 +0100
Subject: [PATCH] [feature] New functions new_lit and new_atom

---
 src/core/external.ml    |  3 +++
 src/core/internal.ml    | 15 +++++++++++++++
 src/core/internal.mli   | 10 ++++++++++
 src/core/solver_intf.ml | 10 ++++++++++
 4 files changed, 38 insertions(+)

diff --git a/src/core/external.ml b/src/core/external.ml
index acfde77a..548fc3fc 100644
--- a/src/core/external.ml
+++ b/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
diff --git a/src/core/internal.ml b/src/core/internal.ml
index 345befcd..2fd8ce5e 100644
--- a/src/core/internal.ml
+++ b/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. *)
diff --git a/src/core/internal.mli b/src/core/internal.mli
index a8e2180b..ca0aef17 100644
--- a/src/core/internal.mli
+++ b/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. *)
diff --git a/src/core/solver_intf.ml b/src/core/solver_intf.ml
index b4673374..2852aadc 100644
--- a/src/core/solver_intf.ml
+++ b/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. *)