Made SmtCommands independent from VeritSyntax

Made lfsc/* mostly independent from VeritSyntax

4 files changed, 53 insertions, 104 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 57fd0cc..17a230f 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -104,6 +104,7 @@ let import_trace ra' rf' filename first lsmt =
 
 let clear_all () =
   SmtTrace.clear ();
+  SmtMaps.clear ();
   VeritSyntax.clear ()
 
 
@@ -145,13 +146,13 @@ let export out_channel rt ro lsmt =
 
   List.iter (fun (i,t) ->
     let s = "Tindex_"^(string_of_int i) in
-    VeritSyntax.add_btype s (Tindex t);
+    SmtMaps.add_btype s (Tindex t);
     Format.fprintf fmt "(declare-sort %s 0)@." s
   ) (SmtBtype.to_list rt);
 
   List.iter (fun (i,dom,cod,op) ->
     let s = "op_"^(string_of_int i) in
-    VeritSyntax.add_fun s op;
+    SmtMaps.add_fun s op;
     Format.fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
     Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) dom;
@@ -161,7 +162,7 @@ let export out_channel rt ro lsmt =
   ) (Op.to_list ro);
 
   List.iter (fun u -> Format.fprintf fmt "(assert ";
-                      Form.to_smt Atom.to_smt fmt u;
+                      Form.to_smt fmt u;
                       Format.fprintf fmt ")\n") lsmt;
 
   Format.fprintf fmt "(check-sat)\n(exit)@."
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 65eb6b7..08c5cb3 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -175,7 +175,7 @@ lit_list:
 ;
 
 lit:   /* returns a SmtAtom.Form.t option */
-  | name_term                                              { let decl, t = $1 in decl, lit_of_atom_form_lit rf (decl, t) }
+  | name_term                                              { let decl, t = $1 in decl, Form.lit_of_atom_form_lit rf (decl, t) }
   | LPAR NOT lit RPAR                                      { apply_dec Form.neg $3 }
 ;
 
@@ -191,15 +191,15 @@ var_atvar:
 name_term:   /* returns a bool * (SmtAtom.Form.pform or a SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | SHARPINT                                              { get_solver $1 }
   | SHARPINT COLON LPAR term RPAR                         { let res = $4 in add_solver $1 res; res }
-  | BITV                                                   { true, Atom (Atom.mk_bvconst ra (parse_bv $1)) }
-  | TRUE                                                   { true, Form Form.pform_true }
-  | FALS                                                   { true, Form Form.pform_false }
+  | BITV                                                   { true, Form.Atom (Atom.mk_bvconst ra (parse_bv $1)) }
+  | TRUE                                                   { true, Form.Form Form.pform_true }
+  | FALS                                                   { true, Form.Form Form.pform_false }
   | var_atvar						   { let x = $1 in match find_opt_qvar x with
-    					                   | Some bt -> false, Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
-							   | None -> true, Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
+    					                   | Some bt -> false, Form.Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
+							   | None -> true, Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun $1, [||]))) }
   | BINDVAR                                                { true, Hashtbl.find hlets $1 }
-  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | INT                                                    { true, Form.Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Form.Atom (Atom.hatom_Z_of_bigint ra $1) }
 ;
 
 tvar:
@@ -214,27 +214,27 @@ var_decl_list:
 ;
 
 forall_decl:
-  | FORALL LPAR var_decl_list RPAR blit		   { clear_qvar (); false, Form (Fapp (Fforall $3, [|lit_of_atom_form_lit rf $5|])) }
+  | FORALL LPAR var_decl_list RPAR blit		   { clear_qvar (); false, Form.Form (Fapp (Fforall $3, [|Form.lit_of_atom_form_lit rf $5|])) }
 ; 
 
 term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean indicates if we should declare the term or not */
   | LPAR term RPAR                                         { $2 }
 
   /* Formulae */
