From d35b057995b4940af0e66bb081b3fe3ac7ff97f3 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 25 Sep 2019 18:22:53 +0200
Subject: Made SmtCommands independent from VeritSyntax Made lfsc/* mostly
 independent from VeritSyntax

---
 src/smtlib2/smtlib2_genConstr.ml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'src/smtlib2/smtlib2_genConstr.ml')

diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 64f0b20..f938671 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -45,7 +45,7 @@ let string_type s =
   | "Array" -> (function [ti;te] -> TFArray (ti, te) | _ -> assert false)
   | _ ->
     try Scanf.sscanf s "BitVec_%d%!" (fun size -> fun _ -> TBV size)
-    with _ -> fun _ -> VeritSyntax.get_btype s
+    with _ -> fun _ -> SmtMaps.get_btype s
 
 let sort_of_string s = string_type s
 
@@ -96,30 +96,33 @@ let rec sort_of_sort = function
     sort_of_string (string_of_identifier id) (List.map sort_of_sort l)
 
 
-let declare_sort rt sym =
-  let s = string_of_symbol sym in
+let declare_sort_from_name rt s =
   let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in
   let compdec_type = mklApp cCompDec [| cons_t |] in
   let compdec_var =
     Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in
   let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in
   let res = SmtBtype.declare rt cons_t ce in
-  VeritSyntax.add_btype s res;
+  SmtMaps.add_btype s res;
   res
 
+let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
 
-let declare_fun rt ro sym arg cod =
-  let s = string_of_symbol sym in
-  let tyl = List.map sort_of_sort arg in
-  let ty = sort_of_sort cod in
+
+let declare_fun_from_name rt ro s tyl ty =
   let coqTy = List.fold_right (fun typ c ->
       Term.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
   let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
-  VeritSyntax.add_fun s op;
+  SmtMaps.add_fun s op;
   op
 
+let declare_fun rt ro sym arg cod =
+  let tyl = List.map sort_of_sort arg in
+  let ty = sort_of_sort cod in
+  declare_fun_from_name rt ro (string_of_symbol sym) tyl ty
+
 
 
 let parse_smt2bv s =
@@ -405,7 +408,7 @@ let make_root ra rf t =
          with _ -> assert false)
 
       | _, _ ->
-        let op = VeritSyntax.get_fun v in
+        let op = SmtMaps.get_fun v in
         let l' = List.map (fun t ->
             match make_root_term t with
             | Atom h -> h | Form _ -> assert false) l in
-- 
cgit