Replaced clause number by tag in solver.assume

sat/sat.ml

@@ -94,12 +94,12 @@ module Make(Dummy : sig end) = struct
   type clause = SatSolver.St.clause
   type proof = SatSolver.Proof.proof
 
+  let tag_clause cl = SatSolver.St.(cl.tag)
+
   type res =
     | Sat
     | Unsat
 
-  let _i = ref 0
-
   let new_atom () =
     try
       Fsat.fresh ()
@@ -126,10 +126,9 @@ module Make(Dummy : sig end) = struct
       Sat
     with SatSolver.Unsat -> Unsat
 
-  let assume l =
-    incr _i;
+  let assume ?tag l =
     try
-      SatSolver.assume l !_i
+      SatSolver.assume ?tag l
     with SatSolver.Unsat -> ()
 
   let eval = SatSolver.eval

sat/sat.mli

@@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Fsat : Formula_intf.S
+module Fsat : Formula_intf.S with type t = int
 
 module Tseitin : Tseitin.S with type atom = Fsat.t
 
@@ -52,9 +52,12 @@ module Make(Dummy: sig end) : sig
   val eval : atom -> bool
   (** Return the current assignement of the literals. *)
 
-  val assume : atom list list -> unit
+  val assume : ?tag:int -> atom list list -> unit
   (** Add a list of clauses to the set of assumptions. *)
 
+  val tag_clause : clause -> int option
+  (** Returns the tag associated with the clause. *)
+
   val get_proof : unit -> proof
   (** Returns the resolution proof found, if [solve] returned [Unsat]. *)
 

smt/smt.ml

@@ -72,7 +72,6 @@ module Make(Dummy:sig end) = struct
     | Sat
     | Unsat
 
-  let _i = ref 0
   let solve () =
     try
       SmtSolver.solve ();
@@ -80,9 +79,8 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> Unsat
 
   let assume l =
-    incr _i;
     try
-      SmtSolver.assume l !_i
+      SmtSolver.assume l
     with SmtSolver.Unsat -> ()
 
   let get_proof () =

solver/solver.ml

@@ -394,10 +394,10 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     else
         partition_aux [] [] [] [] atoms
 
-  let add_clause ~cnumber atoms history =
+  let add_clause ?tag name atoms history =
     if env.is_unsat then raise Unsat;
-    let init_name = string_of_int cnumber in
-    let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in
+    let init_name = name in
+    let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in
     Log.debug 10 "Adding clause : %a" St.pp_clause init0;
     try
       let atoms, init = partition atoms init0 in
@@ -526,7 +526,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     let atoms = List.rev_map (fun x -> add_atom x) l in
     Iheap.grow_to_by_double env.order (St.nb_vars ());
     List.iter (fun a -> insert_var_order a.var) atoms;
-    add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
+    add_clause "lemma" atoms (Lemma lemma)
 
   let current_slice () = Th.({
       start = env.tatoms_qhead;
@@ -706,15 +706,15 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     with
     | Sat -> ()
 
-  let add_clauses cnf ~cnumber =
+  let add_clauses ?tag cnf =
     let aux cl =
-        add_clause ~cnumber cl (History []);
+        add_clause ?tag "hyp" cl (History []);
         match propagate () with
         | None -> () | Some confl -> report_unsat confl
     in
     List.iter aux cnf
 
-  let init_solver cnf ~cnumber =
+  let init_solver ?tag cnf =
     let nbv = St.nb_vars () in
     let nbc = env.nb_init_clauses + List.length cnf in
     Iheap.grow_to_by_double env.order nbv;
@@ -724,12 +724,11 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     Vec.grow_to_by_double env.clauses nbc;
     Vec.grow_to_by_double env.learnts nbc;
     env.nb_init_clauses <- nbc;
-    add_clauses cnf ~cnumber
+    add_clauses ?tag cnf
 
-
-  let assume cnf ~cnumber =
+  let assume ?tag cnf =
     let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
-    init_solver cnf ~cnumber
+    init_solver ?tag cnf
 
   let eval lit =
     let var, negated = make_var lit in

solver/solver.mli

@@ -31,7 +31,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
       @return () if the current set of clauses is satisfiable
       @raise Unsat if a toplevel conflict is found *)
 
-  val assume : F.t list list -> cnumber:int -> unit
+  val assume : ?tag:int -> F.t list list -> unit
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place.
       @raise Unsat if a conflict is detect when adding the clauses *)

solver/solver_types.ml

@@ -40,6 +40,7 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct
 
   and clause =
     { name : string;
+      tag : int option;
       atoms : atom Vec.t ;
       mutable activity : float;
       mutable removed : bool;
@@ -75,6 +76,7 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct
 
   let dummy_clause =
     { name = "";
+      tag = None;
       atoms = Vec.make_empty dummy_atom;
       activity = -1.;
       removed = false;
@@ -136,9 +138,10 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct
     let var, negated = make_var lit in
     if negated then var.na else var.pa
 
-  let make_clause name ali sz_ali is_learnt premise =
+  let make_clause ?tag name ali sz_ali is_learnt premise =
     let atoms = Vec.from_list ali sz_ali dummy_atom in
     { name  = name;
+      tag = tag;
       atoms = atoms;
       removed = false;
       learnt = is_learnt;

solver/solver_types_intf.ml

@@ -39,6 +39,7 @@ module type S = sig
 
   and clause = {
     name : string;
+    tag : int option;
     atoms : atom Vec.t;
     mutable activity : float;
     mutable removed : bool;
@@ -67,7 +68,7 @@ module type S = sig
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)
 
-  val make_clause : string -> atom list -> int -> bool -> premise -> clause
+  val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause
   (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
   val nb_vars : unit -> int