-  | TRUE                                                   { true, Form Form.pform_true }
-  | FALS                                                   { true, Form Form.pform_false }
-  | AND lit_list                                           { apply_dec (fun x -> Form (Fapp (Fand, Array.of_list x))) (list_dec $2) }
-  | OR lit_list                                            { apply_dec (fun x -> Form (Fapp (For, Array.of_list x))) (list_dec $2) }
-  | IMP lit_list                                           { apply_dec (fun x -> Form (Fapp (Fimp, Array.of_list x))) (list_dec $2) }
-  | XOR lit_list                                           { apply_dec (fun x -> Form (Fapp (Fxor, Array.of_list x))) (list_dec $2) }
-  | ITE lit_list                                           { apply_dec (fun x -> Form (Fapp (Fite, Array.of_list x))) (list_dec $2) }
+  | TRUE                                                   { true, Form.Form Form.pform_true }
+  | FALS                                                   { true, Form.Form Form.pform_false }
+  | AND lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fand, Array.of_list x))) (list_dec $2) }
+  | OR lit_list                                            { apply_dec (fun x -> Form.Form (Fapp (For, Array.of_list x))) (list_dec $2) }
+  | IMP lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fimp, Array.of_list x))) (list_dec $2) }
+  | XOR lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fxor, Array.of_list x))) (list_dec $2) }
+  | ITE lit_list                                           { apply_dec (fun x -> Form.Form (Fapp (Fite, Array.of_list x))) (list_dec $2) }
   | forall_decl                                            { $1 }
-  | BBT name_term LBRACKET lit_list RBRACKET               { let (decl, t) = $2 in let (decll, l) = list_dec $4 in (decl && decll, match t with | Atom a -> Form (FbbT (a, l)) | _ -> assert false) }
+  | BBT name_term LBRACKET lit_list RBRACKET               { let (decl, t) = $2 in let (decll, l) = list_dec $4 in (decl && decll, match t with | Form.Atom a -> Form.Form (FbbT (a, l)) | _ -> assert false) }
 
   /* Atoms */
-  | INT                                                    { true, Atom (Atom.hatom_Z_of_int ra $1) }
-  | BIGINT                                                 { true, Atom (Atom.hatom_Z_of_bigint ra $1) }
-  | BITV                                                   { true, Atom (Atom.mk_bvconst ra (parse_bv $1)) }
+  | INT                                                    { true, Form.Atom (Atom.hatom_Z_of_int ra $1) }
+  | BIGINT                                                 { true, Form.Atom (Atom.hatom_Z_of_bigint ra $1) }
+  | BITV                                                   { true, Form.Atom (Atom.mk_bvconst ra (parse_bv $1)) }
   | LT name_term name_term                                 { apply_bdec_atom (Atom.mk_lt ra) $2 $3 }
   | LEQ name_term name_term                                { apply_bdec_atom (Atom.mk_le ra) $2 $3 }
   | GT name_term name_term                                 { apply_bdec_atom (Atom.mk_gt ra) $2 $3 }
@@ -246,7 +246,7 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | OPP name_term                                          { apply_dec_atom (Atom.mk_opp ra) $2 }
   | DIST args                                              { let da, la = list_dec $2 in
     	 						     let a = Array.of_list la in
-                                                             da, Atom (Atom.mk_distinct ra ~declare:da (Atom.type_of a.(0)) a) }
+                                                             da, Form.Atom (Atom.mk_distinct ra ~declare:da (Atom.type_of a.(0)) a) }
   | BITOF INT name_term                                    { apply_dec_atom (fun ?declare:(d=true) h -> match Atom.type_of h with TBV s -> Atom.mk_bitof ra ~declare:d s $2 h | _ -> assert false) $3 }
   | BVNOT name_term                                        { apply_dec_atom (fun ?declare:(d=true) h -> match Atom.type_of h with TBV s -> Atom.mk_bvnot ra ~declare:d s h | _ -> assert false) $2 }
   | BVAND name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvand ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
@@ -257,8 +257,8 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | BVMUL name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvmult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVULT name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVSLT name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvslt ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
-  | BVULE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Lit (Form.neg (lit_of_atom_form_lit rf a))) }
-  | BVSLE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvslt ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Lit (Form.neg (lit_of_atom_form_lit rf a))) }
+  | BVULE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvult ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Form.Lit (Form.neg (Form.lit_of_atom_form_lit rf a))) }
+  | BVSLE name_term name_term                              { let (decl,_) as a = apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvslt ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 in (decl, Form.Lit (Form.neg (Form.lit_of_atom_form_lit rf a))) }
   | BVSHL name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvshl ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVSHR name_term name_term                              { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TBV s -> Atom.mk_bvshr ra ~declare:d s h1 h2 | _ -> assert false) $2 $3 }
   | BVCONC name_term name_term                             { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1, Atom.type_of h2 with TBV s1, TBV s2 -> Atom.mk_bvconcat ra ~declare:d s1 s2 h1 h2 | _, _ -> assert false) $2 $3 }
