Made SmtCommands independent from VeritSyntax

Made lfsc/* mostly independent from VeritSyntax

4 files changed, 75 insertions, 68 deletions

diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml
index a11139d..7938885 100644
--- a/src/lfsc/lfsc.ml
+++ b/src/lfsc/lfsc.ml
@@ -134,7 +134,9 @@ let import_trace_from_file first filename =
 
 let clear_all () =
   SmtTrace.clear ();
+  SmtMaps.clear ();
   VeritSyntax.clear ();
+  Tosmtcoq.clear ();
   C.clear ()
 
 
@@ -142,8 +144,8 @@ let import_all fsmt fproof =
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
-  let ra = VeritSyntax.ra in
-  let rf = VeritSyntax.rf in
+  let ra = Tosmtcoq.ra in
+  let rf = Tosmtcoq.rf in
   let roots = Smtlib2_genConstr.import_smtlib2 rt ro ra rf fsmt in
   let (max_id, confl) = import_trace_from_file None fproof in
   (rt, ro, ra, rf, roots, max_id, confl)
@@ -362,13 +364,13 @@ let call_cvc4 env rt ro ra rf root _ =
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
-    VeritSyntax.add_btype s (SmtBtype.Tindex t);
+    SmtMaps.add_btype s (SmtBtype.Tindex t);
     declare_sort cvc4 s 0;
   ) (SmtBtype.to_list rt);
   
   List.iter (fun (i,cod,dom,op) ->
     let s = "op_"^(string_of_int i) in
-    VeritSyntax.add_fun s op;
+    SmtMaps.add_fun s op;
     let args =
       Array.fold_right
         (fun t acc -> asprintf "%a" SmtBtype.to_smt t :: acc) cod [] in
@@ -376,7 +378,7 @@ let call_cvc4 env rt ro ra rf root _ =
     declare_fun cvc4 s args ret
   ) (Op.to_list ro);
 
-  assume cvc4 (asprintf "%a" (Form.to_smt Atom.to_smt) fl);
+  assume cvc4 (asprintf "%a" (Form.to_smt ~debug:false) fl);
 
   let proof =
     match check_sat cvc4 with
@@ -407,13 +409,13 @@ let export out_channel rt ro l =
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
-    VeritSyntax.add_btype s (SmtBtype.Tindex t);
+    SmtMaps.add_btype s (SmtBtype.Tindex t);
     fprintf fmt "(declare-sort %s 0)@." s
   ) (SmtBtype.to_list rt);
 
   List.iter (fun (i,cod,dom,op) ->
     let s = "op_"^(string_of_int i) in
-    VeritSyntax.add_fun s op;
+    SmtMaps.add_fun s op;
     fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
     Array.iter (fun t ->
@@ -424,7 +426,7 @@ let export out_channel rt ro l =
   ) (Op.to_list ro);
 
   fprintf fmt "(assert %a)@\n(check-sat)@\n(exit)@."
-    (Form.to_smt Atom.to_smt) l
+    (Form.to_smt ~debug:false) l
 
 
 
@@ -488,14 +490,12 @@ let tactic_gen vm_cast =
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
-  let ra = VeritSyntax.ra in
-  let rf = VeritSyntax.rf in
-  let ra' = VeritSyntax.ra in
-  let rf' = VeritSyntax.rf in
+  let ra = Tosmtcoq.ra in
+  let rf = Tosmtcoq.rf in
+  let ra' = Tosmtcoq.ra in
+  let rf' = Tosmtcoq.rf in
   SmtCommands.tactic call_cvc4 cvc4_logic rt ro ra rf ra' rf' vm_cast [] []
-  (* let ra = VeritSyntax.ra in
-   * let rf = VeritSyntax.rf in
-   * (\* Currently, quantifiers are not handled by the cvc4 tactic: we pass
+  (* (\* Currently, quantifiers are not handled by the cvc4 tactic: we pass
    *    the same ra and rf twice to have everything reifed *\)
    * SmtCommands.tactic call_cvc4 cvc4_logic rt ro ra rf ra rf vm_cast [] [] *)
 let tactic () = tactic_gen vm_cast_true
diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml
index f520ba7..6382e9e 100644
--- a/src/lfsc/tosmtcoq.ml
+++ b/src/lfsc/tosmtcoq.ml
@@ -12,18 +12,20 @@
 
 open SmtAtom
 open SmtForm
-open VeritSyntax
 open Ast
 open Builtin
 open Format
 open Translator_sig
 open SmtBtype
 
+let ra = Atom.create ()
+let rf = Form.create ()
+
 type lit = SmtAtom.Form.t
 
 type clause = lit list
 
-let lit_of_atom_form_lit rf af = lit_of_atom_form_lit rf (true, af)
+let lit_of_atom_form_lit rf af = Form.lit_of_atom_form_lit rf (true, af)
 
 let show_veritproof =
   try ignore (Sys.getenv "DONTSHOWVERIT"); false
@@ -213,44 +215,44 @@ let rec const_bv_aux acc t = match name t with
 
 let const_bv t =
   let bv_list = const_bv_aux [] t in
-  Atom (Atom.mk_bvconst ra bv_list)
+  Form.Atom (Atom.mk_bvconst ra bv_list)
 
 
 let rec term_smtcoq_old t =
   match value t with
-  | Const {sname=Name n} when n == H.ttrue -> Form Form.pform_true
-  | Const {sname=Name n} when n == H.tfalse -> Form Form.pform_false
+  | Const {sname=Name n} when n == H.ttrue -> Form.Form Form.pform_true
+  | Const {sname=Name n} when n == H.tfalse -> Form.Form Form.pform_false
   | Const {sname=Name n} when n == H.bvn -> const_bv t
   | Const {sname=Name n} ->
     begin
       try
         term_smtcoq  (HS.find alias_tbl n)
       with Not_found ->
-        Atom (Atom.get ra (Aapp (get_fun (Hstring.view n),[||])))
+        Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun (Hstring.view n),[||])))
     end
-  | Int bi -> Atom (Atom.hatom_Z_of_bigint ra bi)
+  | Int bi -> Form.Atom (Atom.hatom_Z_of_bigint ra bi)
   | App _ ->
     begin match app_name t with
       | Some (n, [f]) when n == H.not_ ->
-        Lit (Form.neg (lit_of_atom_form_lit rf (term_smtcoq f)))
-      | Some (n, args) when n == H.and_ -> Form (Fapp (Fand, args_smtcoq args))
-      | Some (n, args) when n == H.or_ -> Form (Fapp (For, args_smtcoq args))
-      | Some (n, args) when n == H.impl_ -> Form (Fapp (Fimp, args_smtcoq args))
-      | Some (n, args) when n == H.xor_ -> Form (Fapp (Fxor, args_smtcoq args))
+        Form.Lit (Form.neg (lit_of_atom_form_lit rf (term_smtcoq f)))
+      | Some (n, args) when n == H.and_ -> Form.Form (Fapp (Fand, args_smtcoq args))
+      | Some (n, args) when n == H.or_ -> Form.Form (Fapp (For, args_smtcoq args))
+      | Some (n, args) when n == H.impl_ -> Form.Form (Fapp (Fimp, args_smtcoq args))
+      | Some (n, args) when n == H.xor_ -> Form.Form (Fapp (Fxor, args_smtcoq args))
       | Some (n, args) when n == H.ite || n == H.ifte_ ->
-        Form (Fapp (Fite, args_smtcoq args))
-      | Some (n, args) when n == H.iff -> Form (Fapp (Fiff, args_smtcoq args))
+        Form.Form (Fapp (Fite, args_smtcoq args))
+      | Some (n, args) when n == H.iff -> Form.Form (Fapp (Fiff, args_smtcoq args))
       | Some (n, [_; a; b]) when n == H.eq ->
         let h1, h2 = term_smtcoq_atom a, term_smtcoq_atom b in
-        Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2)
+        Form.Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2)
       | Some (n, _) when n == H.apply -> uncurry [] t
       | Some (n, [p]) when n == H.p_app -> term_smtcoq p
       | Some (n, [{value = Int bi}]) when n == H.a_int ->
-        Atom (Atom.hatom_Z_of_bigint ra bi)
+        Form.Atom (Atom.hatom_Z_of_bigint ra bi)
       | Some (n, [ni]) when n == H.a_int ->
         begin match app_name ni with
           | Some (n, [{value = Int bi}]) when n == H.uminus ->
-            Atom (Atom.hatom_Z_of_bigint ra (Big_int.minus_big_int bi))
+            Form.Atom (Atom.hatom_Z_of_bigint ra (Big_int.minus_big_int bi))
           | _ -> assert false
         end
       | Some (n, [_; v]) when n == H.a_var_bv -> term_smtcoq v
@@ -259,83 +261,83 @@ let rec term_smtcoq_old t =
       | Some (b, [a; {value = Int n}]) when b == H.bitof ->
          (let ha = term_smtcoq_atom a in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bitof ra s (Big_int.int_of_big_int n) ha)
+            | TBV s -> Form.Atom (Atom.mk_bitof ra s (Big_int.int_of_big_int n) ha)
             | _ -> assert false)
       | Some (n, [_; a; bb]) when n == H.bblast_term ->
-        Form (FbbT ((term_smtcoq_atom a), bblt_lits [] bb))
+        Form.Form (FbbT ((term_smtcoq_atom a), bblt_lits [] bb))
       | Some (n, [_; a]) when n == H.bvnot ->
          (let ha = term_smtcoq_atom a in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvnot ra s ha)
+            | TBV s -> Form.Atom (Atom.mk_bvnot ra s ha)
             | _ -> assert false)
       | Some (n, [_; a]) when n == H.bvneg ->
          (let ha = term_smtcoq_atom a in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvneg ra s ha)
+            | TBV s -> Form.Atom (Atom.mk_bvneg ra s ha)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvand ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvand ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvand ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvor ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvor ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvor ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvxor ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvxor ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvxor ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvadd ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvadd ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvadd ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvmul ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvmult ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvmult ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvult ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvult ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvult ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvslt ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvslt ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvslt ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvule ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
          | TBV s ->
-           let a = Atom (Atom.mk_bvult ra s hb ha) in
-           Lit (Form.neg (lit_of_atom_form_lit rf a))
+           let a = Form.Atom (Atom.mk_bvult ra s hb ha) in
+           Form.Lit (Form.neg (lit_of_atom_form_lit rf a))
          | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvsle ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
          | TBV s ->
-           let a = Atom (Atom.mk_bvslt ra s hb ha) in
-           Lit (Form.neg (lit_of_atom_form_lit rf a))
+           let a = Form.Atom (Atom.mk_bvslt ra s hb ha) in
+           Form.Lit (Form.neg (lit_of_atom_form_lit rf a))
          | _ -> assert false)         
       | Some (n, [_; _; _; a; b]) when n == H.concat ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha, Atom.type_of hb with
-            | TBV s1, TBV s2 -> Atom (Atom.mk_bvconcat ra s1 s2 ha hb)
+            | TBV s1, TBV s2 -> Form.Atom (Atom.mk_bvconcat ra s1 s2 ha hb)
             | _ -> assert false)
       | Some (n, [_; {value = Int bj}; {value = Int bi}; _; a])
         when n == H.extract ->
@@ -343,51 +345,51 @@ let rec term_smtcoq_old t =
          let i = Big_int.int_of_big_int bi in
          let j = Big_int.int_of_big_int bj in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) ha)
+            | TBV s -> Form.Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) ha)
             | _ -> assert false)
       | Some (n, [_; {value = Int bi}; _; a])
         when n == H.zero_extend ->
         (let ha = term_smtcoq_atom a in
          let n = Big_int.int_of_big_int bi in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvzextn ra ~s ~n ha)
+            | TBV s -> Form.Atom (Atom.mk_bvzextn ra ~s ~n ha)
             | _ -> assert false)
       | Some (n, [_; {value = Int bi}; _; a])
         when n == H.sign_extend ->
         (let ha = term_smtcoq_atom a in
          let n = Big_int.int_of_big_int bi in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvsextn ra ~s ~n ha)
+            | TBV s -> Form.Atom (Atom.mk_bvsextn ra ~s ~n ha)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvshl ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvshl ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvshl ra s ha hb)
             | _ -> assert false)
       | Some (n, [_; a; b]) when n == H.bvlshr ->
          (let ha = term_smtcoq_atom a in
           let hb = term_smtcoq_atom b in
           match Atom.type_of ha with
-            | TBV s -> Atom (Atom.mk_bvshr ra s ha hb)
+            | TBV s -> Form.Atom (Atom.mk_bvshr ra s ha hb)
             | _ -> assert false)
 
       | Some (n, [a; b]) when n == H.lt_Int ->
-        Atom (Atom.mk_lt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_lt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.le_Int ->
-        Atom (Atom.mk_le ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_le ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.gt_Int ->
-        Atom (Atom.mk_gt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_gt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.ge_Int ->
-        Atom (Atom.mk_ge ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_ge ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.plus_Int ->
-        Atom (Atom.mk_plus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_plus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.minus_Int ->
-        Atom (Atom.mk_minus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_minus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a; b]) when n == H.times_Int ->
-        Atom (Atom.mk_mult ra (term_smtcoq_atom a) (term_smtcoq_atom b))
+        Form.Atom (Atom.mk_mult ra (term_smtcoq_atom a) (term_smtcoq_atom b))
       | Some (n, [a]) when n == H.uminus_Int ->
-        Atom (Atom.mk_opp ra (term_smtcoq_atom a))
+        Form.Atom (Atom.mk_opp ra (term_smtcoq_atom a))
       | Some (n, _) ->
         Format.eprintf "\nTerm: %a\n@." print_term t;
         failwith ("LFSC function symbol "^Hstring.view n^" not supported.")
@@ -416,7 +418,7 @@ and term_smtcoq t =
 
 
 and term_smtcoq_atom a = match term_smtcoq a with
-  | Atom h -> h
+  | Form.Atom h -> h
   | _ ->  assert false
 
 and args_smtcoq args =
@@ -428,21 +430,21 @@ and uncurry acc t = match app_name t, acc with
     uncurry (term_smtcoq_atom a :: acc) f
   | Some (n, [_; _]) , [h1; h2] when n == H.read ->
     (match Atom.type_of h1 with
-     | TFArray (ti,te) -> Atom (Atom.mk_select ra ti te h1 h2)
+     | TFArray (ti,te) -> Form.Atom (Atom.mk_select ra ti te h1 h2)
      | _ -> assert false)
   | Some (n, [_; _]) , [h1; h2; h3] when n == H.write ->
     (match Atom.type_of h1 with
-     | TFArray (ti,te) -> Atom (Atom.mk_store ra ti te h1 h2 h3)
+     | TFArray (ti,te) -> Form.Atom (Atom.mk_store ra ti te h1 h2 h3)
      | _ -> assert false)
   | Some (n, [_; _]) , [h1; h2] when n == H.diff ->
     (match Atom.type_of h1 with
-     | TFArray (ti,te) -> Atom (Atom.mk_diffarray ra ti te h1 h2)
+     | TFArray (ti,te) -> Form.Atom (Atom.mk_diffarray ra ti te h1 h2)
      | _ -> assert false)
   | None, _ ->
     (match name t with
      | Some n ->
        let args = Array.of_list acc in
-       Atom (Atom.get ra (Aapp (get_fun (Hstring.view n), args)))
+       Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun (Hstring.view n), args)))
      | _ -> assert false)
   | _ ->
     eprintf "uncurry fail: %a@." Ast.print_term t;
@@ -484,7 +486,7 @@ let to_clause = clause_smtcoq []
 
 let print_clause fmt cl =
   fprintf fmt "(";
-  List.iter (fprintf fmt "%a " (Form.to_smt Atom.to_smt)) cl;
+  List.iter (fprintf fmt "%a " (Form.to_smt ~debug:false)) cl;
   fprintf fmt ")"
 
 
@@ -581,6 +583,8 @@ let register_decl_id name id =
 
 
 let clear () =
+  Atom.clear ra;
+  Form.clear rf;
   HCl.clear clauses_ids;
   Hashtbl.clear ids_clauses;
   HT.clear propvars;
diff --git a/src/lfsc/tosmtcoq.mli b/src/lfsc/tosmtcoq.mli
index b0d980b..34d3119 100644
--- a/src/lfsc/tosmtcoq.mli
+++ b/src/lfsc/tosmtcoq.mli
@@ -11,3 +11,6 @@
 
 
 include Translator_sig.S
+
+val ra : SmtAtom.Atom.reify_tbl
+val rf : SmtAtom.Form.reify
diff --git a/src/lfsc/translator_sig.mli b/src/lfsc/translator_sig.mli
index 66005f3..0937aef 100644
--- a/src/lfsc/translator_sig.mli
+++ b/src/lfsc/translator_sig.mli
@@ -19,7 +19,7 @@ open Ast
 open Format
 
 
-(** The type of destination rules that are currently supported byt the
+(** The type of destination rules that are currently supported by the
     converter *)
 type rule =
   | Reso