3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00

add also get-consequences

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-08 12:28:45 -07:00
parent be33bb7b48
commit 228b952a50
4 changed files with 28 additions and 0 deletions

View file

@ -61,6 +61,11 @@ extern "C" {
m_out << "(push)\n";
}
void solver2smt2_pp::reset() {
m_out << "(reset)\n";
m_pp_util.reset();
}
void solver2smt2_pp::pop(unsigned n) {
m_out << "(pop " << n << ")\n";
}
@ -75,6 +80,22 @@ extern "C" {
m_out.flush();
}
void solver2smt2_pp::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables) {
m_out << "(get-consequences (";
for (expr* f : assumptions) {
m_out << "\n";
m_pp_util.display_expr(m_out, f);
}
m_out << ") (";
for (expr* f : variables) {
m_out << "\n";
m_pp_util.display_expr(m_out, f);
}
m_out << ")\n";
m_out.flush();
}
solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) {
if (!m_out) {
std::string msg;
@ -383,6 +404,7 @@ extern "C" {
LOG_Z3_solver_reset(c, s);
RESET_ERROR_CODE();
to_solver(s)->m_solver = nullptr;
if (to_solver(s)->m_pp) to_solver(s)->m_pp->reset();
Z3_CATCH;
}
@ -711,6 +733,7 @@ extern "C" {
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
if (to_solver(s)->m_pp) to_solver(s)->m_pp->get_consequences(_assumptions, _variables);
result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
}
catch (z3_exception & ex) {

View file

@ -29,7 +29,9 @@ struct solver2smt2_pp {
void assert_expr(expr* e, expr* t);
void push();
void pop(unsigned n);
void reset();
void check(unsigned n, expr* const* asms);
void get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables);
};
struct Z3_solver_ref : public api::object {

View file

@ -35,6 +35,8 @@ class ast_pp_util {
ast_pp_util(ast_manager& m): m(m), m_env(m), m_num_sorts(0), m_num_decls(0), coll(m) {}
void reset() { coll.reset(); m_removed.reset(); m_num_sorts = 0; m_num_decls = 0; }
void collect(expr* e);
void collect(unsigned n, expr* const* es);

View file

@ -48,6 +48,7 @@ public:
decl_collector(ast_manager & m);
ast_manager & m() { return m_manager; }
void reset() { m_sorts.reset(); m_decls.reset(); m_visited.reset(); m_trail.reset(); }
void visit_func(func_decl* n);
void visit(ast * n);
void visit(unsigned n, expr* const* es);