@@ -268,26 +268,20 @@ term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i
   | SELECT name_term name_term                             { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TFArray (ti, te) -> Atom.mk_select ra ~declare:d ti te h1 h2 | _ -> assert false) $2 $3 }
   | DIFF name_term name_term                               { apply_bdec_atom (fun ?declare:(d=true) h1 h2 -> match Atom.type_of h1 with TFArray (ti, te) -> Atom.mk_diffarray ra ~declare:d ti te h1 h2 | _ -> assert false) $2 $3 }
   | STORE name_term name_term name_term                    { apply_tdec_atom (fun ?declare:(d=true) h1 h2 h3 -> match Atom.type_of h1 with TFArray (ti, te) -> Atom.mk_store ra ~declare:d ti te h1 h2 h3 | _ -> assert false) $2 $3 $4 }
-  | VAR                                                    { let x = $1 in match find_opt_qvar x with
-    							                     | Some bt -> false, Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||])))
-                                                                             | None -> true, Atom (Atom.get ra (Aapp (get_fun $1, [||]))) }
-  | VAR args                                               { let f = $1 in let a = $2 in match find_opt_qvar f with
-    							                                   | Some bt -> let op = dummy_indexed_op (Rel_name f) [||] bt in
-							       	       	                                false, Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a)))))
-      							                                   | None -> let dl, l = list_dec $2 in
-                                                                                                     dl, Atom (Atom.get ra ~declare:dl (Aapp (get_fun f, Array.of_list l))) }
+  | VAR                                                    { let x = $1 in match find_opt_qvar x with | Some bt -> false, Form.Atom (Atom.get ~declare:false ra (Aapp (dummy_indexed_op (Rel_name x) [||] bt, [||]))) | None -> true, Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun $1, [||]))) }
+  | VAR args                                               { let f = $1 in let a = $2 in match find_opt_qvar f with | Some bt -> let op = dummy_indexed_op (Rel_name f) [||] bt in false, Form.Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a))))) | None -> let dl, l = list_dec $2 in dl, Form.Atom (Atom.get ra ~declare:dl (Aapp (SmtMaps.get_fun f, Array.of_list l))) }
 
   /* Both */
-  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Atom h1), (decl2, Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Atom (Atom.mk_eq ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|lit_of_atom_form_lit rf (decl1, t1); lit_of_atom_form_lit rf (decl2, t2)|])) }
-  | EQ nlit lit                                            { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|t1; t2|])) }
-  | EQ name_term nlit                                      { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form (Fapp (Fiff, [|lit_of_atom_form_lit rf (decl1, t1); t2|])) }
+  | EQ name_term name_term                                 { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Form.Atom h1), (decl2, Form.Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Form.Atom (Atom.mk_eq ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); Form.lit_of_atom_form_lit rf (decl2, t2)|])) }
+  | EQ nlit lit                                            { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|t1; t2|])) }
+  | EQ name_term nlit                                      { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); t2|])) }
   | LET LPAR bindlist RPAR name_term                       { $3; $5 }
   | BINDVAR                                                { true, Hashtbl.find hlets $1 }
 ;
 
 blit:
   | name_term                                              { $1 }
-  | LPAR NOT lit RPAR                                      { apply_dec (fun l -> Lit (Form.neg l)) $3 }
+  | LPAR NOT lit RPAR                                      { apply_dec (fun l -> Form.Lit (Form.neg l)) $3 }
 ;
 
 bindlist:
@@ -295,8 +289,8 @@ bindlist:
   | LPAR BINDVAR blit RPAR bindlist                        { Hashtbl.add hlets $2 (snd $3); $5 }
 
 args:
-  | name_term                                              { match $1 with decl, Atom h -> [decl, h] | _ -> assert false }
-  | name_term args                                         { match $1 with decl, Atom h -> (decl, h)::$2 | _ -> assert false }
+  | name_term                                              { match $1 with decl, Form.Atom h -> [decl, h] | _ -> assert false }
+  | name_term args                                         { match $1 with decl, Form.Atom h -> (decl, h)::$2 | _ -> assert false }
 ;
 
 clause_ids_params:
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 6b26f65..b1a6304 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -496,20 +496,6 @@ let mk_clause cl =
     Structures.error ("SMTCoq was not able to check the certificate \
                        for the following reason.\n"^f)
 
