From b3bd9b89b541bff02bdad7db735394cdf71cc53d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 17 Nov 2017 19:55:23 -0800
Subject: [PATCH] prepare for inverse model conversion for formulas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/tactic/goal2sat.cpp | 15 ++-
src/solver/solver.cpp | 13 ++-
src/tactic/bv/bit_blaster_model_converter.cpp | 31 ++++--
src/tactic/extension_model_converter.cpp | 94 -------------------
src/tactic/horn_subsume_model_converter.cpp | 8 +-
src/tactic/horn_subsume_model_converter.h | 13 +--
src/tactic/model_converter.cpp | 44 +++++----
7 files changed, 79 insertions(+), 139 deletions(-)
delete mode 100644 src/tactic/extension_model_converter.cpp
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index f037a0e26..d730ea0ee 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -881,8 +881,9 @@ 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;
- expr_ref_vector m_var2expr;
+ model_converter_ref m_cached_mc;
+ sat::model_converter m_mc;
+ expr_ref_vector m_var2expr;
generic_model_converter_ref m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
sat_model_converter(ast_manager & m):
@@ -1025,6 +1026,9 @@ struct sat2goal::imp {
if (m_fmc) m_fmc->collect(visitor);
}
+ void operator()(expr_ref& formula) override {
+ NOT_IMPLEMENTED_YET();
+ }
};
typedef ref<sat_model_converter> sat_model_converter_ref;
@@ -1033,7 +1037,6 @@ struct sat2goal::imp {
expr_ref_vector m_lit2expr;
unsigned long long m_max_memory;
bool m_learned;
- unsigned m_glue;
imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
updt_params(p);
@@ -1041,7 +1044,6 @@ struct sat2goal::imp {
void updt_params(params_ref const & p) {
m_learned = p.get_bool("learned", false);
- m_glue = p.get_uint("glue", UINT_MAX);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
}
@@ -1131,7 +1133,6 @@ struct sat2goal::imp {
checkpoint();
lits.reset();
sat::clause const & c = *cp;
- unsigned sz = c.size();
if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) {
for (sat::literal l : c) {
lits.push_back(lit2expr(mc, l));
@@ -1142,8 +1143,7 @@ struct sat2goal::imp {
}
sat::ba_solver* get_ba_solver(sat::solver const& s) {
- sat::extension* ext = s.get_extension();
- return dynamic_cast<sat::ba_solver*>(ext);
+ return dynamic_cast<sat::ba_solver*>(s.get_extension());
}
void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) {
@@ -1229,7 +1229,6 @@ sat2goal::sat2goal():m_imp(0) {
void sat2goal::collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
- r.insert("glue", CPK_UINT, "(default: max-int) collect learned clauses with glue level below parameter.");
}
struct sat2goal::scoped_set_imp {
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 8f1287dab..f14467337 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -185,21 +185,20 @@ bool solver::is_literal(ast_manager& m, expr* e) {
void solver::assert_expr(expr* f) {
expr_ref fml(f, get_manager());
- if (mc0()) {
- (*mc0())(fml);
+ model_converter_ref mc = get_model_converter();
+ if (mc) {
+ (*mc)(fml);
}
assert_expr_core(fml);
}
void solver::assert_expr(expr* f, expr* t) {
- // let mc0 be the model converter associated with the solver
- // that converts models to their "real state".
ast_manager& m = get_manager();
expr_ref fml(f, m);
expr_ref a(t, m);
-
- if (mc0()) {
- (*mc0())(fml);
+ model_converter_ref mc = get_model_converter();
+ if (mc) {
+ (*mc)(fml);
// (*mc0())(a);
}
assert_expr_core(fml, a);
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index d8dbb77a4..cdcc486a6 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -21,6 +21,7 @@ Notes:
#include "tactic/model_converter.h"
#include "ast/bv_decl_plugin.h"
#include "ast/ast_smt2_pp.h"
+#include "ast/ast_util.h"
/**
If TO_BOOL == true, then bit-vectors of size n were blasted into n-tuples of Booleans.
@@ -171,7 +172,7 @@ struct bit_blaster_model_converter : public model_converter {
return result;
}
- virtual void operator()(model_ref & md, unsigned goal_idx) {
+ void operator()(model_ref & md, unsigned goal_idx) override {
SASSERT(goal_idx == 0);
model * new_model = alloc(model, m());
obj_hashtable<func_decl> bits;
@@ -181,11 +182,29 @@ struct bit_blaster_model_converter : public model_converter {
md = new_model;
}
- virtual void operator()(model_ref & md) {
+ void operator()(model_ref & md) override {
operator()(md, 0);
}
+
+ /**
+ \brief simplisic expansion operator for formulas.
+ It just adds back bit-vector definitions to the formula whether they are used or not.
+
+ */
+ void operator()(expr_ref& fml) override {
+ unsigned sz = m_vars.size();
+ if (sz == 0) return;
+ expr_ref_vector fmls(m());
+ fmls.push_back(fml);
+ for (unsigned i = 0; i < sz; i++) {
+ fmls.push_back(m().mk_eq(m().mk_const(m_vars.get(i)), m_bits.get(i)));
+ }
+ m_vars.reset();
+ m_bits.reset();
+ fml = mk_and(fmls);
+ }
- virtual void display(std::ostream & out) {
+ void display(std::ostream & out) override {
unsigned sz = m_vars.size();
for (unsigned i = 0; i < sz; i++) {
display_add(out, m(), m_vars.get(i), m_bits.get(i));
@@ -196,7 +215,7 @@ protected:
bit_blaster_model_converter(ast_manager & m):m_vars(m), m_bits(m) { }
public:
- virtual model_converter * translate(ast_translation & translator) {
+ model_converter * translate(ast_translation & translator) override {
bit_blaster_model_converter * res = alloc(bit_blaster_model_converter, translator.to());
for (func_decl * v : m_vars)
res->m_vars.push_back(translator(v));
@@ -207,11 +226,11 @@ public:
};
model_converter * mk_bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits) {
- return alloc(bit_blaster_model_converter<true>, m, const2bits);
+ return const2bits.empty() ? nullptr : alloc(bit_blaster_model_converter<true>, m, const2bits);
}
model_converter * mk_bv1_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits) {
- return alloc(bit_blaster_model_converter<false>, m, const2bits);
+ return const2bits.empty() ? nullptr : alloc(bit_blaster_model_converter<false>, m, const2bits);
}
diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp
deleted file mode 100644
index 0ae4e1323..000000000
--- a/src/tactic/extension_model_converter.cpp
+++ /dev/null
@@ -1,94 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
- extension_model_converter.cpp
-
-Abstract:
-
-Model converter that introduces eliminated variables in a model.
-
-Author:
-
- Leonardo (leonardo) 2011-10-21
-
-Notes:
-
---*/
-#include "ast/ast_pp.h"
-#include "ast/ast_smt2_pp.h"
-#include "model/model_evaluator.h"
-#include "model/model_v2_pp.h"
-#include "tactic/extension_model_converter.h"
-
-extension_model_converter::~extension_model_converter() {
-}
-
-#ifdef _TRACE
-static void display_decls_info(std::ostream & out, model_ref & md) {
- ast_manager & m = md->get_manager();
- unsigned sz = md->get_num_decls();
- for (unsigned i = 0; i < sz; i++) {
- func_decl * d = md->get_decl(i);
- out << d->get_name();
- out << " (";
- for (unsigned j = 0; j < d->get_arity(); j++)
- out << mk_pp(d->get_domain(j), m);
- out << mk_pp(d->get_range(), m);
- out << ") ";
- if (d->get_info())
- out << *(d->get_info());
- out << " :id " << d->get_id() << "\n";
- }
-}
-#endif
-
-void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
- SASSERT(goal_idx == 0);
- TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
- model_evaluator ev(*(md.get()));
- ev.set_model_completion(true);
- ev.set_expand_array_equalities(false);
- expr_ref val(m());
- unsigned i = m_vars.size();
- while (i > 0) {
- --i;
- expr * def = m_defs.get(i);
- ev(def, val);
- TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";);
- func_decl * f = m_vars.get(i);
- unsigned arity = f->get_arity();
- if (arity == 0) {
- md->register_decl(f, val);
- }
- else {
- func_interp * new_fi = alloc(func_interp, m(), arity);
- new_fi->set_else(val);
- md->register_decl(f, new_fi);
- }
- }
- TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
-}
-
-void extension_model_converter::insert(func_decl * v, expr * def) {
- m_vars.push_back(v);
- m_defs.push_back(def);
-}
-
-
-void extension_model_converter::display(std::ostream & out) {
- for (unsigned i = 0; i < m_vars.size(); i++) {
- display_add(out, m(), m_vars.get(i), m_defs.get(i));
- }
-}
-
-model_converter * extension_model_converter::translate(ast_translation & translator) {
- extension_model_converter * res = alloc(extension_model_converter, translator.to());
- for (func_decl* v : m_vars)
- res->m_vars.push_back(translator(v));
- for (expr* d : m_defs)
- res->m_defs.push_back(translator(d));
- return res;
-}
-
diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp
index cb56f9b7b..0d49a769e 100644
--- a/src/tactic/horn_subsume_model_converter.cpp
+++ b/src/tactic/horn_subsume_model_converter.cpp
@@ -170,6 +170,10 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
}
+void horn_subsume_model_converter::operator()(expr_ref& fml) {
+ NOT_IMPLEMENTED_YET();
+}
+
void horn_subsume_model_converter::operator()(model_ref& mr) {
func_decl_ref pred(m);
@@ -190,11 +194,11 @@ void horn_subsume_model_converter::operator()(model_ref& mr) {
add_default_false_interpretation(body, mr);
SASSERT(m.is_bool(body));
- TRACE("mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
+ TRACE("mc", tout << "eval: " << h->get_name() << "\n" << body << "\n";);
expr_ref tmp(body);
mr->eval(tmp, body);
- TRACE("mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
+ TRACE("mc", tout << "to:\n" << body << "\n";);
if (arity == 0) {
expr* e = mr->get_const_interp(h);
diff --git a/src/tactic/horn_subsume_model_converter.h b/src/tactic/horn_subsume_model_converter.h
index 74d5882a5..9b094e575 100644
--- a/src/tactic/horn_subsume_model_converter.h
+++ b/src/tactic/horn_subsume_model_converter.h
@@ -58,9 +58,8 @@ class horn_subsume_model_converter : public model_converter {
public:
- horn_subsume_model_converter(ast_manager& m):
- m(m), m_funcs(m), m_bodies(m), m_rewrite(m),
- m_delay_head(m), m_delay_body(m) {}
+ horn_subsume_model_converter(ast_manager& m):
+ m(m), m_funcs(m), m_bodies(m), m_rewrite(m), m_delay_head(m), m_delay_body(m) {}
bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body);
@@ -72,13 +71,15 @@ public:
void insert(func_decl* p, expr* body) { m_funcs.push_back(p); m_bodies.push_back(body); }
- virtual void operator()(model_ref& _m);
+ void operator()(model_ref& _m) override;
- virtual model_converter * translate(ast_translation & translator);
+ void operator()(expr_ref& fml) override;
+
+ model_converter * translate(ast_translation & translator) override;
ast_manager& get_manager() { return m; }
- virtual void display(std::ostream & out) {}
+ void display(std::ostream & out) override {}
};
#endif
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index 01c7a16bb..ab1e2a9bc 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -58,28 +58,33 @@ public:
VERIFY(m_c1 && m_c2);
}
- virtual void operator()(model_ref & m) {
+ void operator()(model_ref & m) override {
this->m_c2->operator()(m);
this->m_c1->operator()(m);
}
- virtual void operator()(model_ref & m, unsigned goal_idx) {
+ void operator()(expr_ref & fml) override {
+ this->m_c1->operator()(fml);
+ this->m_c2->operator()(fml);
+ }
+
+ void operator()(model_ref & m, unsigned goal_idx) override {
this->m_c2->operator()(m, goal_idx);
this->m_c1->operator()(m, 0);
}
- virtual void operator()(labels_vec & r, unsigned goal_idx) {
+ void operator()(labels_vec & r, unsigned goal_idx) override {
this->m_c2->operator()(r, goal_idx);
this->m_c1->operator()(r, 0);
}
- virtual char const * get_name() const { return "concat-model-converter"; }
+ char const * get_name() const override { return "concat-model-converter"; }
- virtual model_converter * translate(ast_translation & translator) {
+ model_converter * translate(ast_translation & translator) override {
return this->translate_core<concat_model_converter>(translator);
}
- virtual void collect(ast_pp_util& visitor) {
+ void collect(ast_pp_util& visitor) override {
this->m_c1->collect(visitor);
this->m_c2->collect(visitor);
}
@@ -99,12 +104,12 @@ public:
concat_star_converter<model_converter>(mc1, num, mc2s, szs) {
}
- virtual void operator()(model_ref & m) {
+ void operator()(model_ref & m) override {
// TODO: delete method after conversion is complete
UNREACHABLE();
}
- virtual void operator()(model_ref & m, unsigned goal_idx) {
+ void operator()(model_ref & m, unsigned goal_idx) override {
unsigned num = this->m_c2s.size();
for (unsigned i = 0; i < num; i++) {
if (goal_idx < this->m_szs[i]) {
@@ -122,7 +127,7 @@ public:
UNREACHABLE();
}
- virtual void operator()(labels_vec & r, unsigned goal_idx) {
+ void operator()(labels_vec & r, unsigned goal_idx) override {
unsigned num = this->m_c2s.size();
for (unsigned i = 0; i < num; i++) {
if (goal_idx < this->m_szs[i]) {
@@ -140,9 +145,9 @@ public:
UNREACHABLE();
}
- virtual char const * get_name() const { return "concat-star-model-converter"; }
+ char const * get_name() const override { return "concat-star-model-converter"; }
- virtual model_converter * translate(ast_translation & translator) {
+ model_converter * translate(ast_translation & translator) override {
return this->translate_core<concat_star_model_converter>(translator);
}
};
@@ -173,22 +178,28 @@ public:
virtual ~model2mc() {}
- virtual void operator()(model_ref & m) {
+ void operator()(model_ref & m) override {
m = m_model;
}
- virtual void operator()(model_ref & m, unsigned goal_idx) {
+ void operator()(model_ref & m, unsigned goal_idx) override {
m = m_model;
}
- virtual void operator()(labels_vec & r, unsigned goal_idx) {
+ void operator()(labels_vec & r, unsigned goal_idx) {
r.append(m_labels.size(), m_labels.c_ptr());
}
- virtual void cancel() {
+ void operator()(expr_ref& fml) override {
+ expr_ref r(m_model->get_manager());
+ m_model->eval(fml, r, false);
+ fml = r;
+ }
+
+ void cancel() override {
}
- virtual void display(std::ostream & out) {
+ void display(std::ostream & out) override {
out << "(model->model-converter-wrapper\n";
model_v2_pp(out, *m_model);
out << ")\n";
@@ -198,6 +209,7 @@ public:
model * m = m_model->translate(translator);
return alloc(model2mc, m);
}
+
};
model_converter * model2model_converter(model * m) {