mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

smtfd

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-08 18:14:28 +02:00
parent d3da161803
commit c22a17f430
2 changed files with 366 additions and 172 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/array_decl_plugin.h
View file

@ -149,6 +149,7 @@ public:
bool is_select(expr* n) const { return is_app_of(n, m_fid, OP_SELECT); } bool is_select(expr* n) const { return is_app_of(n, m_fid, OP_SELECT); }
bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); } bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); } bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
bool is_ext(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_EXT); }
bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); } bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); } bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); } bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }

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

@ -81,58 +81,41 @@
if not compatible: if not compatible:
lemmas += (args2 != args => select(t, args2) = select(A, args2)) lemmas += (args2 != args => select(t, args2) = select(A, args2))
for t in subterms(core) where t is const(k):
vk := M(abs(k))
vT := M(abs(t))
for v_args2 |-> v2, args2, t2 in table[vT]:
if vk != v2:
lemmas += (t = t2 => select(t2, args2) = k)
or lemmas += (select(t, args2) = k)
for t in subterms(core) where t is (lambda x . M), t is ground: for t in subterms(core) where t is (lambda x . M), t is ground:
vT := M(abs(t)) vT := M(abs(t))
for v_args2 |-> v2, args2, t2 in table[vT]: for v_args2 |-> v2, args2, t2 in table[vT]:
v1 := M(abs(M[args2/x])) v1 := M(abs(M[args2/x]))
if v1 != v2: if v1 != v2:
lemmas += (t = t2 => select(t2, args2) = M[args2/x]) lemmas += (select(t2, args2) = M[args2/x])
for t in subterms(core) where t is map(f, A, B, C): for t in subterms(core) where t is map(f, A, B, C), t is const:
similar to lambda similar to lambda
for A in array_terms(core): for A, B in array_terms(core):
// extensionality:
vA := M(abs(A))
B := table[vA].array
if B = nil:
table[vA].array := A
else:
// add if not already true:
lemmas += (select(A, delta(A,B)) = select(B, delta(A,B)) => A = B) lemmas += (select(A, delta(A,B)) = select(B, delta(A,B)) => A = B)
if AUF solver timed out and lemmas == []: if AUF solver returned unsat:
really call AUF solver on core
return sat or continue with adding !core
add abs(!core) to solver add abs(!core) to solver
add abs(lemmas) to solver add abs(lemmas) to solver
TBD: Note:
- extract UF model without relying on SMT
- hint to SMT solver using FD model (add equalities from FD model) - hint to SMT solver using FD model (add equalities from FD model)
- extensionality?
- abstractions for multiplication and other BV operations: - abstractions for multiplication and other BV operations:
- add ackerman reductions for BV - add ackerman reductions for BV
- commutativity? - commutativity?
- fix most bits using model, blast specialization. - fix most bits using model, blast specialization.
Z = X * Y Z = X * Y
X[range] = k1, Y[range] = k2 => Z = (k1++X') * (k2 ++ Y') X[range] = k1, Y[range] = k2 => Z = (k1++X') * (k2 ++ Y')
- do something about arithmetic? - abstract also equality
- add triangle lemmas whenever using equality chaining in lemmas.
- add equality resolution lemmas - add equality resolution lemmas
For core: v = t & phi(v) For core: v = t & phi(v)
and v = t occurs in several cores and v = t occurs in several cores
set core := phi(t/v) set core := phi(t/v)
- do something about arithmetic?
*/ */
@ -141,6 +124,7 @@ TBD:
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "ast/pb_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "tactic/tactic_exception.h" #include "tactic/tactic_exception.h"
#include "tactic/fd_solver/fd_solver.h" #include "tactic/fd_solver/fd_solver.h"
@ -156,6 +140,7 @@ namespace smtfd {
expr_ref_vector m_abs, m_rep, m_atoms, m_atom_defs; // abstraction and representation maps expr_ref_vector m_abs, m_rep, m_atoms, m_atom_defs; // abstraction and representation maps
array_util m_autil; array_util m_autil;
bv_util m_butil; bv_util m_butil;
pb_util m_pb;
ptr_vector<expr> m_args, m_todo; ptr_vector<expr> m_args, m_todo;
unsigned m_nv; unsigned m_nv;
unsigned_vector m_abs_trail, m_rep_trail, m_nv_trail; unsigned_vector m_abs_trail, m_rep_trail, m_nv_trail;
@ -223,6 +208,7 @@ namespace smtfd {
m_atom_defs(m), m_atom_defs(m),
m_autil(m), m_autil(m),
m_butil(m), m_butil(m),
m_pb(m),
m_nv(0) m_nv(0)
{ {
abs(m.mk_true()); abs(m.mk_true());
@ -267,6 +253,7 @@ namespace smtfd {
m_todo.push_back(e); m_todo.push_back(e);
family_id bvfid = m_butil.get_fid(); family_id bvfid = m_butil.get_fid();
family_id bfid = m.get_basic_family_id(); family_id bfid = m.get_basic_family_id();
family_id pbfid = m_pb.get_family_id();
while (!m_todo.empty()) { while (!m_todo.empty()) {
expr* t = m_todo.back(); expr* t = m_todo.back();
r = try_abs(t); r = try_abs(t);
@ -293,10 +280,13 @@ namespace smtfd {
if (m.is_eq(a)) { if (m.is_eq(a)) {
r = m.mk_eq(m_args.get(0), m_args.get(1)); r = m.mk_eq(m_args.get(0), m_args.get(1));
} }
else if (m.is_distinct(a)) {
r = m.mk_distinct(m_args.size(), m_args.c_ptr());
}
else if (m.is_ite(a)) { else if (m.is_ite(a)) {
r = m.mk_ite(m_args.get(0), m_args.get(1), m_args.get(2)); r = m.mk_ite(m_args.get(0), m_args.get(1), m_args.get(2));
} }
else if (bvfid == fid || bfid == fid) { else if (bvfid == fid || bfid == fid || pbfid == fid) {
r = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr()); r = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
} }
else if (is_uninterp_const(t) && m.is_bool(t)) { else if (is_uninterp_const(t) && m.is_bool(t)) {
@ -330,7 +320,8 @@ namespace smtfd {
expr* r = try_rep(e); expr* r = try_rep(e);
if (r) return r; if (r) return r;
VERIFY(m.is_not(e, r)); VERIFY(m.is_not(e, r));
r = m.mk_not(try_rep(r)); r = try_rep(r);
r = m.mk_not(r);
abs(r); abs(r);
return r; return r;
} }
@ -344,6 +335,36 @@ namespace smtfd {
class theory_plugin; class theory_plugin;
class plugin_context {
expr_ref_vector m_lemmas;
unsigned m_max_lemmas;
ptr_vector<theory_plugin> m_plugins;
public:
plugin_context(ast_manager& m, unsigned max):
m_lemmas(m),
m_max_lemmas(max)
{}
void add(expr* f) { m_lemmas.push_back(f); }
ast_manager& get_manager() { return m_lemmas.get_manager(); }
bool at_max() const { return m_lemmas.size() >= m_max_lemmas; }
expr_ref_vector::iterator begin() { return m_lemmas.begin(); }
expr_ref_vector::iterator end() { return m_lemmas.end(); }
unsigned size() const { return m_lemmas.size(); }
bool empty() const { return m_lemmas.empty(); }
void add_plugin(theory_plugin* p) { m_plugins.push_back(p); }
expr_ref model_value(expr* t);
expr_ref model_value(sort* s);
bool term_covered(expr* t);
bool sort_covered(sort* s);
void populate_model(model_ref& mdl, expr_ref_vector const& core);
};
struct f_app_eq { struct f_app_eq {
theory_plugin& p; theory_plugin& p;
f_app_eq(theory_plugin& p):p(p) {} f_app_eq(theory_plugin& p):p(p) {}
@ -363,7 +384,7 @@ namespace smtfd {
typedef hashtable<f_app, f_app_hash, f_app_eq> table; typedef hashtable<f_app, f_app_hash, f_app_eq> table;
ast_manager& m; ast_manager& m;
smtfd_abs& m_abs; smtfd_abs& m_abs;
expr_ref_vector& m_lemmas; plugin_context& m_context;
model_ref m_model; model_ref m_model;
expr_ref_vector m_values; expr_ref_vector m_values;
ast_ref_vector m_pinned; ast_ref_vector m_pinned;
@ -391,17 +412,19 @@ namespace smtfd {
} }
public: public:
theory_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl) : theory_plugin(smtfd_abs& a, plugin_context& context, model_ref& mdl) :
m(lemmas.get_manager()), m(context.get_manager()),
m_abs(a), m_abs(a),
m_lemmas(lemmas), m_context(context),
m_model(mdl), m_model(mdl),
m_values(m), m_values(m),
m_pinned(m), m_pinned(m),
m_args(m), m_args2(m), m_vargs(m), m_args(m), m_args2(m), m_vargs(m),
m_eq(*this), m_eq(*this),
m_hash(*this) m_hash(*this)
{} {
m_context.add_plugin(this);
}
table& ast2table(ast* f) { table& ast2table(ast* f) {
unsigned idx = 0; unsigned idx = 0;
@ -421,7 +444,7 @@ namespace smtfd {
void add_lemma(expr* fml) { void add_lemma(expr* fml) {
expr_ref _fml(fml, m); expr_ref _fml(fml, m);
TRACE("smtfd", tout << _fml << "\n";); TRACE("smtfd", tout << _fml << "\n";);
m_lemmas.push_back(m_abs.abs(fml)); m_context.add(m_abs.abs(fml));
} }
expr_ref eval_abs(expr* t) { return (*m_model)(m_abs.abs(t)); } expr_ref eval_abs(expr* t) { return (*m_model)(m_abs.abs(t)); }
@ -457,12 +480,56 @@ namespace smtfd {
add_lemma(m.mk_implies(mk_and(m_args), m.mk_eq(f1.m_t, f2.m_t))); add_lemma(m.mk_implies(mk_and(m_args), m.mk_eq(f1.m_t, f2.m_t)));
} }
expr_ref model_value(expr* t) { return m_context.model_value(t); }
expr_ref model_value(sort* s) { return m_context.model_value(s); }
virtual void check_term(expr* t, unsigned round) = 0; virtual void check_term(expr* t, unsigned round) = 0;
virtual expr_ref model_value_core(expr* t) = 0;
virtual expr_ref model_value_core(sort* s) = 0;
virtual bool term_covered(expr* t) = 0; virtual bool term_covered(expr* t) = 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& core) {}
}; };
expr_ref plugin_context::model_value(expr* t) {
expr_ref r(get_manager());
for (theory_plugin* p : m_plugins) {
r = p->model_value_core(t);
if (r) break;
}
return r;
}
expr_ref plugin_context::model_value(sort* s) {
expr_ref r(get_manager());
for (theory_plugin* p : m_plugins) {
r = p->model_value_core(s);
if (r) break;
}
return r;
}
bool plugin_context::sort_covered(sort* s) {
for (theory_plugin* p : m_plugins) {
if (p->sort_covered(s)) return true;
}
return false;
}
bool plugin_context::term_covered(expr* t) {
for (theory_plugin* p : m_plugins) {
if (p->term_covered(t)) return true;
}
return false;
}
void plugin_context::populate_model(model_ref& mdl, expr_ref_vector const& core) {
for (theory_plugin* p : m_plugins) {
p->populate_model(mdl, core);
}
}
bool f_app_eq::operator()(f_app const& a, f_app const& b) const { bool f_app_eq::operator()(f_app const& a, f_app const& b) const {
if (a.m_f != b.m_f) if (a.m_f != b.m_f)
return false; return false;
@ -481,58 +548,96 @@ namespace smtfd {
class basic_plugin : public theory_plugin { class basic_plugin : public theory_plugin {
public: public:
basic_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl): basic_plugin(smtfd_abs& a, plugin_context& context, model_ref& mdl):
theory_plugin(a, lemmas, mdl) theory_plugin(a, context, mdl)
{} {}
void check_term(expr* t, unsigned round) override { } void check_term(expr* t, unsigned round) override { }
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); }
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& core) override { }
#if 0 expr_ref model_value_core(expr* t) override { return m.is_bool(t) ? (*m_model)(m_abs.abs(t)) : expr_ref(m); }
// not needed expr_ref model_value_core(sort* s) override { return m.is_bool(s) ? expr_ref(m.mk_false(), m) : expr_ref(m); }
for (expr* t : subterms(core)) { };
if (is_uninterp_const(t) && m.is_bool(t)) {
expr_ref val = eval_abs(t); class pb_plugin : public theory_plugin {
mdl->register_decl(to_app(t)->get_decl(), val); pb_util m_pb;
} public:
} pb_plugin(smtfd_abs& a, plugin_context& context, model_ref& mdl):
#endif theory_plugin(a, context, mdl),
} m_pb(m)
{}
void check_term(expr* t, unsigned round) override { }
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); }
unsigned max_rounds() override { return 0; }
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { }
expr_ref model_value_core(expr* t) override { return expr_ref(m); }
expr_ref model_value_core(sort* s) override { return expr_ref(m); }
}; };
class bv_plugin : public theory_plugin { class bv_plugin : public theory_plugin {
bv_util m_butil; bv_util m_butil;
public: public:
bv_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl): bv_plugin(smtfd_abs& a, plugin_context& context, model_ref& mdl):
theory_plugin(a, lemmas, mdl), theory_plugin(a, context, mdl),
m_butil(m) m_butil(m)
{} {}
void check_term(expr* t, unsigned round) override { } void check_term(expr* t, unsigned round) override { }
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); }
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& core) override { }
#if 0 expr_ref model_value_core(expr* t) override { return m_butil.is_bv(t) ? (*m_model)(m_abs.abs(t)) : expr_ref(m); }
// not needed as model for abstraction already knows value. 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); }
for (expr* t : subterms(core)) {
if (is_uninterp_const(t) && m_butil.is_bv(t)) {
expr_ref val = eval_abs(t);
mdl->register_decl(to_app(t)->get_decl(), val);
}
}
#endif
}
}; };
class uf_plugin : public theory_plugin { class uf_plugin : public theory_plugin {
expr_ref_vector m_pinned;
obj_map<sort, unsigned> m_sort2idx;
typedef obj_map<expr, expr*> val2elem_t;
scoped_ptr_vector<val2elem_t> m_val2elem;
val2elem_t& get_table(sort* s) {
unsigned idx = 0;
if (!m_sort2idx.find(s, idx)) {
idx = m_val2elem.size();
m_sort2idx.insert(s, idx);
m_val2elem.push_back(alloc(val2elem_t));
}
return *m_val2elem[idx];
}
bool is_uf(expr* t) { bool is_uf(expr* t) {
return is_app(t) && to_app(t)->get_family_id() == null_family_id && to_app(t)->get_num_args() > 0; return is_app(t) && to_app(t)->get_family_id() == null_family_id && to_app(t)->get_num_args() > 0;
} }
val2elem_t& ensure_table(sort* s) {
val2elem_t& v2e = get_table(s);
if (v2e.empty()) {
v2e.insert(m.mk_true(), nullptr);
}
ptr_vector<expr> keys, values;
for (auto const& kv : v2e) {
if (kv.m_value) return v2e;
keys.push_back(kv.m_key);
values.push_back(m.mk_model_value(values.size(), s));
m_pinned.push_back(values.back());
}
m_model->register_usort(s, values.size(), values.c_ptr());
for (unsigned i = 0; i < keys.size(); ++i) {
v2e.insert(keys[i], values[i]);
}
return v2e;
}
public: public:
uf_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl): uf_plugin(smtfd_abs& a, plugin_context& context, model_ref& mdl):
theory_plugin(a, lemmas, mdl) theory_plugin(a, context, mdl),
m_pinned(m)
{} {}
void check_term(expr* t, unsigned round) override { void check_term(expr* t, unsigned round) override {
@ -541,9 +646,22 @@ namespace smtfd {
} }
bool term_covered(expr* t) override { bool term_covered(expr* t) override {
sort* s = m.get_sort(t);
if (sort_covered(s)) {
val2elem_t& v2e = get_table(s);
expr_ref v = eval_abs(t);
if (!v2e.contains(v)) {
m_pinned.push_back(v);
v2e.insert(v, nullptr);
}
}
return is_uf(t) || is_uninterp_const(t); return is_uf(t) || is_uninterp_const(t);
} }
bool sort_covered(sort* s) override {
return s->get_family_id() == m.get_user_sort_family_id();
}
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& core) override {
@ -559,13 +677,35 @@ namespace smtfd {
} }
args.reset(); args.reset();
for (expr* arg : *f.m_t) { for (expr* arg : *f.m_t) {
args.push_back(eval_abs(arg)); args.push_back(model_value(arg));
} }
expr_ref val = eval_abs(f.m_t); expr_ref val = model_value(f.m_t);
fi->insert_new_entry(args.c_ptr(),val); fi->insert_new_entry(args.c_ptr(),val);
} }
mdl->register_decl(fn, fi); mdl->register_decl(fn, fi);
} }
for (expr* t : subterms(core)) {
if (is_uninterp_const(t) && sort_covered(m.get_sort(t))) {
expr_ref val = model_value(t);
mdl->register_decl(to_app(t)->get_decl(), val);
}
}
}
expr_ref model_value_core(expr* t) override {
sort* s = m.get_sort(t);
if (sort_covered(s)) {
auto& v2e = ensure_table(s);
return expr_ref(v2e[eval_abs(t)], m);
}
return expr_ref(m);
}
expr_ref model_value_core(sort* s) override {
if (sort_covered(s)) {
auto& v2e = ensure_table(s);
return expr_ref(v2e.begin()->m_value, m);
}
return expr_ref(m);
} }
}; };
@ -631,6 +771,9 @@ namespace smtfd {
for (auto& fA : tA) { for (auto& fA : tA) {
f_app fT; f_app fT;
if (m_context.at_max()) {
break;
}
if (tT.find(fA, fT) && value_of(fA) != value_of(fT) && !eq(m_vargs, fA)) { if (tT.find(fA, fT) && value_of(fA) != value_of(fT) && !eq(m_vargs, fA)) {
SASSERT(same_array_sort(fA, fT)); SASSERT(same_array_sort(fA, fT));
m_args2.reset(); m_args2.reset();
@ -661,6 +804,8 @@ namespace smtfd {
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;
if (m_context.at_max())
break;
m_args.reset(); m_args.reset();
m_args.append(f.m_t->get_num_args(), f.m_t->get_args()); m_args.append(f.m_t->get_num_args(), f.m_t->get_args());
m_args[0] = t; m_args[0] = t;
@ -678,8 +823,8 @@ namespace smtfd {
bool eq(expr_ref_vector const& args, f_app const& f) { bool eq(expr_ref_vector const& args, f_app const& f) {
SASSERT(args.size() == f.m_t->get_num_args()); SASSERT(args.size() == f.m_t->get_num_args());
for (unsigned i = 0, sz = args.size(); i < sz; ++i) { for (unsigned i = args.size(); i-- > 0; ) {
if (args.get(i) != m_values.get(f.m_val_offset + 1)) if (args.get(i) != m_values.get(f.m_val_offset + i))
return false; return false;
} }
return true; return true;
@ -694,15 +839,13 @@ namespace smtfd {
return mk_and(r); return mk_and(r);
} }
#if 0
// TBD, the following does not make sense to use as the lemmas are true given the way they are defined.
bool same_table(table const& t1, table const& t2) { bool same_table(table const& t1, table const& t2) {
if (t1.size() != t2.size()) { if (t1.size() != t2.size()) {
return false; return false;
} }
for (f_app const& f1 : t1) { for (f_app const& f1 : t1) {
f_app f2;
if (!t2.find(f1, f2) || value_of(f1) != value_of(f2)) { if (!t2.find(f1, f2) || value_of(f1) != value_of(f2)) {
return false; return false;
} }
@ -710,9 +853,11 @@ namespace smtfd {
return true; return true;
} }
typedef obj_map<expr, expr*> val2array_map; bool same_table(expr* v1, expr* v2) {
return same_table(ast2table(v1), ast2table(v2));
}
void check_extensionality(expr* a, expr* b) { void enforce_extensionality(expr* a, expr* b) {
sort* s = m.get_sort(a); sort* s = m.get_sort(a);
unsigned arity = get_array_arity(s); unsigned arity = get_array_arity(s);
expr_ref_vector args(m); expr_ref_vector args(m);
@ -723,58 +868,28 @@ namespace smtfd {
expr_ref a1(m_autil.mk_select(args), m); expr_ref a1(m_autil.mk_select(args), m);
args[0] = b; args[0] = b;
expr_ref b1(m_autil.mk_select(args), m); expr_ref b1(m_autil.mk_select(args), m);
expr_ref vA = eval_abs(a1);
expr_ref vB = eval_abs(b1);
if (vA == vB) {
add_lemma(m.mk_implies(m.mk_eq(a1, b1), m.mk_eq(a, b))); add_lemma(m.mk_implies(m.mk_eq(a1, b1), m.mk_eq(a, b)));
} }
}
void global_check(expr_ref_vector const& core) {
obj_map<sort, val2array_map*> sort2val2array;
expr_ref_vector pinned(m);
scoped_ptr_vector<val2array_map> maps;
for (expr* t : subterms(core)) {
if (m_autil.is_array(t)) {
sort* s = m.get_sort(t);
val2array_map* v2a = nullptr;
if (!sort2val2array.find(s, v2a)) {
v2a = alloc(val2array_map);
sort2val2array.insert(s, v2a);
maps.push_back(v2a);
}
expr* a = nullptr;
expr_ref v = eval_abs(t);
pinned.push_back(v);
if (v2a->find(v, a)) {
check_extensionality(a, t);
}
else {
v2a->insert(v, t);
}
}
}
}
#endif
expr_ref mk_array_value(table& t) { expr_ref mk_array_value(table& t) {
expr_ref value(m); expr_ref value(m), default_value(m);
SASSERT(!t.empty()); SASSERT(!t.empty());
expr_ref_vector args(m); expr_ref_vector args(m);
for (f_app const& f : t) { for (f_app const& f : t) {
SASSERT(m_autil.is_select(f.m_t)); SASSERT(m_autil.is_select(f.m_t));
expr_ref v = model_value(f.m_t);
if (!value) { if (!value) {
sort* s = m.get_sort(f.m_t->get_arg(0)); sort* s = m.get_sort(f.m_t->get_arg(0));
value = m_autil.mk_const_array(s, eval_abs(f.m_t)); default_value = v;
value = m_autil.mk_const_array(s, default_value);
} }
else { else if (v != default_value) {
args.reset(); args.reset();
args.push_back(value); args.push_back(value);
for (unsigned i = 1; i < f.m_t->get_num_args(); ++i) { for (unsigned i = 1; i < f.m_t->get_num_args(); ++i) {
args.push_back(eval_abs(f.m_t->get_arg(i))); args.push_back(model_value(f.m_t->get_arg(i)));
} }
args.push_back(eval_abs(f.m_t)); args.push_back(v);
value = m_autil.mk_store(args); value = m_autil.mk_store(args);
} }
} }
@ -783,8 +898,8 @@ namespace smtfd {
public: public:
a_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl): a_plugin(smtfd_abs& a, plugin_context& context, model_ref& mdl):
theory_plugin(a, lemmas, mdl), theory_plugin(a, context, mdl),
m_autil(m), m_autil(m),
m_rewriter(m) m_rewriter(m)
{} {}
@ -824,24 +939,95 @@ namespace smtfd {
m_autil.is_store(t) || m_autil.is_store(t) ||
m_autil.is_select(t) || m_autil.is_select(t) ||
m_autil.is_map(t) || m_autil.is_map(t) ||
m_autil.is_ext(t) ||
m_autil.is_const(t); m_autil.is_const(t);
} }
bool sort_covered(sort* s) override {
if (!m_autil.is_array(s)) {
return false;
}
if (!m_context.sort_covered(get_array_range(s))) {
return false;
}
for (unsigned i = 0; i < get_array_arity(s); ++i) {
if (!m_context.sort_covered(get_array_domain(s, i)))
return false;
}
return true;
}
expr_ref model_value_core(expr* t) override {
if (m_autil.is_array(t)) {
expr_ref vT = eval_abs(t);
table& tb = ast2table(vT);
if (tb.empty()) {
return model_value_core(m.get_sort(t));
}
else {
return mk_array_value(tb);
}
}
return expr_ref(m);
}
expr_ref model_value_core(sort* s) override {
if (m_autil.is_array(s)) {
return expr_ref(m_autil.mk_const_array(s, model_value(get_array_range(s))), m);
}
return expr_ref(m);
}
void populate_model(model_ref& mdl, expr_ref_vector const& core) override { void populate_model(model_ref& mdl, expr_ref_vector const& core) override {
for (expr* t : subterms(core)) { for (expr* t : subterms(core)) {
if (is_uninterp_const(t) && m_autil.is_array(t)) { if (is_uninterp_const(t) && m_autil.is_array(t)) {
expr_ref vT = eval_abs(t); mdl->register_decl(to_app(t)->get_decl(), model_value_core(t));
table& tb = ast2table(vT);
if (!tb.empty()) {
expr_ref val = mk_array_value(tb);
mdl->register_decl(to_app(t)->get_decl(), val);
}
} }
} }
} }
unsigned max_rounds() override { return 2; } unsigned max_rounds() override { return 2; }
void global_check(expr_ref_vector const& core) {
expr_mark seen;
expr_ref_vector shared(m), sharedvals(m);
for (expr* t : subterms(core)) {
if (!is_app(t)) continue;
app* a = to_app(t);
unsigned offset = 0;
if (m_autil.is_select(t) || m_autil.is_store(t)) {
offset = 1;
}
else if (m_autil.is_map(t)) {
continue;
}
for (unsigned i = a->get_num_args(); i-- > offset; ) {
expr* arg = a->get_arg(i);
if (m_autil.is_array(arg) && !seen.is_marked(arg)) {
shared.push_back(arg);
seen.mark(arg, true);
}
}
}
for (expr* s : shared) {
sharedvals.push_back(eval_abs(s));
}
for (unsigned i = 0; !m_context.at_max() && i < shared.size(); ++i) {
expr* s1 = shared.get(i);
expr* v1 = sharedvals.get(i);
for (unsigned j = i + 1; !m_context.at_max() && j < shared.size(); ++j) {
expr* s2 = shared.get(j);
expr* v2 = sharedvals.get(j);
if (v1 != v2 && m.get_sort(s1) == m.get_sort(s2) && same_table(v1, v2)) {
enforce_extensionality(s1, s2);
}
}
}
}
}; };
struct stats { struct stats {
@ -853,7 +1039,8 @@ namespace smtfd {
class solver : public solver_na2as { class solver : public solver_na2as {
ast_manager& m; ast_manager& m;
smtfd_abs m_abs; smtfd_abs m_abs;
ref<::solver> m_fd_solver; ref<::solver> m_fd_sat_solver;
ref<::solver> m_fd_core_solver;
ref<::solver> m_smt_solver; ref<::solver> m_smt_solver;
expr_ref_vector m_assertions; expr_ref_vector m_assertions;
unsigned_vector m_assertions_lim; unsigned_vector m_assertions_lim;
@ -865,14 +1052,13 @@ namespace smtfd {
std::string m_reason_unknown; std::string m_reason_unknown;
unsigned m_max_lemmas; unsigned m_max_lemmas;
stats m_stats; stats m_stats;
unsigned m_useful_smt;
unsigned m_non_useful_smt;
unsigned m_max_conflicts; unsigned m_max_conflicts;
void set_delay_simplify() { void set_delay_simplify() {
params_ref p; params_ref p;
p.set_uint("simplify.delay", 10000); p.set_uint("simplify.delay", 10000);
m_fd_solver->updt_params(p); m_fd_sat_solver->updt_params(p);
m_fd_core_solver->updt_params(p);
} }
void flush_assertions() { void flush_assertions() {
@ -896,10 +1082,9 @@ namespace smtfd {
init_assumptions(num_assumptions, assumptions, asms); init_assumptions(num_assumptions, assumptions, asms);
TRACE("smtfd", display(tout << asms);); TRACE("smtfd", display(tout << asms););
SASSERT(asms.contains(m_toggle)); SASSERT(asms.contains(m_toggle));
m_fd_sat_solver->assert_expr(m_toggle);
// test: m_fd_solver->assert_expr(m_toggle); lbool r = m_fd_sat_solver->check_sat(asms);
lbool r = m_fd_solver->check_sat(asms); update_reason_unknown(r, m_fd_sat_solver);
update_reason_unknown(r, m_fd_solver);
set_delay_simplify(); set_delay_simplify();
return r; return r;
} }
@ -907,17 +1092,17 @@ namespace smtfd {
// not necessarily prime // not necessarily prime
lbool get_prime_implicate(unsigned num_assumptions, expr * const * assumptions, expr_ref_vector& core) { lbool get_prime_implicate(unsigned num_assumptions, expr * const * assumptions, expr_ref_vector& core) {
expr_ref_vector asms(m); expr_ref_vector asms(m);
m_fd_solver->get_model(m_model); m_fd_sat_solver->get_model(m_model);
init_literals(num_assumptions, assumptions, asms); init_literals(num_assumptions, assumptions, asms);
TRACE("smtfd", display(tout << asms);); TRACE("smtfd", display(tout << asms););
SASSERT(asms.contains(m_not_toggle)); SASSERT(asms.contains(m_not_toggle));
lbool r = m_fd_solver->check_sat(asms); lbool r = m_fd_core_solver->check_sat(asms);
update_reason_unknown(r, m_fd_solver); update_reason_unknown(r, m_fd_core_solver);
if (r == l_false) { if (r == l_false) {
m_fd_solver->get_unsat_core(core); m_fd_core_solver->get_unsat_core(core);
TRACE("smtfd", display(tout << core);); TRACE("smtfd", display(tout << core););
core.erase(m_not_toggle.get()); core.erase(m_not_toggle.get());
SASSERT(!asms.contains(m_not_toggle)); SASSERT(asms.contains(m_not_toggle));
SASSERT(!asms.contains(m_toggle)); SASSERT(!asms.contains(m_toggle));
} }
return r; return r;
@ -939,17 +1124,14 @@ namespace smtfd {
TRACE("smtfd", display(tout << core);); TRACE("smtfd", display(tout << core););
unsigned sz1 = core.size(); unsigned sz1 = core.size();
if (sz1 < sz0) { if (sz1 < sz0) {
++m_useful_smt;
m_max_conflicts += 10; m_max_conflicts += 10;
} }
else { else {
++m_non_useful_smt;
if (m_max_conflicts > 20) m_max_conflicts -= 5; if (m_max_conflicts > 20) m_max_conflicts -= 5;
} }
break; break;
} }
case l_undef: case l_undef:
++m_non_useful_smt;
if (m_max_conflicts > 20) m_max_conflicts -= 5; if (m_max_conflicts > 20) m_max_conflicts -= 5;
break; break;
case l_true: case l_true:
@ -960,43 +1142,43 @@ namespace smtfd {
} }
bool add_theory_lemmas(expr_ref_vector const& core) { bool add_theory_lemmas(expr_ref_vector const& core) {
expr_ref_vector lemmas(m); plugin_context context(m, m_max_lemmas);
a_plugin ap(m_abs, lemmas, m_model.get()); a_plugin ap(m_abs, context, m_model);
uf_plugin uf(m_abs, lemmas, m_model.get()); uf_plugin uf(m_abs, context, m_model);
unsigned max_rounds = std::max(ap.max_rounds(), uf.max_rounds()); unsigned max_rounds = std::max(ap.max_rounds(), uf.max_rounds());
for (unsigned round = 0; round < max_rounds; ++round) { for (unsigned round = 0; round < max_rounds; ++round) {
for (expr* t : subterms(core)) { for (expr* t : subterms(core)) {
if (lemmas.size() >= m_max_lemmas) if (context.at_max()) break;
break;
ap.check_term(t, round); ap.check_term(t, round);
uf.check_term(t, round); uf.check_term(t, round);
} }
} }
for (expr* f : lemmas) { ap.global_check(core);
for (expr* f : context) {
IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(rep(f), m) << "\n"); IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(rep(f), m) << "\n");
assert_fd(f); assert_fd(f);
} }
m_stats.m_num_lemmas += lemmas.size(); m_stats.m_num_lemmas += context.size();
return !lemmas.empty(); if (context.at_max()) {
m_max_lemmas = (3*m_max_lemmas)/2;
}
return !context.empty();
} }
bool is_decided_sat(expr_ref_vector const& core) { bool is_decided_sat(expr_ref_vector const& core) {
expr_ref_vector lemmas(m); plugin_context context(m, m_max_lemmas);
uf_plugin uf(m_abs, lemmas, m_model.get()); uf_plugin uf(m_abs, context, m_model);
a_plugin ap(m_abs, lemmas, m_model.get()); a_plugin ap(m_abs, context, m_model);
bv_plugin bv(m_abs, lemmas, m_model.get()); bv_plugin bv(m_abs, context, m_model);
basic_plugin bs(m_abs, lemmas, m_model.get()); basic_plugin bs(m_abs, context, m_model);
pb_plugin pb(m_abs, context, m_model);
for (expr* t : subterms(core)) { for (expr* t : subterms(core)) {
if (!uf.term_covered(t) && !ap.term_covered(t) && !bv.term_covered(t) && !bs.term_covered(t)) { if (!context.term_covered(t) || !context.sort_covered(m.get_sort(t))) {
return false; return false;
} }
} }
context.populate_model(m_model, core);
uf.populate_model(m_model, core);
ap.populate_model(m_model, core);
bv.populate_model(m_model, core);
bs.populate_model(m_model, core);
return true; return true;
} }
@ -1038,16 +1220,18 @@ 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() {
if (!m_fd_solver) { if (!m_fd_sat_solver) {
m_fd_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_smt_solver = mk_smt_solver(m, get_params(), symbol::null); m_smt_solver = mk_smt_solver(m, get_params(), symbol::null);
m_smt_solver->updt_params(get_params()); m_smt_solver->updt_params(get_params());
} }
} }
std::ostream& display(std::ostream& out, unsigned n = 0, expr * const * assumptions = nullptr) const override { std::ostream& display(std::ostream& out, unsigned n = 0, expr * const * assumptions = nullptr) const override {
if (!m_fd_solver) return out; if (!m_fd_sat_solver) return out;
m_fd_solver->display(out); m_fd_sat_solver->display(out);
m_fd_core_solver->display(out);
m_smt_solver->display(out); m_smt_solver->display(out);
out << m_assumptions << "\n"; out << m_assumptions << "\n";
m_abs.display(out); m_abs.display(out);
@ -1068,8 +1252,6 @@ namespace smtfd {
m_toggles(m), m_toggles(m),
m_toggle(m.mk_true(), m), m_toggle(m.mk_true(), m),
m_not_toggle(m.mk_false(), m), m_not_toggle(m.mk_false(), m),
m_useful_smt(0),
m_non_useful_smt(0),
m_max_conflicts(50) m_max_conflicts(50)
{ {
updt_params(p); updt_params(p);
@ -1080,7 +1262,8 @@ namespace smtfd {
::solver* translate(ast_manager& dst_m, params_ref const& p) override { ::solver* translate(ast_manager& dst_m, params_ref const& p) override {
solver* result = alloc(solver, dst_m, p); solver* result = alloc(solver, dst_m, p);
if (m_smt_solver) result->m_smt_solver = m_smt_solver->translate(dst_m, p); if (m_smt_solver) result->m_smt_solver = m_smt_solver->translate(dst_m, p);
if (m_fd_solver) result->m_fd_solver = m_fd_solver->translate(dst_m, p); if (m_fd_sat_solver) result->m_fd_sat_solver = m_fd_sat_solver->translate(dst_m, p);
if (m_fd_core_solver) result->m_fd_core_solver = m_fd_core_solver->translate(dst_m, p);
return result; return result;
} }
@ -1093,13 +1276,15 @@ namespace smtfd {
flush_assertions(); flush_assertions();
m_toggles.push_back(m_toggle); m_toggles.push_back(m_toggle);
m_abs.push(); m_abs.push();
m_fd_solver->push(); m_fd_sat_solver->push();
m_fd_core_solver->push();
m_smt_solver->push(); m_smt_solver->push();
m_assertions_lim.push_back(m_assertions.size()); m_assertions_lim.push_back(m_assertions.size());
} }
void pop_core(unsigned n) override { void pop_core(unsigned n) override {
m_fd_solver->pop(n); m_fd_sat_solver->pop(n);
m_fd_core_solver->pop(n);
m_smt_solver->pop(n); m_smt_solver->pop(n);
m_abs.pop(n); m_abs.pop(n);
m_toggle = m_toggles.get(m_toggles.size() - n); m_toggle = m_toggles.get(m_toggles.size() - n);
@ -1111,9 +1296,11 @@ namespace smtfd {
} }
void assert_fd(expr* fml) { void assert_fd(expr* fml) {
m_fd_solver->assert_expr(fml); m_fd_sat_solver->assert_expr(fml);
m_fd_core_solver->assert_expr(fml);
for (expr* f : m_abs.atom_defs()) { for (expr* f : m_abs.atom_defs()) {
m_fd_solver->assert_expr(f); m_fd_sat_solver->assert_expr(f);
m_fd_core_solver->assert_expr(f);
} }
m_abs.reset_atom_defs(); m_abs.reset_atom_defs();
} }
@ -1150,11 +1337,14 @@ namespace smtfd {
if (r == l_false) { if (r == l_false) {
assert_fd(m.mk_not(mk_and(abs(core)))); assert_fd(m.mk_not(mk_and(abs(core))));
} }
if (!add_theory_lemmas(core) && r == l_undef) { if (add_theory_lemmas(core)) {
continue;
}
if (r == l_undef) {
if (is_decided_sat(core)) { if (is_decided_sat(core)) {
return l_true; return l_true;
} }
m_max_conflicts *= 2; m_max_conflicts = UINT_MAX;
} }
} }
@ -1163,8 +1353,9 @@ namespace smtfd {
void updt_params(params_ref const & p) override { void updt_params(params_ref const & p) override {
::solver::updt_params(p); ::solver::updt_params(p);
if (m_fd_solver) { if (m_fd_sat_solver) {
m_fd_solver->updt_params(p); m_fd_sat_solver->updt_params(p);
m_fd_core_solver->updt_params(p);
m_smt_solver->updt_params(p); m_smt_solver->updt_params(p);
} }
m_max_lemmas = p.get_uint("max-lemmas", 100); m_max_lemmas = p.get_uint("max-lemmas", 100);
@ -1173,20 +1364,22 @@ namespace smtfd {
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
init(); init();
m_smt_solver->collect_param_descrs(r); m_smt_solver->collect_param_descrs(r);
m_fd_solver->collect_param_descrs(r); m_fd_sat_solver->collect_param_descrs(r);
m_fd_core_solver->collect_param_descrs(r);
r.insert("max-lemmas", CPK_UINT, "maximal number of lemmas per round", "10"); r.insert("max-lemmas", CPK_UINT, "maximal number of lemmas per round", "10");
} }
void set_produce_models(bool f) override { } void set_produce_models(bool f) override { }
void set_progress_callback(progress_callback * callback) override { } void set_progress_callback(progress_callback * callback) override { }
void collect_statistics(statistics & st) const override { void collect_statistics(statistics & st) const override {
m_fd_solver->collect_statistics(st); m_fd_sat_solver->collect_statistics(st);
m_fd_core_solver->collect_statistics(st);
m_smt_solver->collect_statistics(st); m_smt_solver->collect_statistics(st);
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);
} }
void get_unsat_core(expr_ref_vector & r) override { void get_unsat_core(expr_ref_vector & r) override {
m_fd_solver->get_unsat_core(r); m_fd_sat_solver->get_unsat_core(r);
r.erase(m_toggle.get()); r.erase(m_toggle.get());
rep(r); rep(r);
} }