-type atom_form_lit =
-  | Atom of SmtAtom.Atom.t
-  | Form of SmtAtom.Form.pform
-  | Lit of SmtAtom.Form.t
-
-(* functions for applying on a pair with a boolean when the boolean indicates
-   if the entire term should be declared in the tables *)
-let lit_of_atom_form_lit rf = function
-  | decl, Atom a -> Form.get ~declare:decl rf (Fatom a)
-  | decl, Form f -> begin match f with
-                    | Fapp (Fforall _, _) when decl -> failwith "decl is true on a forall"
-                    | _ -> Form.get ~declare:decl rf f end
-  | decl, Lit l -> l
-
 let apply_dec f (decl, a) = decl, f a
 
 let rec list_dec = function
@@ -519,54 +505,37 @@ let rec list_dec = function
      decl_h && decl_t, h :: l_t
 
 let apply_dec_atom (f:?declare:bool -> SmtAtom.hatom -> SmtAtom.hatom) = function
-  | decl, Atom h -> decl, Atom (f ~declare:decl h)
+  | decl, Form.Atom h -> decl, Form.Atom (f ~declare:decl h)
   | _ -> assert false
 
 let apply_bdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 =
   match o1, o2 with
-  | (decl1, Atom h1), (decl2, Atom h2) ->
+  | (decl1, Form.Atom h1), (decl2, Form.Atom h2) ->
      let decl = decl1 && decl2 in
-     decl, Atom (f ~declare:decl h1 h2)
+     decl, Form.Atom (f ~declare:decl h1 h2)
   | _ -> assert false
 
 let apply_tdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 o3 =
   match o1, o2, o3 with
-  | (decl1, Atom h1), (decl2, Atom h2), (decl3, Atom h3) ->
+  | (decl1, Form.Atom h1), (decl2, Form.Atom h2), (decl3, Form.Atom h3) ->
      let decl = decl1 && decl2 && decl3 in
-     decl, Atom (f ~declare:decl h1 h2 h3)
+     decl, Form.Atom (f ~declare:decl h1 h2 h3)
   | _ -> assert false
 
 
-let solver : (int, (bool * atom_form_lit)) Hashtbl.t = Hashtbl.create 17
+let solver : (int, (bool * Form.atom_form_lit)) Hashtbl.t = Hashtbl.create 17
 let get_solver id =
   try Hashtbl.find solver id
   with | Not_found -> failwith ("VeritSyntax.get_solver : solver variable number "^(string_of_int id)^" not found\n")
 let add_solver id cl = Hashtbl.add solver id cl
 let clear_solver () = Hashtbl.clear solver
 
-let btypes : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 17
-let get_btype id =
-  try Hashtbl.find btypes id
-  with | Not_found -> failwith ("VeritSyntax.get_btype : sort symbol \""^id^"\" not found\n")
-let add_btype id cl = Hashtbl.add btypes id cl
-let clear_btypes () = Hashtbl.clear btypes
-
-let funs : (string,indexed_op) Hashtbl.t = Hashtbl.create 17
-let get_fun id =
-  try Hashtbl.find funs id
-  with | Not_found -> failwith ("VeritSyntax.get_fun : function symbol \""^id^"\" not found\n")
-let add_fun id cl = Hashtbl.add funs id cl
-let remove_fun id = Hashtbl.remove funs id
-let clear_funs () = Hashtbl.clear funs
-
 let qvar_tbl : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 10
 let find_opt_qvar s = try Some (Hashtbl.find qvar_tbl s)
                       with Not_found -> None
 let add_qvar s bt = Hashtbl.add qvar_tbl s bt
 let clear_qvar () = Hashtbl.clear qvar_tbl
 
-let hform_to_smt = Form.to_smt ~pi:true Atom.to_smt
-
 (* Finding the index of a root in <lsmt> modulo the <re_hash> function.
    This function is used by SmtTrace.order_roots *)
 let init_index lsmt re_hash =
@@ -583,8 +552,8 @@ let init_index lsmt re_hash =
             with Not_found ->
               let oc = open_out "/tmp/input_not_found.log" in
               let fmt = Format.formatter_of_out_channel oc in
