track assumptions when parsing into a solver. This enables solver.fro…

…m_file/solver.from_string to support assumptions/cores #6587

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/api/api_parsers.cpp

@@ -128,7 +128,8 @@ extern "C" {
 
     static Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr<cmd_context>& ctx, bool owned, std::istream& is) {
         Z3_TRY;
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        ast_manager& m = mk_c(c)->m();
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m);        
         mk_c(c)->save_object(v);        
         std::stringstream errstrm;
         ctx->set_regular_stream(errstrm);
@@ -147,8 +148,11 @@ extern "C" {
             SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
             return of_ast_vector(v);
         }
-        for (expr* e : ctx->tracked_assertions()) 
-            v->m_ast_vector.push_back(e);
+        for (auto const& [asr, an] : ctx->tracked_assertions())
+            if (an)
+                v->m_ast_vector.push_back(m.mk_implies(an, asr));
+            else
+                v->m_ast_vector.push_back(asr);
         ctx->reset_tracked_assertions();        
         return of_ast_vector(v);
         Z3_CATCH_RETURN(nullptr);        

src/api/api_solver.cpp

@@ -314,8 +314,11 @@ extern "C" {
         bool initialized = to_solver(s)->m_solver.get() != nullptr;
         if (!initialized)
             init_solver(c, s);
-        for (expr* e : ctx->tracked_assertions()) 
-            to_solver(s)->assert_expr(e);
+        for (auto const& [asr, an] : ctx->tracked_assertions())
+            if (an)
+                to_solver(s)->assert_expr(asr, an);
+            else
+                to_solver(s)->assert_expr(asr);
         ctx->reset_tracked_assertions();
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
         auto* ctx_s = ctx->get_solver();

src/cmd_context/cmd_context.cpp

@@ -2201,21 +2201,18 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
 }
 
 
-expr_ref_vector cmd_context::tracked_assertions() {
-    expr_ref_vector result(m());
+vector<std::pair<expr*,expr*>> cmd_context::tracked_assertions() {
+    vector<std::pair<expr*,expr*>> result;
     if (assertion_names().size() == assertions().size()) {
         for (unsigned i = 0; i < assertions().size(); ++i) {
             expr* an  = assertion_names()[i];
             expr* asr = assertions()[i];
-            if (an) 
-                result.push_back(m().mk_implies(an, asr));
-            else 
-                result.push_back(asr);
+            result.push_back({ asr, an });
         }
     }
     else {
         for (expr * e : assertions()) 
-            result.push_back(e);
+            result.push_back({ e, nullptr});
     }
     return result;
 }

src/cmd_context/cmd_context.h

@@ -523,7 +523,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
 
     ptr_vector<expr> const& assertions() const { return m_assertions; }
     ptr_vector<expr> const& assertion_names() const { return m_assertion_names; }
-    expr_ref_vector tracked_assertions();
+    vector<std::pair<expr*,expr*>> tracked_assertions();
     void reset_tracked_assertions();
 
     /**