mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fixing smtfd

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-10 18:23:23 -08:00
parent d23230ec15
commit 779183da06
3 changed files with 132 additions and 103 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/dotnet/Context.cs
View file

@ -2636,6 +2636,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create the empty regular expression. /// Create the empty regular expression.
/// The sort s should be a regular expression.
/// </summary> /// </summary>
public ReExpr MkEmptyRe(Sort s) public ReExpr MkEmptyRe(Sort s)
{ {
@ -2645,6 +2646,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create the full regular expression. /// Create the full regular expression.
/// The sort s should be a regular expression.
/// </summary> /// </summary>
public ReExpr MkFullRe(Sort s) public ReExpr MkFullRe(Sort s)
{ {

3
src/ast/array_decl_plugin.cpp
View file

@ -259,8 +259,8 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
std::stringstream strm; std::stringstream strm;
strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter "; strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter ";
strm << parameter_pp(parameters[i], *m_manager) << " do not match"; strm << parameter_pp(parameters[i], *m_manager) << " do not match";
SASSERT(false);
m_manager->raise_exception(strm.str()); m_manager->raise_exception(strm.str());
UNREACHABLE();
return nullptr; return nullptr;
} }
new_domain.push_back(to_sort(parameters[i].get_ast())); new_domain.push_back(to_sort(parameters[i].get_ast()));
@ -303,6 +303,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
if (!m_manager->compatible_sorts(srt1, srt2)) { if (!m_manager->compatible_sorts(srt1, srt2)) {
std::stringstream strm; std::stringstream strm;
strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match"; strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match";
SASSERT(false);
m_manager->raise_exception(strm.str()); m_manager->raise_exception(strm.str());
UNREACHABLE(); UNREACHABLE();
return nullptr; return nullptr;

230
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -121,6 +121,7 @@ Note:
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
#include "util/obj_pair_hashtable.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
@ -358,6 +359,7 @@ namespace smtfd {
struct f_app { struct f_app {
ast* m_f; ast* m_f;
app* m_t; app* m_t;
sort* m_s;
unsigned m_val_offset; unsigned m_val_offset;
}; };
@ -387,7 +389,7 @@ namespace smtfd {
smtfd_abs& get_abs() { return m_abs; } smtfd_abs& get_abs() { return m_abs; }
void add(expr* f) { m_lemmas.push_back(f); } void add(expr* f, char const* msg) { m_lemmas.push_back(f); TRACE("smtfd", tout << msg << " " << mk_bounded_pp(f, m, 2) << "\n";); }
ast_manager& get_manager() { return m_lemmas.get_manager(); } ast_manager& get_manager() { return m_lemmas.get_manager(); }
@ -413,7 +415,7 @@ namespace smtfd {
/** /**
* \brief use propositional model to create a model of uninterpreted functions * \brief use propositional model to create a model of uninterpreted functions
*/ */
void populate_model(model_ref& mdl, expr_ref_vector const& core); void populate_model(model_ref& mdl, expr_ref_vector const& terms);
/** /**
* \brief check consistency properties that can only be achived using a global analysis of terms * \brief check consistency properties that can only be achived using a global analysis of terms
@ -457,14 +459,15 @@ namespace smtfd {
f_app_eq m_eq; f_app_eq m_eq;
f_app_hash m_hash; f_app_hash m_hash;
scoped_ptr_vector<table> m_tables; scoped_ptr_vector<table> m_tables;
obj_map<ast, unsigned> m_ast2table; obj_pair_map<ast, sort, unsigned> m_ast2table;
f_app mk_app(ast* f, app* t) { f_app mk_app(ast* f, app* t, sort* s) {
f_app r; f_app r;
r.m_f = f; r.m_f = f;
r.m_val_offset = m_values.size(); r.m_val_offset = m_values.size();
r.m_t = t; r.m_t = t;
r.m_s = s;
for (expr* arg : *t) { for (expr* arg : *t) {
m_values.push_back(eval_abs(arg)); m_values.push_back(eval_abs(arg));
} }
@ -473,7 +476,7 @@ namespace smtfd {
} }
f_app const& insert(f_app const& f) { f_app const& insert(f_app const& f) {
return ast2table(f.m_f).insert_if_not_there(f); return ast2table(f.m_f, f.m_s).insert_if_not_there(f);
} }
public: public:
@ -491,12 +494,12 @@ namespace smtfd {
m_context.add_plugin(this); m_context.add_plugin(this);
} }
table& ast2table(ast* f) { table& ast2table(ast* f, sort* s) {
unsigned idx = 0; unsigned idx = 0;
if (!m_ast2table.find(f, idx)) { if (!m_ast2table.find(f, s, idx)) {
idx = m_tables.size(); idx = m_tables.size();
m_tables.push_back(alloc(table, DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq)); m_tables.push_back(alloc(table, DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq));
m_ast2table.insert(f, idx); m_ast2table.insert(f, s, idx);
m_pinned.push_back(f); m_pinned.push_back(f);
} }
return *m_tables[idx]; return *m_tables[idx];
@ -506,17 +509,13 @@ namespace smtfd {
ast_manager& get_manager() { return m; } ast_manager& get_manager() { return m; }
void add_lemma(expr* fml) {
m_context.add(fml);
}
expr_ref eval_abs(expr* t) { return m_context.get_model()(m_abs.abs(t)); } expr_ref eval_abs(expr* t) { return m_context.get_model()(m_abs.abs(t)); }
bool is_true_abs(expr* t) { return m_context.get_model().is_true(m_abs.abs(t)); } bool is_true_abs(expr* t) { return m_context.get_model().is_true(m_abs.abs(t)); }
expr* value_of(f_app const& f) const { return m_values[f.m_val_offset + f.m_t->get_num_args()]; } expr* value_of(f_app const& f) const { return m_values[f.m_val_offset + f.m_t->get_num_args()]; }
bool check_congruence(ast* f, app* t) { bool check_congruence(ast* f, app* t, sort* s) {
f_app f1 = mk_app(f, t); f_app f1 = mk_app(f, t, s);
f_app const& f2 = insert(f1); f_app const& f2 = insert(f1);
if (f2.m_val_offset == f1.m_val_offset) { if (f2.m_val_offset == f1.m_val_offset) {
return true; return true;
@ -526,15 +525,17 @@ namespace smtfd {
return eq; return eq;
} }
void enforce_congruence(ast* f, app* t) { void enforce_congruence(ast* f, app* t, sort* s) {
f_app f1 = mk_app(f, t); f_app f1 = mk_app(f, t, s);
f_app const& f2 = insert(f1); f_app const& f2 = insert(f1);
if (f2.m_val_offset == f1.m_val_offset) { if (f2.m_val_offset == f1.m_val_offset) {
TRACE("smtfd_verbose", tout << "fresh: " << mk_pp(f, m, 2) << "\n";);
return; return;
} }
bool eq = value_of(f1) == value_of(f2); bool eq = value_of(f1) == value_of(f2);
m_values.shrink(f1.m_val_offset); m_values.shrink(f1.m_val_offset);
if (eq) { if (eq) {
TRACE("smtfd_verbose", tout << "eq: " << " " << mk_bounded_pp(t, m, 2) << " " << mk_bounded_pp(f2.m_t, m, 2) << "\n";);
return; return;
} }
m_args.reset(); m_args.reset();
@ -545,8 +546,8 @@ namespace smtfd {
expr* e2 = f2.m_t->get_arg(i); expr* e2 = f2.m_t->get_arg(i);
if (e1 != e2) m_args.push_back(m.mk_eq(e1, e2)); if (e1 != e2) m_args.push_back(m.mk_eq(e1, e2));
} }
TRACE("smtfd", tout << mk_bounded_pp(f1.m_t, m, 2) << " " << mk_bounded_pp(f2.m_t, m, 2) << "\n";); TRACE("smtfd_verbose", tout << "diff: " << mk_bounded_pp(f1.m_t, m, 2) << " " << mk_bounded_pp(f2.m_t, m, 2) << "\n";);
add_lemma(m.mk_implies(mk_and(m_args), m.mk_eq(f1.m_t, f2.m_t))); m_context.add(m.mk_implies(mk_and(m_args), m.mk_eq(f1.m_t, f2.m_t)), __FUNCTION__);
} }
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
@ -579,7 +580,7 @@ namespace smtfd {
virtual bool term_covered(expr* t) = 0; virtual bool term_covered(expr* t) = 0;
virtual bool sort_covered(sort* s) = 0; virtual bool sort_covered(sort* s) = 0;
virtual unsigned max_rounds() = 0; virtual unsigned max_rounds() = 0;
virtual void populate_model(model_ref& mdl, expr_ref_vector const& core) {} virtual void populate_model(model_ref& mdl, expr_ref_vector const& terms) {}
virtual void reset() { virtual void reset() {
m_pinned.reset(); m_pinned.reset();
m_tables.reset(); m_tables.reset();
@ -662,9 +663,9 @@ namespace smtfd {
return out; return out;
} }
void plugin_context::populate_model(model_ref& mdl, expr_ref_vector const& core) { void plugin_context::populate_model(model_ref& mdl, expr_ref_vector const& terms) {
for (theory_plugin* p : m_plugins) { for (theory_plugin* p : m_plugins) {
p->populate_model(mdl, core); p->populate_model(mdl, terms);
} }
} }
@ -693,7 +694,7 @@ namespace smtfd {
bool term_covered(expr* t) override { return is_app(t) && to_app(t)->get_family_id() == m.get_basic_family_id(); } bool term_covered(expr* t) override { return is_app(t) && to_app(t)->get_family_id() == m.get_basic_family_id(); }
bool sort_covered(sort* s) override { return m.is_bool(s); } bool sort_covered(sort* s) override { return m.is_bool(s); }
unsigned max_rounds() override { return 0; } unsigned max_rounds() override { return 0; }
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { } void populate_model(model_ref& mdl, expr_ref_vector const& terms) override { }
expr_ref model_value_core(expr* t) override { return m.is_bool(t) ? m_context.get_model()(m_abs.abs(t)) : expr_ref(m); } expr_ref model_value_core(expr* t) override { return m.is_bool(t) ? m_context.get_model()(m_abs.abs(t)) : expr_ref(m); }
expr_ref model_value_core(sort* s) override { return m.is_bool(s) ? expr_ref(m.mk_false(), m) : expr_ref(m); } expr_ref model_value_core(sort* s) override { return m.is_bool(s) ? expr_ref(m.mk_false(), m) : expr_ref(m); }
}; };
@ -709,7 +710,7 @@ namespace smtfd {
bool term_covered(expr* t) override { return is_app(t) && to_app(t)->get_family_id() == m_pb.get_family_id(); } bool term_covered(expr* t) override { return is_app(t) && to_app(t)->get_family_id() == m_pb.get_family_id(); }
bool sort_covered(sort* s) override { return m.is_bool(s); } bool sort_covered(sort* s) override { return m.is_bool(s); }
unsigned max_rounds() override { return 0; } unsigned max_rounds() override { return 0; }
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { } void populate_model(model_ref& mdl, expr_ref_vector const& terms) override { }
expr_ref model_value_core(expr* t) override { return expr_ref(m); } expr_ref model_value_core(expr* t) override { return expr_ref(m); }
expr_ref model_value_core(sort* s) override { return expr_ref(m); } expr_ref model_value_core(sort* s) override { return expr_ref(m); }
}; };
@ -725,7 +726,7 @@ namespace smtfd {
bool term_covered(expr* t) override { return is_app(t) && to_app(t)->get_family_id() == m_butil.get_family_id(); } bool term_covered(expr* t) override { return is_app(t) && to_app(t)->get_family_id() == m_butil.get_family_id(); }
bool sort_covered(sort* s) override { return m_butil.is_bv_sort(s); } bool sort_covered(sort* s) override { return m_butil.is_bv_sort(s); }
unsigned max_rounds() override { return 0; } unsigned max_rounds() override { return 0; }
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { } void populate_model(model_ref& mdl, expr_ref_vector const& terms) override { }
expr_ref model_value_core(expr* t) override { return m_butil.is_bv(t) ? m_context.get_model()(m_abs.abs(t)) : expr_ref(m); } expr_ref model_value_core(expr* t) override { return m_butil.is_bv(t) ? m_context.get_model()(m_abs.abs(t)) : expr_ref(m); }
expr_ref model_value_core(sort* s) override { return m_butil.is_bv_sort(s) ? expr_ref(m_butil.mk_numeral(rational(0), s), m) : expr_ref(m); } expr_ref model_value_core(sort* s) override { return m_butil.is_bv_sort(s) ? expr_ref(m_butil.mk_numeral(rational(0), s), m) : expr_ref(m); }
}; };
@ -777,8 +778,10 @@ namespace smtfd {
{} {}
void check_term(expr* t, unsigned round) override { void check_term(expr* t, unsigned round) override {
if (round == 0 && is_uf(t)) if (round == 0 && is_uf(t)) {
enforce_congruence(to_app(t)->get_decl(), to_app(t)); TRACE("smtfd_verbose", tout << "check-term: " << mk_bounded_pp(t, m, 2) << "\n";);
enforce_congruence(to_app(t)->get_decl(), to_app(t), m.get_sort(t));
}
} }
bool term_covered(expr* t) override { bool term_covered(expr* t) override {
@ -791,6 +794,7 @@ namespace smtfd {
v2e.insert(v, nullptr); v2e.insert(v, nullptr);
} }
} }
check_term(t, 0);
return is_uf(t) || is_uninterp_const(t); return is_uf(t) || is_uninterp_const(t);
} }
@ -807,7 +811,7 @@ namespace smtfd {
unsigned max_rounds() override { return 1; } unsigned max_rounds() override { return 1; }
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { void populate_model(model_ref& mdl, expr_ref_vector const& terms) override {
expr_ref_vector args(m); expr_ref_vector args(m);
for (table* tb : m_tables) { for (table* tb : m_tables) {
func_interp* fi = nullptr; func_interp* fi = nullptr;
@ -823,11 +827,12 @@ namespace smtfd {
args.push_back(model_value(arg)); args.push_back(model_value(arg));
} }
expr_ref val = model_value(f.m_t); expr_ref val = model_value(f.m_t);
fi->insert_new_entry(args.c_ptr(),val); TRACE("smtfd_verbose", tout << mk_bounded_pp(f.m_t, m, 2) << " := " << val << "\n";);
fi->insert_new_entry(args.c_ptr(), val);
} }
mdl->register_decl(fn, fi); mdl->register_decl(fn, fi);
} }
for (expr* t : subterms(core)) { for (expr* t : subterms(terms)) {
if (is_uninterp_const(t) && sort_covered(m.get_sort(t))) { if (is_uninterp_const(t) && sort_covered(m.get_sort(t))) {
expr_ref val = model_value(t); expr_ref val = model_value(t);
mdl->register_decl(to_app(t)->get_decl(), val); mdl->register_decl(to_app(t)->get_decl(), val);
@ -886,13 +891,13 @@ namespace smtfd {
void insert_select(app* t) { void insert_select(app* t) {
expr* a = t->get_arg(0); expr* a = t->get_arg(0);
expr_ref vA = eval_abs(a); expr_ref vA = eval_abs(a);
check_congruence(vA, t); check_congruence(vA, t, m.get_sort(a));
} }
void check_select(app* t) { void check_select(app* t) {
expr* a = t->get_arg(0); expr* a = t->get_arg(0);
expr_ref vA = eval_abs(a); expr_ref vA = eval_abs(a);
enforce_congruence(vA, t); enforce_congruence(vA, t, m.get_sort(a));
} }
// check that (select(t, t.args) = t.value) // check that (select(t, t.args) = t.value)
@ -910,7 +915,7 @@ namespace smtfd {
// A[i] = v // A[i] = v
if (val1 != val2) { if (val1 != val2) {
TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";); TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";);
add_lemma(m.mk_eq(sel, stored_value)); m_context.add(m.mk_eq(sel, stored_value), __FUNCTION__);
m_pinned.push_back(sel); m_pinned.push_back(sel);
insert_select(sel); insert_select(sel);
} }
@ -943,14 +948,14 @@ namespace smtfd {
expr_ref val1 = eval_abs(t); expr_ref val1 = eval_abs(t);
expr_ref val2 = eval_abs(val); expr_ref val2 = eval_abs(val);
if (val1 != val2 && !m.is_false(eqV)) { if (val1 != val2 && !m.is_false(eqV)) {
add_lemma(m.mk_implies(mk_and(eqs), m.mk_eq(t, val))); m_context.add(m.mk_implies(mk_and(eqs), m.mk_eq(t, val)), __FUNCTION__);
} }
app_ref sel(m_autil.mk_select(m_args), m); app_ref sel(m_autil.mk_select(m_args), m);
val2 = eval_abs(sel); val2 = eval_abs(sel);
if (val1 != val2 && !m.is_true(eqV)) { if (val1 != val2 && !m.is_true(eqV)) {
TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";); TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";);
add_lemma(m.mk_or(m.mk_eq(sel, t), mk_and(eqs))); m_context.add(m.mk_or(m.mk_eq(sel, t), mk_and(eqs)), __FUNCTION__);
m_pinned.push_back(sel); m_pinned.push_back(sel);
insert_select(sel); insert_select(sel);
} }
@ -976,8 +981,8 @@ namespace smtfd {
expr_ref vT = eval_abs(t); expr_ref vT = eval_abs(t);
expr_ref vA = eval_abs(arg); expr_ref vA = eval_abs(arg);
table& tT = ast2table(vT); // select table of t table& tT = ast2table(vT, m.get_sort(t)); // select table of t
table& tA = ast2table(vA); // select table of arg table& tA = ast2table(vA, m.get_sort(arg)); // select table of arg
if (vT == vA) { if (vT == vA) {
return; return;
@ -997,7 +1002,7 @@ namespace smtfd {
// //
void reconcile_stores(app* t, expr* vT, table& tT, expr* vA, table& tA) { void reconcile_stores(app* t, expr* vT, table& tT, expr* vA, table& tA) {
unsigned r = 0; unsigned r = 0;
if (false && get_lambda(vA) <= 1) { if (get_lambda(vA) <= 1) {
return; return;
} }
inc_lambda(vT); inc_lambda(vT);
@ -1014,8 +1019,8 @@ namespace smtfd {
++r; ++r;
} }
} }
#if 1 #if 0
// only up-propagation really needed. // only up-propagation really needed.
for (auto& fT : tT) { for (auto& fT : tT) {
f_app fA; f_app fA;
if (m_context.at_max()) { if (m_context.at_max()) {
@ -1028,11 +1033,6 @@ namespace smtfd {
} }
} }
#endif #endif
if (r > 0 && false) {
std::cout << r << " " << mk_bounded_pp(t, m, 3) << "\n";
display(std::cout, tT);
display(std::cout, tA);
}
} }
void add_select_store_axiom(app* t, f_app& f) { void add_select_store_axiom(app* t, f_app& f) {
@ -1051,7 +1051,7 @@ namespace smtfd {
expr_ref sel2(m_autil.mk_select(m_args), m); expr_ref sel2(m_autil.mk_select(m_args), m);
expr_ref fml(m.mk_or(eq, m.mk_eq(sel1, sel2)), m); expr_ref fml(m.mk_or(eq, m.mk_eq(sel1, sel2)), m);
if (!is_true_abs(fml)) { if (!is_true_abs(fml)) {
add_lemma(fml); m_context.add(fml, __FUNCTION__);
} }
} }
@ -1067,7 +1067,7 @@ namespace smtfd {
m_autil.is_const(t) || m_autil.is_const(t) ||
is_lambda(t)) { is_lambda(t)) {
expr_ref vT = eval_abs(t); expr_ref vT = eval_abs(t);
table& tT = ast2table(vT); table& tT = ast2table(vT, m.get_sort(t));
for (f_app & f : tT) { for (f_app & f : tT) {
if (m.get_sort(t) != m.get_sort(f.m_t->get_arg(0))) if (m.get_sort(t) != m.get_sort(f.m_t->get_arg(0)))
continue; continue;
@ -1082,7 +1082,7 @@ namespace smtfd {
expr_ref vS = eval_abs(sel); expr_ref vS = eval_abs(sel);
expr_ref vR = eval_abs(selr); expr_ref vR = eval_abs(selr);
if (vS != vR) { if (vS != vR) {
add_lemma(m.mk_eq(sel, selr)); m_context.add(m.mk_eq(sel, selr), __FUNCTION__);
} }
} }
} }
@ -1122,8 +1122,8 @@ namespace smtfd {
return true; return true;
} }
bool same_table(expr* v1, expr* v2) { bool same_table(expr* v1, sort* s1, expr* v2, sort* s2) {
return same_table(ast2table(v1), ast2table(v2)); return same_table(ast2table(v1, s1), ast2table(v2, s2));
} }
void enforce_extensionality(expr* a, expr* b) { void enforce_extensionality(expr* a, expr* b) {
@ -1140,7 +1140,7 @@ namespace smtfd {
expr_ref ext(m.mk_iff(m.mk_eq(a1, b1), m.mk_eq(a, b)), m); expr_ref ext(m.mk_iff(m.mk_eq(a1, b1), m.mk_eq(a, b)), m);
if (!m.is_true(eval_abs(ext))) { if (!m.is_true(eval_abs(ext))) {
TRACE("smtfd", tout << mk_bounded_pp(a, m, 2) << " " << mk_bounded_pp(b, m, 2) << "\n";); TRACE("smtfd", tout << mk_bounded_pp(a, m, 2) << " " << mk_bounded_pp(b, m, 2) << "\n";);
add_lemma(ext); m_context.add(ext, __FUNCTION__);
} }
} }
@ -1218,7 +1218,7 @@ namespace smtfd {
if (m_autil.is_select(t)) { if (m_autil.is_select(t)) {
expr* a = to_app(t)->get_arg(0); expr* a = to_app(t)->get_arg(0);
expr_ref vA = eval_abs(a); expr_ref vA = eval_abs(a);
insert(mk_app(vA, to_app(t))); insert(mk_app(vA, to_app(t), m.get_sort(a)));
} }
return return
@ -1247,7 +1247,7 @@ namespace smtfd {
expr_ref model_value_core(expr* t) override { expr_ref model_value_core(expr* t) override {
if (m_autil.is_array(t)) { if (m_autil.is_array(t)) {
expr_ref vT = eval_abs(t); expr_ref vT = eval_abs(t);
table& tb = ast2table(vT); table& tb = ast2table(vT, m.get_sort(t));
if (tb.empty()) { if (tb.empty()) {
return model_value_core(m.get_sort(t)); return model_value_core(m.get_sort(t));
} }
@ -1266,8 +1266,8 @@ namespace smtfd {
} }
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { void populate_model(model_ref& mdl, expr_ref_vector const& terms) override {
for (expr* t : subterms(core)) { for (expr* t : subterms(terms)) {
if (is_uninterp_const(t) && m_autil.is_array(t)) { if (is_uninterp_const(t) && m_autil.is_array(t)) {
mdl->register_decl(to_app(t)->get_decl(), model_value_core(t)); mdl->register_decl(to_app(t)->get_decl(), model_value_core(t));
} }
@ -1307,7 +1307,7 @@ namespace smtfd {
for (unsigned j = i + 1; !m_context.at_max() && j < shared.size(); ++j) { for (unsigned j = i + 1; !m_context.at_max() && j < shared.size(); ++j) {
expr* s2 = shared.get(j); expr* s2 = shared.get(j);
expr* v2 = sharedvals.get(j); expr* v2 = sharedvals.get(j);
if (v1 != v2 && m.get_sort(s1) == m.get_sort(s2) && same_table(v1, v2)) { if (v1 != v2 && m.get_sort(s1) == m.get_sort(s2) && same_table(v1, m.get_sort(s1), v2, m.get_sort(s2))) {
enforce_extensionality(s1, s2); enforce_extensionality(s1, s2);
} }
} }
@ -1323,7 +1323,7 @@ namespace smtfd {
model_ref m_model; model_ref m_model;
ref<::solver> m_solver; ref<::solver> m_solver;
expr_ref_vector m_pinned; expr_ref_vector m_pinned;
obj_map<expr, expr*> m_val2term; obj_pair_map<expr, sort, expr*> m_val2term;
expr* abs(expr* e) { return m_context.get_abs().abs(e); } expr* abs(expr* e) { return m_context.get_abs().abs(e); }
expr_ref eval_abs(expr* t) { return (*m_model)(abs(t)); } expr_ref eval_abs(expr* t) { return (*m_model)(abs(t)); }
@ -1350,10 +1350,14 @@ namespace smtfd {
if (!m_model->eval_expr(q->get_expr(), tmp, true)) { if (!m_model->eval_expr(q->get_expr(), tmp, true)) {
return l_undef; return l_undef;
} }
if (m.is_true(tmp)) {
return l_false;
}
TRACE("smtfd", TRACE("smtfd",
tout << mk_pp(q, m) << "\n"; tout << mk_pp(q, m) << "\n";
tout << "eval: " << tmp << "\n"; /*tout << *m_model << "\n"; */
tout << *m_model << "\n";); tout << "eval: " << tmp << "\n";);
m_solver->push(); m_solver->push();
expr_ref_vector vars(m), vals(m); expr_ref_vector vars(m), vals(m);
@ -1384,11 +1388,12 @@ namespace smtfd {
if (is_ground(t)) { if (is_ground(t)) {
expr_ref v = eval_abs(t); expr_ref v = eval_abs(t);
m_pinned.push_back(v); m_pinned.push_back(v);
m_val2term.insert(v, t); m_val2term.insert(v, m.get_sort(t), t);
} }
} }
m_solver->get_model(mdl); m_solver->get_model(mdl);
IF_VERBOSE(1, verbose_stream() << *mdl << "\n"); TRACE("smtfd", tout << *mdl << "\n";);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
app* v = to_app(vars.get(i)); app* v = to_app(vars.get(i));
func_decl* f = v->get_decl(); func_decl* f = v->get_decl();
@ -1396,26 +1401,26 @@ namespace smtfd {
if (!val) { if (!val) {
r = l_undef; r = l_undef;
break; break;
} }
expr* t = nullptr; expr* t = nullptr;
if (m_val2term.find(val, t)) { if (m_val2term.find(val, m.get_sort(v), t)) {
val = t; val = t;
} }
vals[i] = val; vals[i] = val;
} }
if (r == l_true) { }
body = subst(q->get_expr(), vals.size(), vals.c_ptr());
m_context.rewrite(body); if (r == l_true) {
TRACE("smtfd", tout << vals << "\n" << body << "\n";); body = subst(q->get_expr(), vals.size(), vals.c_ptr());
if (is_forall(q)) { m_context.rewrite(body);
body = m.mk_implies(q, body); TRACE("smtfd", tout << "vals: " << vals << "\n" << body << "\n";);
} if (is_forall(q)) {
else { body = m.mk_implies(q, body);
body = m.mk_implies(body, q);
}
m_context.add(body);
} }
else {
body = m.mk_implies(body, q);
}
m_context.add(body, __FUNCTION__);
} }
m_solver->pop(1); m_solver->pop(1);
return r; return r;
@ -1441,7 +1446,7 @@ namespace smtfd {
body = m.mk_implies(body, q); body = m.mk_implies(body, q);
} }
m_enforced.insert(q); m_enforced.insert(q);
m_context.add(body); m_context.add(body, __FUNCTION__);
return l_true; return l_true;
} }
@ -1450,7 +1455,7 @@ namespace smtfd {
if (!m.is_bool(t) && is_ground(t)) { if (!m.is_bool(t) && is_ground(t)) {
expr_ref v = eval_abs(t); expr_ref v = eval_abs(t);
m_pinned.push_back(v); m_pinned.push_back(v);
m_val2term.insert(v, t); m_val2term.insert(v, m.get_sort(t), t);
} }
} }
} }
@ -1469,7 +1474,7 @@ namespace smtfd {
bool check_quantifiers(expr_ref_vector const& core) { bool check_quantifiers(expr_ref_vector const& core) {
bool result = true; bool result = true;
init_val2term(core); init_val2term(core);
IF_VERBOSE(1, IF_VERBOSE(9,
for (expr* c : core) { for (expr* c : core) {
verbose_stream() << "core: " << mk_bounded_pp(c, m, 2) << "\n"; verbose_stream() << "core: " << mk_bounded_pp(c, m, 2) << "\n";
}); });
@ -1521,6 +1526,7 @@ namespace smtfd {
expr_ref_vector m_assertions; expr_ref_vector m_assertions;
unsigned_vector m_assertions_lim; unsigned_vector m_assertions_lim;
unsigned m_assertions_qhead; unsigned m_assertions_qhead;
expr_ref_vector m_axioms;
expr_ref_vector m_toggles; expr_ref_vector m_toggles;
unsigned_vector m_toggles_lim; unsigned_vector m_toggles_lim;
model_ref m_model; model_ref m_model;
@ -1586,7 +1592,7 @@ namespace smtfd {
m_fd_sat_solver->get_model(m_model); m_fd_sat_solver->get_model(m_model);
m_model->set_model_completion(true); m_model->set_model_completion(true);
init_model_assumptions(num_assumptions, assumptions, asms); init_model_assumptions(num_assumptions, assumptions, asms);
TRACE("smtfd", display(tout << asms << "\n");); TRACE("smtfd", display(tout << asms << "\n" << *m_model << "\n"););
lbool r = m_fd_core_solver->check_sat(asms); lbool r = m_fd_core_solver->check_sat(asms);
update_reason_unknown(r, m_fd_core_solver); update_reason_unknown(r, m_fd_core_solver);
if (r == l_false) { if (r == l_false) {
@ -1635,11 +1641,13 @@ namespace smtfd {
bool add_theory_axioms(expr_ref_vector const& core) { bool add_theory_axioms(expr_ref_vector const& core) {
m_context.reset(m_model); m_context.reset(m_model);
for (unsigned round = 0; !m_context.at_max() && m_context.add_theory_axioms(core, round); ++round); expr_ref_vector terms(core);
terms.append(m_axioms);
for (unsigned round = 0; !m_context.at_max() && m_context.add_theory_axioms(terms, round); ++round);
TRACE("smtfd", m_context.display(tout);); TRACE("smtfd", m_context.display(tout););
for (expr* f : m_context) { for (expr* f : m_context) {
IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(f, m) << "\n");
assert_fd(f); assert_fd(f);
} }
m_stats.m_num_lemmas += m_context.size(); m_stats.m_num_lemmas += m_context.size();
@ -1653,16 +1661,28 @@ namespace smtfd {
bool has_q = false; bool has_q = false;
lbool is_decided = l_true; lbool is_decided = l_true;
m_context.reset(m_model); m_context.reset(m_model);
expr_ref_vector terms(core);
terms.append(m_axioms);
TRACE("smtfd", tout << "axioms: " << m_axioms << "\n";);
for (expr* t : subterms(core)) { for (expr* t : subterms(core)) {
if (is_forall(t) || is_exists(t)) { if (is_forall(t) || is_exists(t)) {
has_q = true; has_q = true;
} }
else if (!m_context.term_covered(t) || !m_context.sort_covered(m.get_sort(t))) { }
for (expr* t : subterms(terms)) {
if (!m_context.term_covered(t) || !m_context.sort_covered(m.get_sort(t))) {
is_decided = l_false; is_decided = l_false;
} }
} }
m_context.populate_model(m_model, core); m_context.populate_model(m_model, terms);
TRACE("smtfd",
for (expr* a : subterms(terms)) {
expr_ref val0 = (*m_model)(a);
expr_ref val1 = (*m_model)(abs(a));
if (val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
}
});
TRACE("smtfd", tout << "has quantifier: " << has_q << "\n" << core << "\n";); TRACE("smtfd", tout << "has quantifier: " << has_q << "\n" << core << "\n";);
if (!has_q) { if (!has_q) {
return is_decided; return is_decided;
@ -1676,9 +1696,8 @@ namespace smtfd {
} }
for (expr* f : m_context) { for (expr* f : m_context) {
IF_VERBOSE(10, verbose_stream() << "lemma: " << f->get_id() << ": " << expr_ref(f, m) << "\n"); IF_VERBOSE(10, verbose_stream() << "lemma: " << f->get_id() << ": " << expr_ref(f, m) << "\n");
assert_expr_core(f); assert_fd(f);
} }
flush_assertions();
m_stats.m_num_mbqi += m_context.size(); m_stats.m_num_mbqi += m_context.size();
IF_VERBOSE(10, verbose_stream() << "context size: " << m_context.size() << "\n"); IF_VERBOSE(10, verbose_stream() << "context size: " << m_context.size() << "\n");
return m_context.empty() ? is_decided : l_undef; return m_context.empty() ? is_decided : l_undef;
@ -1709,7 +1728,6 @@ namespace smtfd {
asms.push_back(m.mk_not(a)); asms.push_back(m.mk_not(a));
} }
} }
std::cout << "asms: " << asms << "\n";
} }
void checkpoint() { void checkpoint() {
@ -1725,6 +1743,7 @@ namespace smtfd {
expr_ref_vector& abs(expr_ref_vector& v) { for (unsigned i = v.size(); i-- > 0; ) v[i] = abs(v.get(i)); return v; } expr_ref_vector& abs(expr_ref_vector& v) { for (unsigned i = v.size(); i-- > 0; ) v[i] = abs(v.get(i)); return v; }
void init() { void init() {
m_axioms.reset();
if (!m_fd_sat_solver) { if (!m_fd_sat_solver) {
m_fd_sat_solver = mk_fd_solver(m, get_params()); m_fd_sat_solver = mk_fd_solver(m, get_params());
m_fd_core_solver = mk_fd_solver(m, get_params()); m_fd_core_solver = mk_fd_solver(m, get_params());
@ -1758,6 +1777,7 @@ namespace smtfd {
m_pb(m_context), m_pb(m_context),
m_assertions(m), m_assertions(m),
m_assertions_qhead(0), m_assertions_qhead(0),
m_axioms(m),
m_toggles(m), m_toggles(m),
m_max_conflicts(50) m_max_conflicts(50)
{ {
@ -1804,7 +1824,7 @@ namespace smtfd {
} }
void flush_atom_defs() { void flush_atom_defs() {
TRACE("smtfd", for (expr* f : m_abs.atom_defs()) tout << mk_bounded_pp(f, m, 4) << "\n";); CTRACE("smtfd", !m_abs.atom_defs().empty(), for (expr* f : m_abs.atom_defs()) tout << mk_bounded_pp(f, m, 4) << "\n";);
for (expr* f : m_abs.atom_defs()) { for (expr* f : m_abs.atom_defs()) {
m_fd_sat_solver->assert_expr(f); m_fd_sat_solver->assert_expr(f);
m_fd_core_solver->assert_expr(f); m_fd_core_solver->assert_expr(f);
@ -1815,24 +1835,28 @@ namespace smtfd {
void assert_fd(expr* fml) { void assert_fd(expr* fml) {
expr_ref _fml(fml, m); expr_ref _fml(fml, m);
TRACE("smtfd", tout << mk_bounded_pp(fml, m, 3) << "\n";); TRACE("smtfd", tout << mk_bounded_pp(fml, m, 3) << "\n";);
SASSERT(!m_axioms.contains(fml));
m_axioms.push_back(fml);
_fml = abs(fml); _fml = abs(fml);
TRACE("smtfd", tout << mk_bounded_pp(_fml, m, 3) << "\n";);
m_fd_sat_solver->assert_expr(_fml); m_fd_sat_solver->assert_expr(_fml);
m_fd_core_solver->assert_expr(_fml); m_fd_core_solver->assert_expr(_fml);
flush_atom_defs(); flush_atom_defs();
} }
void block_core(expr_ref_vector const& core) { void block_core(expr_ref_vector const& core) {
assert_fd(m.mk_not(mk_and(core))); expr_ref fml(m.mk_not(mk_and(core)), m);
TRACE("smtfd", tout << "block:\n" << mk_bounded_pp(fml, m, 3) << "\n" << mk_bounded_pp(abs(fml), m, 3) << "\n";);
assert_fd(fml);
} }
#if 0
#if 0
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
init(); init();
flush_assertions(); flush_assertions();
lbool r; lbool r;
expr_ref_vector core(m); expr_ref_vector core(m);
while (true) { while (true) {
IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds << " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n"); IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat :rounds " << m_stats.m_num_rounds << " lemmas: " << m_stats.m_num_lemmas << " :qi " << m_stats.m_num_mbqi << ")\n");
m_stats.m_num_rounds++; m_stats.m_num_rounds++;
checkpoint(); checkpoint();
@ -1883,15 +1907,12 @@ namespace smtfd {
init(); init();
flush_assertions(); flush_assertions();
lbool r = l_undef; lbool r = l_undef;
expr_ref_vector core(m); expr_ref_vector core(m), axioms(m);
unsigned nt = m_toggles.size();
while (true) { while (true) {
IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat :rounds " << m_stats.m_num_rounds
<< " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n"); << " :lemmas " << m_stats.m_num_lemmas << " :qi " << m_stats.m_num_mbqi << ")\n");
m_stats.m_num_rounds++; m_stats.m_num_rounds++;
checkpoint(); checkpoint();
m_toggles.shrink(nt);
std::cout << "toggles: " << m_toggles << "\n";
// phase 1: check sat of abs // phase 1: check sat of abs
r = check_abs(num_assumptions, assumptions); r = check_abs(num_assumptions, assumptions);
@ -1944,22 +1965,27 @@ namespace smtfd {
unsigned round = 0; unsigned round = 0;
m_context.reset(m_model); m_context.reset(m_model);
while (true) { while (true) {
if (!m_context.add_theory_axioms(core, round)) {
expr_ref_vector terms(core);
terms.append(m_axioms);
if (!m_context.add_theory_axioms(terms, round)) {
break; break;
} }
if (m_context.empty()) { if (m_context.empty()) {
++round; ++round;
continue; continue;
} }
IF_VERBOSE(1, verbose_stream() << "(smtfd-round " << round << " " << m_context.size() << ")\n"); IF_VERBOSE(1, verbose_stream() << "(smtfd-round :round " << round << " :lemmas " << m_context.size() << ")\n");
round = 0; round = 0;
TRACE("smtfd_verbose", TRACE("smtfd_verbose",
for (expr* f : m_context) tout << "refine " << mk_bounded_pp(f, m, 3) << "\n"; for (expr* f : m_context) tout << "refine " << mk_bounded_pp(f, m, 3) << "\n";
m_context.display(tout);); m_context.display(tout););
for (expr* f : m_context) { for (expr* f : m_context) {
core.push_back(f); assert_fd(f);
} }
m_stats.m_num_lemmas += m_context.size(); m_stats.m_num_lemmas += m_context.size();
m_context.reset(m_model);
r = check_abs(core.size(), core.c_ptr()); r = check_abs(core.size(), core.c_ptr());
update_reason_unknown(r, m_fd_sat_solver); update_reason_unknown(r, m_fd_sat_solver);
switch (r) { switch (r) {
@ -2011,7 +2037,7 @@ namespace smtfd {
} }
st.update("smtfd-num-lemmas", m_stats.m_num_lemmas); st.update("smtfd-num-lemmas", m_stats.m_num_lemmas);
st.update("smtfd-num-rounds", m_stats.m_num_rounds); st.update("smtfd-num-rounds", m_stats.m_num_rounds);
st.update("smtfd-num-mbqi", m_stats.m_num_mbqi); st.update("smtfd-num-mbqi", m_stats.m_num_mbqi);
} }
void get_unsat_core(expr_ref_vector & r) override { void get_unsat_core(expr_ref_vector & r) override {
m_fd_sat_solver->get_unsat_core(r); m_fd_sat_solver->get_unsat_core(r);