From 46a96127bef61e5fa00153e11e7852a5139bf98b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Nov 2017 18:37:20 -0800
Subject: [PATCH] add solver_from_string to APIs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp   | 60 ++++++++++++++++++++++++----------------
 src/api/dotnet/Solver.cs |  8 ++++++
 src/api/java/Solver.java | 17 ++++++++++++
 src/api/python/z3/z3.py  |  2 +-
 src/api/z3_api.h         |  7 +++++
 5 files changed, 69 insertions(+), 25 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 2455d3a81..8c2cbf25e 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -128,30 +128,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) {
-        Z3_TRY;
-        LOG_Z3_solver_from_file(c, s, file_name);
-        char const* ext = get_extension(file_name);
-        std::ifstream is(file_name);
-        if (!is) {
-            SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
-            return;
-        }
-        if (ext && std::string("dimacs") == ext) {
-            ast_manager& m = to_solver_ref(s)->get_manager();
-            sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
-            parse_dimacs(is, solver);
-            sat2goal s2g;
-            model_converter_ref mc;
-            atom2bool_var a2b(m);
-            goal g(m);            
-            s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
-            for (unsigned i = 0; i < g.size(); ++i) {
-                to_solver_ref(s)->assert_expr(g.form(i));
-            }
-            return;
-        }
-
+    void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {
         scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
         ctx->set_ignore_check(true);
 
@@ -170,6 +147,41 @@ extern "C" {
             to_solver_ref(s)->assert_expr(*it);
         }
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
+    }
+
+    void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) {
+        Z3_TRY;
+        LOG_Z3_solver_from_string(c, s, c_str);
+        std::string str(c_str);
+        std::istringstream is(str);
+        solver_from_stream(c, s, is);
+        Z3_CATCH;        
+    }
+
+    void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) {
+        Z3_TRY;
+        LOG_Z3_solver_from_file(c, s, file_name);
+        char const* ext = get_extension(file_name);
+        std::ifstream is(file_name);
+        if (!is) {
+            SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
+        }
+        else if (ext && std::string("dimacs") == ext) {
+            ast_manager& m = to_solver_ref(s)->get_manager();
+            sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
+            parse_dimacs(is, solver);
+            sat2goal s2g;
+            model_converter_ref mc;
+            atom2bool_var a2b(m);
+            goal g(m);            
+            s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
+            for (unsigned i = 0; i < g.size(); ++i) {
+                to_solver_ref(s)->assert_expr(g.form(i));
+            }
+        }
+        else {
+            solver_from_stream(c, s, is);
+        }
         Z3_CATCH;
     }
 
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index e310f938c..af5f8e47e 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -231,6 +231,14 @@ namespace Microsoft.Z3
 	     Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);	
 	}
 
+	/// <summary>
+	/// Load solver assertions from a string.
+	/// </summary>
+	public void FromString(string str) 
+        {
+	     Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);	
+	}
+
         /// <summary>
         /// Assert a lemma (or multiple) into the solver.
         /// </summary>        
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 19f3b01da..8eb634e23 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -170,6 +170,23 @@ public class Solver extends Z3Object {
                 constraint.getNativeObject(), p.getNativeObject());
     }
 
+    /// <summary>
+    /// Load solver assertions from a file.
+    /// </summary>
+    public void FromFile(string file) 
+    {
+        Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);	
+    }
+
+    /// <summary>
+    /// Load solver assertions from a string.
+    /// </summary>
+    public void FromString(string str) 
+    {
+        Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);	
+    }
+
+
     /**
      * The number of assertions in the solver.
      * 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index f911732ef..9819af47f 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6335,7 +6335,7 @@ class Solver(Z3PPObject):
 
     def from_string(self, s):
         """Parse assertions from a string"""
-        self.add([f for f in parse_smt2_string(s, ctx=self.ctx)])
+        Z3_solver_from_string(self.ctx.ref(), self.solver, filename)
         
     def assertions(self):
         """Return an AST vector containing all added constraints.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index c9603c018..7f92501ec 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6152,6 +6152,13 @@ extern "C" {
     */
     void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
 
+    /**
+       \brief load solver assertions from a string.
+
+       def_API('Z3_solver_from_string', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING)))
+    */
+    void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name);
+
     /**
        \brief Return the set of asserted formulas on the solver.