add direct FromFile method to solvers so that model transformations are loaded along with assertions.

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_solver.cpp

@@ -33,6 +33,9 @@ Revision History:
 #include "smt/smt_solver.h"
 #include "smt/smt_implied_equalities.h"
 #include "solver/smt_logics.h"
+#include "cmd_context/cmd_context.h"
+#include "parsers/smt2/smt2parser.h"
+
 
 extern "C" {
 
@@ -121,6 +124,30 @@ 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);
+        scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
+        ctx->set_ignore_check(true);
+        std::ifstream is(file_name);
+        if (!is) {
+            SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
+            return;
+        }
+        if (!parse_smt2_commands(*ctx.get(), is)) {
+            ctx = nullptr;
+            SET_ERROR_CODE(Z3_PARSER_ERROR);
+            return;
+        }
+        ptr_vector<expr>::const_iterator it  = ctx->begin_assertions();
+        ptr_vector<expr>::const_iterator end = ctx->end_assertions();
+        for (; it != end; ++it) {
+            to_solver_ref(s)->assert_expr(*it);
+        }
+        to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
+        Z3_CATCH;
+    }
+
     Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {
         Z3_TRY;
         LOG_Z3_solver_get_help(c, s);

src/api/dotnet/Solver.cs

@@ -181,6 +181,14 @@ namespace Microsoft.Z3
             Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
         }
 
+	/// <summary>
+	/// Load solver assertions from a file.
+	/// </summary>
+	public void FromFile(string file) 
+        {
+	     Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);	
+	}
+
         /// <summary>
         /// Assert a lemma (or multiple) into the solver.
         /// </summary>        

src/api/python/z3/z3.py

@@ -6300,7 +6300,7 @@ class Solver(Z3PPObject):
 
     def from_file(self, filename):
         """Parse assertions from a file"""
-        self.add([f for f in parse_smt2_file(filename, ctx=self.ctx)])
+        Z3_solver_from_file(self.ctx.ref(), self.solver)
 
     def from_string(self, s):
         """Parse assertions from a string"""

src/api/z3_api.h

@@ -6137,6 +6137,13 @@ extern "C" {
      */
     void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a);
 
+    /**
+       \brief load solver assertions from a file.
+
+       def_API('Z3_solver_from_file', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING)))
+    */
+    void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
+
     /**
        \brief Return the set of asserted formulas on the solver.
 

src/cmd_context/cmd_context.h

@@ -443,6 +443,8 @@ public:
 
     dictionary<macro_decls> const & get_macros() const { return m_macros; }
 
+    model_converter* get_model_converter() { return m_mc0.get(); }
+
     bool is_model_available() const;
 
     double get_seconds() const { return m_watch.get_seconds(); }

src/sat/tactic/goal2sat.cpp

@@ -882,10 +882,6 @@ struct sat2goal::imp {
     // Wrapper for sat::model_converter: converts it into an "AST level" model_converter.
     class sat_model_converter : public model_converter {
         sat::model_converter        m_mc;
-        // TODO: the following mapping is storing a lot of useless information, and may be a performance bottleneck.
-        // We need to save only the expressions associated with variables that occur in m_mc.
-        // This information may be stored as a vector of pairs.
-        // The mapping is only created during the model conversion.
         expr_ref_vector             m_var2expr;
         filter_model_converter_ref  m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion