From 092c25d5963a0d645b8df7064f5254efd18ee9e9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Dec 2018 18:37:30 -0800
Subject: [PATCH] fix #2007
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_ast.cpp | 3 +++
src/api/api_context.h | 21 +++++++++++++++++++++
src/api/api_model.cpp | 5 ++++-
src/cmd_context/cmd_context.h | 21 +++++++++++++++++++++
src/cmd_context/eval_cmd.cpp | 1 +
src/cmd_context/simplify_cmd.cpp | 19 -------------------
src/model/model.cpp | 4 ++++
src/model/model.h | 1 +
src/model/model_evaluator.cpp | 4 ++++
src/model/model_evaluator.h | 3 +++
10 files changed, 62 insertions(+), 20 deletions(-)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index d10da60db..eeb85687d 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -34,6 +34,7 @@ Revision History:
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/recfun_replace.h"
+#include "ast/rewriter/seq_rewriter.h"
#include "ast/pp.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
@@ -733,6 +734,7 @@ extern "C" {
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
+
static Z3_ast simplify(Z3_context c, Z3_ast _a, Z3_params _p) {
Z3_TRY;
RESET_ERROR_CODE();
@@ -742,6 +744,7 @@ extern "C" {
unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = p.get_bool("ctrl_c", false);
th_rewriter m_rw(m, p);
+ m_rw.set_solver(alloc(api::seq_expr_solver, m, p));
expr_ref result(m);
cancel_eh<reslimit> eh(m.limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
diff --git a/src/api/api_context.h b/src/api/api_context.h
index a6b8600d6..aacd4edd3 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -38,6 +38,9 @@ Revision History:
#include "cmd_context/cmd_context.h"
#include "api/api_polynomial.h"
#include "util/hashtable.h"
+#include "ast/rewriter/seq_rewriter.h"
+#include "smt/smt_solver.h"
+#include "solver/solver.h"
namespace smtlib {
class parser;
@@ -49,6 +52,24 @@ namespace realclosure {
namespace api {
+ class seq_expr_solver : public expr_solver {
+ ast_manager& m;
+ params_ref const& p;
+ solver_ref s;
+ public:
+ seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {}
+ lbool check_sat(expr* e) {
+ if (!s) {
+ s = mk_smt_solver(m, p, symbol("ALL"));
+ }
+ s->push();
+ s->assert_expr(e);
+ lbool r = s->check_sat();
+ s->pop(1);
+ return r;
+ }
+ };
+
class context : public tactic_manager {
struct add_plugins { add_plugins(ast_manager & m); };
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index c95a36df5..0937e668e 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -161,7 +161,10 @@ extern "C" {
CHECK_NON_NULL(m, false);
CHECK_IS_EXPR(t, false);
model * _m = to_model_ref(m);
- expr_ref result(mk_c(c)->m());
+ params_ref p;
+ ast_manager& mgr = mk_c(c)->m();
+ _m->set_solver(alloc(api::seq_expr_solver, mgr, p));
+ expr_ref result(mgr);
model::scoped_model_completion _scm(*_m, model_completion);
result = (*_m)(to_expr(t));
mk_c(c)->save_ast_trail(result.get());
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index b2ed1e5cb..124821561 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -33,6 +33,7 @@ Notes:
#include "ast/ast_printer.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
+#include "ast/rewriter/seq_rewriter.h"
#include "tactic/generic_model_converter.h"
#include "solver/solver.h"
#include "solver/progress_callback.h"
@@ -493,4 +494,24 @@ public:
std::ostream & operator<<(std::ostream & out, cmd_context::status st);
+
+class th_solver : public expr_solver {
+ cmd_context& m_ctx;
+ params_ref m_params;
+ ref<solver> m_solver;
+public:
+ th_solver(cmd_context& ctx): m_ctx(ctx) {}
+
+ lbool check_sat(expr* e) override {
+ if (!m_solver) {
+ m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
+ }
+ m_solver->push();
+ m_solver->assert_expr(e);
+ lbool r = m_solver->check_sat(0,nullptr);
+ m_solver->pop(1);
+ return r;
+ }
+};
+
#endif
diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp
index 3f564edff..a599cfa4a 100644
--- a/src/cmd_context/eval_cmd.cpp
+++ b/src/cmd_context/eval_cmd.cpp
@@ -72,6 +72,7 @@ public:
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
unsigned rlimit = m_params.get_uint("rlimit", 0);
model_evaluator ev(*(md.get()), m_params);
+ ev.set_solver(alloc(th_solver, ctx));
cancel_eh<reslimit> eh(ctx.m().limit());
{
scoped_ctrl_c ctrlc(eh);
diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp
index de548562e..077a46659 100644
--- a/src/cmd_context/simplify_cmd.cpp
+++ b/src/cmd_context/simplify_cmd.cpp
@@ -24,29 +24,10 @@ Notes:
#include "util/scoped_timer.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
-#include "ast/rewriter/seq_rewriter.h"
#include<iomanip>
class simplify_cmd : public parametric_cmd {
- class th_solver : public expr_solver {
- cmd_context& m_ctx;
- params_ref m_params;
- ref<solver> m_solver;
- public:
- th_solver(cmd_context& ctx): m_ctx(ctx) {}
-
- lbool check_sat(expr* e) override {
- if (!m_solver) {
- m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
- }
- m_solver->push();
- m_solver->assert_expr(e);
- lbool r = m_solver->check_sat(0,nullptr);
- m_solver->pop(1);
- return r;
- }
- };
expr * m_target;
public:
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 86ff64ea3..de6bb4db8 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -468,6 +468,10 @@ expr_ref model::operator()(expr* t) {
return m_mev(t);
}
+void model::set_solver(expr_solver* s) {
+ m_mev.set_solver(s);
+}
+
expr_ref_vector model::operator()(expr_ref_vector const& ts) {
expr_ref_vector rs(m);
for (expr* t : ts) rs.push_back((*this)(t));
diff --git a/src/model/model.h b/src/model/model.h
index 0b74de771..2599a3fcd 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -95,6 +95,7 @@ public:
bool is_false(expr* t);
bool is_true(expr_ref_vector const& ts);
void reset_eval_cache();
+ void set_solver(expr_solver* solver);
class scoped_model_completion {
bool m_old_completion;
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 0fe1fe7c6..b0e97e5e4 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -627,3 +627,7 @@ bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_co
tmp = mk_and(ts);
return eval(tmp, r, model_completion);
}
+
+void model_evaluator::set_solver(expr_solver* solver) {
+ m_imp->m_cfg.m_seq_rw.set_solver(solver);
+}
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index 8666e3519..1959af246 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -25,6 +25,7 @@ Revision History:
class model;
class model_core;
+class expr_solver;
typedef rewriter_exception model_evaluator_exception;
@@ -55,6 +56,8 @@ public:
bool is_false(expr * t);
bool is_true(expr_ref_vector const& ts);
+ void set_solver(expr_solver* solver);
+
/**
* best effort evaluator of extensional array equality.
*/