-              List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt (re_hash h)) lsmt;
-              Format.fprintf fmt "\n%a\n@." hform_to_smt re_hf;
+              List.iter (fun h -> Format.fprintf fmt "%a\n" (Form.to_smt ~debug:true) (re_hash h)) lsmt;
+              Format.fprintf fmt "\n%a\n@." (Form.to_smt ~debug:true) re_hf;
               flush oc; close_out oc;
               failwith "not found: log available"
 
@@ -604,7 +573,7 @@ let rf = Form.create ()
 let ra' = Atom.create ()
 let rf' = Form.create ()
 
-let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
+let hlets : (string, Form.atom_form_lit) Hashtbl.t = Hashtbl.create 17
 
 let clear_mk_clause () =
   to_add := [];
@@ -615,8 +584,6 @@ let clear () =
   clear_mk_clause ();
   clear_clauses ();
   clear_solver ();
-  clear_btypes ();
-  clear_funs ();
   Atom.clear ra;
   Form.clear rf;
   Atom.clear ra';
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index fd39052..7a325a6 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -10,6 +10,8 @@
 (**************************************************************************)
 
 
+open SmtAtom
+
 exception Sat
 
 type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | Weak | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp | Flat | Hole | Bbva | Bbconst | Bbeq | Bbdis | Bbop | Bbadd | Bbmul | Bbult | Bbslt | Bbnot | Bbneg | Bbconc | Bbextr | Bbzext | Bbsext | Bbshl | Bbshr | Row1 | Row2 | Exte
@@ -23,51 +25,36 @@ val to_add : (int * SmtAtom.Form.t list) list ref
 
 val mk_clause : SmtCertif.clause_id * typ * SmtAtom.Form.t list * SmtCertif.clause_id list -> SmtCertif.clause_id
 
-type atom_form_lit =
-  | Atom of SmtAtom.Atom.t
-  | Form of SmtAtom.Form.pform
-  | Lit of SmtAtom.Form.t
-val lit_of_atom_form_lit : SmtAtom.Form.reify -> bool * atom_form_lit -> SmtAtom.Form.t
-
 val apply_dec_atom : (?declare:bool -> SmtAtom.hatom -> SmtAtom.hatom) ->
-                     bool * atom_form_lit -> bool * atom_form_lit
+                     bool * Form.atom_form_lit -> bool * Form.atom_form_lit
 val apply_bdec_atom :
   (?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) ->
-  bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit
+  bool * Form.atom_form_lit -> bool * Form.atom_form_lit -> bool * Form.atom_form_lit
 val apply_tdec_atom :
   (?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) ->
-  bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit
+  bool * Form.atom_form_lit -> bool * Form.atom_form_lit -> bool * Form.atom_form_lit -> bool * Form.atom_form_lit
 
 val apply_dec : ('a -> 'b) -> bool * 'a -> bool * 'b
 val list_dec : (bool * 'a) list -> bool * 'a list
 
 
-val get_solver : int -> bool * atom_form_lit
-val add_solver : int -> bool * atom_form_lit -> unit
-
-val get_btype : string -> SmtBtype.btype
-val add_btype : string -> SmtBtype.btype -> unit
-
-val get_fun : string -> SmtAtom.indexed_op
-val add_fun : string -> SmtAtom.indexed_op -> unit
-val remove_fun : string -> unit
+val get_solver : int -> bool * Form.atom_form_lit
+val add_solver : int -> bool * Form.atom_form_lit -> unit
 
 val find_opt_qvar : string -> SmtBtype.btype option 
 val add_qvar : string -> SmtBtype.btype -> unit
 val clear_qvar : unit -> unit
 
-val hform_to_smt : Format.formatter -> SmtAtom.Form.t -> unit
-
 val init_index : SmtAtom.Form.t list -> (SmtAtom.Form.t -> SmtAtom.Form.t) ->
                  SmtAtom.Form.t -> int
 
 val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCertif.clause_kind * SmtAtom.Form.t list option * SmtAtom.Form.t SmtCertif.clause) list
-                                     
+
 val ra : SmtAtom.Atom.reify_tbl
 val rf : SmtAtom.Form.reify
 val ra' : SmtAtom.Atom.reify_tbl
 val rf' : SmtAtom.Form.reify
 
-val hlets : (string, atom_form_lit) Hashtbl.t
+val hlets : (string, Form.atom_form_lit) Hashtbl.t
 
 val clear : unit -> unit