Made SmtCommands independent from VeritSyntax

Made lfsc/* mostly independent from VeritSyntax

7 files changed, 80 insertions, 112 deletions

diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index c91cee1..0c5bf83 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -62,6 +62,3 @@ module Atom =
 module Form = SmtForm.Make(Atom)
 module Trace = SmtTrace.MakeOpt(Form)
 module Cnf = SmtCnf.MakeCnf(Form)
-
-      
-
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 49bc590..92f9bc7 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -38,38 +38,6 @@ module Form : SmtForm.FORM with type hatom = Atom.t
 
 module Trace :
   sig
-    val share_value : Form.t SmtCertif.clause -> unit
-    module HashedHeadRes :
-      sig
-        type t = Form.t SmtCertif.resolution
-        val equal :
-          'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
-        val hash : 'a SmtCertif.resolution -> int
-      end
-    module HRtbl :
-      sig
-        type key = HashedHeadRes.t
-        type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
-        val create : int -> 'a t
-        val clear : 'a t -> unit
-        val reset : 'a t -> unit
-        val copy : 'a t -> 'a t
-        val add : 'a t -> key -> 'a -> unit
-        val remove : 'a t -> key -> unit
-        val find : 'a t -> key -> 'a
-        val find_all : 'a t -> key -> 'a list
-        val replace : 'a t -> key -> 'a -> unit
-        val mem : 'a t -> key -> bool
-        val iter : (key -> 'a -> unit) -> 'a t -> unit
-        val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-        val length : 'a t -> int
-        val stats : 'a t -> Hashtbl.statistics
-      end
-    val common_head :
-      'a SmtCertif.clause list ->
-      'b SmtCertif.clause list ->
-      'a SmtCertif.clause list * 'a SmtCertif.clause list *
-      'b SmtCertif.clause list
     val share_prefix : Form.t SmtCertif.clause -> int -> unit
   end
 module Cnf :
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 78c07b9..e64a131 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -735,8 +735,8 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
              with Not_found ->
                let oc = open_out "/tmp/find_lemma.log" in
                let fmt = Format.formatter_of_out_channel oc in
-               List.iter (fun u -> Format.fprintf fmt "%a\n" VeritSyntax.hform_to_smt u) lsmt;
-               Format.fprintf fmt "\n%a\n" VeritSyntax.hform_to_smt hl;
+               List.iter (fun u -> Format.fprintf fmt "%a\n" (Form.to_smt ~debug:true) u) lsmt;
+               Format.fprintf fmt "\n%a\n" (Form.to_smt ~debug:true) hl;
                flush oc; close_out oc; failwith "find_lemma" end
       | _ -> failwith "unexpected form of root" in
 
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 20b99ac..12aef5a 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -68,8 +68,7 @@ module type FORM =
     val is_pos : t -> bool
     val is_neg : t -> bool
 
-    val to_smt : ?pi:bool ->
-                 (Format.formatter -> hatom -> unit) ->
+    val to_smt : ?debug:bool ->
                  Format.formatter -> t -> unit
 
     val logic : t -> logic
@@ -108,6 +107,13 @@ module type FORM =
     val interp_to_coq :
       (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
       t -> Structures.constr
+
+    (* Unstratified terms *)
+    type atom_form_lit =
+      | Atom of hatom
+      | Form of pform
+      | Lit of t
+    val lit_of_atom_form_lit : reify -> bool * atom_form_lit -> t
   end
 
 module Make (Atom:ATOM) =
@@ -157,29 +163,29 @@ module Make (Atom:ATOM) =
       | Neg hp -> hp.hval
 
 
-    let rec to_smt ?pi:(pi=false) atom_to_smt fmt = function
+    let rec to_smt ?debug:(debug=false) fmt = function
       | Pos hp ->
-         if pi then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
-         to_smt_pform atom_to_smt fmt hp.hval
+         if debug then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
+         to_smt_pform fmt hp.hval
       | Neg hp ->
-         if pi then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
+         if debug then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
          Format.fprintf fmt "(not ";
-         to_smt_pform atom_to_smt fmt hp.hval;
+         to_smt_pform fmt hp.hval;
          Format.fprintf fmt ")"
 
-    and to_smt_pform atom_to_smt fmt = function
-      | Fatom a -> atom_to_smt fmt a
-      | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args
+    and to_smt_pform fmt = function
+      | Fatom a -> Atom.to_smt fmt a
+      | Fapp (op,args) -> to_smt_op fmt op args
       (* This is an intermediate object of proofs, it correspond to nothing in SMT *)
       | FbbT (a, l) ->
-        Format.fprintf fmt "(bbT %a [" atom_to_smt a;
+        Format.fprintf fmt "(bbT %a [" Atom.to_smt a;
         let fi = ref true in
         List.iter (fun f -> Format.fprintf fmt "%s%a"
                       (if !fi then "" else "; ")
-                      (to_smt atom_to_smt) f; fi := false) l;
+                      (to_smt ~debug:false) f; fi := false) l;
         Format.fprintf fmt "])"
 
-    and to_smt_op atom_to_smt fmt op args =
+    and to_smt_op fmt op args =
       let (s1,s2) = if ((Array.length args = 0) || (match op with Fnot2 _ -> true | _ -> false)) then ("","") else ("(",")") in
       Format.fprintf fmt "%s" s1;
       (match op with
@@ -198,7 +204,7 @@ module Make (Atom:ATOM) =
              Format.fprintf fmt  ")")
       );
 
-      Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args;
+      Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) args;
       Format.fprintf fmt "%s" s2
 
     and to_smt_args fmt = function
@@ -275,6 +281,7 @@ module Make (Atom:ATOM) =
 		| a0::a1::a2::_ ->
                    (to_lit a2) lsl 4 + (to_lit a1) lsl 2 + to_lit a0 in
               (hash_args * 10 + Atom.index ha) * 2 + 1
+
       end
 
     module HashForm = Hashtbl.Make (HashedForm)
@@ -289,34 +296,34 @@ module Make (Atom:ATOM) =
     let check pf =
       match pf with
       | Fatom ha ->  if not (Atom.is_bool_type ha) then
-          raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+          raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                  NotWellTyped pf)
       | Fapp (op, args) ->
 	(match op with
 	 | Ftrue | Ffalse ->
            if Array.length args <> 0 then
-             raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                     NotWellTyped pf)
 	 | Fnot2 _ ->
            if Array.length args <> 1 then
-             raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                     NotWellTyped pf)
 	 | Fand | For -> ()
 	 | Fxor | Fimp | Fiff ->
            if Array.length args <> 2 then
-             raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                     NotWellTyped pf)
 
           | Fite ->
             if Array.length args <> 3 then
-              raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+              raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                      NotWellTyped pf)
 
          | Fforall l -> ()
        )
 
       | FbbT (ha, l) -> if not (Atom.is_bv_type ha) then
-          raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+          raise (Format.eprintf "nwt: %a" to_smt_pform pf;
                  NotWellTyped pf)
 
     let declare reify pf =
@@ -639,4 +646,17 @@ module Make (Atom:ATOM) =
 	  done;
 	  !r in
         interp_form f
+
+    (* Unstratified terms *)
+    type atom_form_lit =
+      | Atom of hatom
+      | Form of pform
+      | Lit of t
+
+    let lit_of_atom_form_lit rf = function
+      | decl, Atom a -> get ~declare:decl rf (Fatom a)
+      | decl, Form f -> begin match f with
+                          | Fapp (Fforall _, _) when decl -> failwith "decl is true on a forall"
+                          | _ -> get ~declare:decl rf f end
+      | decl, Lit l -> l
 end
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index ba8c066..ad7d2ca 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -64,8 +64,7 @@ module type FORM =
       val is_pos : t -> bool
       val is_neg : t -> bool
 
-      val to_smt : ?pi:bool ->
-                   (Format.formatter -> hatom -> unit) ->
+      val to_smt : ?debug:bool ->
                    Format.formatter -> t -> unit
 
       val logic : t -> logic
@@ -105,6 +104,13 @@ module type FORM =
       val interp_to_coq :
 	  (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
 	    t -> Structures.constr
+
+      (* Unstratified terms *)
+      type atom_form_lit =
+        | Atom of hatom
+        | Form of pform
+        | Lit of t
+      val lit_of_atom_form_lit : reify -> bool * atom_form_lit -> t
   end
 
 module Make (Atom:ATOM) : FORM with type hatom = Atom.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 5d9d82d..f397826 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -14,11 +14,14 @@ open SmtMisc
 open CoqTerms
 open SmtCertif
 
+
+(** Steps identifiers **)
+
 let notUsed = 0
 
 let next_id = ref 0
 
-let clear () = next_id := 0
+let clear_id () = next_id := 0
 
 let next_id () =
   let id = !next_id in
@@ -170,7 +173,7 @@ let order_roots init_index first =
 the following clauses reference those clauses instead of the roots *)
 let add_scertifs to_add c =
   let r = ref c in
-  clear (); ignore (next_id ());
+  clear_id (); ignore (next_id ());
   while isRoot !r.kind do
     ignore (next_id ());
     r := next !r;
@@ -498,25 +501,25 @@ let to_coq to_lit interp (cstep,
 module MakeOpt (Form:SmtForm.FORM) =
   struct
     (* Share the certificate building a common clause *)
-    let share_value c =
-      let tbl = Hashtbl.create 17 in
-      let to_lits v = List.map (Form.to_lit) v in
-      let process c =
-	match c.value with
-	| None -> ()
-	| Some v ->
-	    let lits = to_lits v in
-	    try
-	      let c' = Hashtbl.find tbl lits in
-	      set_same c c'
-	    with Not_found  -> Hashtbl.add tbl lits c in
-      let r = ref c in
-      while !r.next <> None do
-	let next = next !r in
-	process !r;
-	r := next
-      done;
-      process !r
+    (* let share_value c =
+     *   let tbl = Hashtbl.create 17 in
+     *   let to_lits v = List.map (Form.to_lit) v in
+     *   let process c =
+     *     match c.value with
+     *     | None -> ()
+     *     | Some v ->
+     *         let lits = to_lits v in
+     *         try
+     *           let c' = Hashtbl.find tbl lits in
+     *           set_same c c'
+     *         with Not_found  -> Hashtbl.add tbl lits c in
+     *   let r = ref c in
+     *   while !r.next <> None do
+     *     let next = next !r in
+     *     process !r;
+     *     r := next
+     *   done;
+     *   process !r *)
 
    (* Sharing of the common prefix *)
 
@@ -593,3 +596,6 @@ module MakeOpt (Form:SmtForm.FORM) =
       done
 
   end
+
+
+let clear () = clear_id ()
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index 5ded32a..a12e2e7 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -10,6 +10,7 @@
 (**************************************************************************)
 
 
+(* Traces *)
 val notUsed : int
 val clear : unit -> unit
 val next_id : unit -> SmtCertif.clause_id
@@ -67,40 +68,10 @@ val to_coq :
   ('a SmtCertif.clause -> Structures.types * Structures.constr) option ->
   Structures.constr * 'a SmtCertif.clause *
     (Structures.id * Structures.types) list
+
+
 module MakeOpt :
   functor (Form : SmtForm.FORM) ->
     sig
-      val share_value : Form.t SmtCertif.clause -> unit
-      module HashedHeadRes :
-        sig
-          type t = Form.t SmtCertif.resolution
-          val equal :
-            'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
-          val hash : 'a SmtCertif.resolution -> int
-        end
-      module HRtbl :
-        sig
-          type key = HashedHeadRes.t
-          type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
-          val create : int -> 'a t
-          val clear : 'a t -> unit
-          val reset : 'a t -> unit
-          val copy : 'a t -> 'a t
-          val add : 'a t -> key -> 'a -> unit
-          val remove : 'a t -> key -> unit
-          val find : 'a t -> key -> 'a
-          val find_all : 'a t -> key -> 'a list
-          val replace : 'a t -> key -> 'a -> unit
-          val mem : 'a t -> key -> bool
-          val iter : (key -> 'a -> unit) -> 'a t -> unit
-          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-          val length : 'a t -> int
-          val stats : 'a t -> Hashtbl.statistics
-        end
-      val common_head :
-        'a SmtCertif.clause list ->
-        'b SmtCertif.clause list ->
-        'a SmtCertif.clause list * 'a SmtCertif.clause list *
-        'b SmtCertif.clause list
       val share_prefix : Form.t SmtCertif.clause -> int -> unit
     end