From 37f297b89f04155124237acf3d7f220a9dcd1544 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 2 Mar 2016 17:31:47 +0100
Subject: Code refactoring

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

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

diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index f11d650..533f139 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -224,3 +224,16 @@ let declare_commands rt ro ra rf acc = function
     let _ = declare_fun rt ro sym arg cod in acc
   | CAssert (_, t) -> (make_root ra rf t)::acc
   | _ -> acc
+
+
+(* Import function *)
+
+let import_smtlib2 rt ro ra rf filename =
+  let chan = open_in filename in
+  let lexbuf = Lexing.from_channel chan in
+  let commands = Smtlib2_parse.main Smtlib2_lex.token lexbuf in
+  close_in chan;
+  match commands with
+    | None -> []
+    | Some (Smtlib2_ast.Commands (_,(_,res))) ->
+      List.rev (List.fold_left (declare_commands rt ro ra rf) [] res)
-- 
cgit