mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-25 00:12:34 +00:00
Code Activity

Start resolving merge conflicts with master branch

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-15 04:14:50 +00:00 • committed by GitHub
commit dcf81a2592
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1020 changed files with 80693 additions and 20317 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/CMakeLists.txt
View file

@ -56,6 +56,8 @@ z3_add_component(smt
theory_char.cpp
theory_datatype.cpp
theory_dense_diff_logic.cpp
theory_finite_set.cpp
theory_finite_set_size.cpp
theory_diff_logic.cpp
theory_dl.cpp
theory_dummy.cpp

8
src/smt/arith_eq_adapter.cpp
View file

@ -87,8 +87,8 @@ namespace smt {
tout << mk_ismt2_pp(n1->get_expr(), m) << "\n" << mk_ismt2_pp(n2->get_expr(), m) << "\n";);
if (n1->get_owner_id() > n2->get_owner_id())
std::swap(n1, n2);
app * t1 = n1->get_expr();
app * t2 = n2->get_expr();
expr * t1 = n1->get_expr();
expr * t2 = n2->get_expr();
if (m.are_distinct(t1, t2)) {
expr_ref eq(m.mk_eq(t1, t2), m);
ctx.internalize(eq, true);
@ -233,7 +233,7 @@ namespace smt {
void arith_eq_adapter::new_eq_eh(theory_var v1, theory_var v2) {
TRACE(arith_eq_adapter, tout << "v" << v1 << " = v" << v2 << " #" << get_enode(v1)->get_owner_id() << " = #" << get_enode(v2)->get_owner_id() << "\n";);
TRACE(arith_eq_adapter_bug, tout << mk_bounded_pp(get_enode(v1)->get_expr(), get_manager()) << "\n" << mk_bounded_pp(get_enode(v2)->get_expr(), get_manager()) << "\n";);
TRACE(arith_eq_adapter_bug, tout << mk_bounded_pp(get_expr(v1), get_manager()) << "\n" << mk_bounded_pp(get_expr(v2), get_manager()) << "\n";);
mk_axioms(get_enode(v1), get_enode(v2));
}
@ -278,5 +278,5 @@ namespace smt {
out << "eq_adapter: #" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n";
}
}
};
}

3
src/smt/arith_eq_adapter.h
View file

@ -70,6 +70,7 @@ namespace smt {
context & get_context() const { return m_owner.get_context(); }
ast_manager & get_manager() const { return m_owner.get_manager(); }
enode * get_enode(theory_var v) const { return m_owner.get_enode(v); }
expr * get_expr(theory_var v) const { return m_owner.get_expr(v); }
public:
arith_eq_adapter(theory & owner, arith_util & u):m_owner(owner), m_util(u) {}
@ -85,6 +86,6 @@ namespace smt {
void collect_statistics(::statistics & st) const;
void display_already_processed(std::ostream & out) const;
};
};
}

7
src/smt/arith_eq_solver.cpp
View file

@ -53,10 +53,7 @@ void arith_eq_solver::prop_mod_const(expr * e, unsigned depth, numeral const& k,
numeral n;
bool is_int;
if (depth == 0) {
result = e;
}
else if (m_util.is_add(e) || m_util.is_mul(e)) {
if (depth != 0 && (m_util.is_add(e) || m_util.is_mul(e))) {
expr_ref_vector args(m);
expr_ref tmp(m);
app* a = to_app(e);
@ -66,7 +63,7 @@ void arith_eq_solver::prop_mod_const(expr * e, unsigned depth, numeral const& k,
}
m_arith_rewriter.mk_app(a->get_decl(), args.size(), args.data(), result);
}
else if (m_util.is_numeral(e, n, is_int) && is_int) {
else if (depth != 0 && m_util.is_numeral(e, n, is_int) && is_int) {
result = m_util.mk_numeral(mod(n, k), true);
}
else {

61
src/smt/dyn_ack.cpp
View file

@ -101,14 +101,14 @@ namespace smt {
};
class dyn_ack_eq_justification : public justification {
app * m_app1;
app * m_app2;
app * m_r;
expr * m_app1;
expr * m_app2;
expr * m_r;
app * m_eq1;
app * m_eq2;
app * m_eq3;
public:
dyn_ack_eq_justification(app * n1, app * n2, app* r, app* eq1, app* eq2, app* eq3):
dyn_ack_eq_justification(expr * n1, expr * n2, expr* r, app* eq1, app* eq2, app* eq3):
justification(false), // dyn_ack_cc_justifications are not stored in regions.
m_app1(n1),
m_app2(n2),
@ -167,7 +167,7 @@ namespace smt {
dyn_ack_manager::~dyn_ack_manager() {
reset_app_pairs();
reset_app_triples();
reset_expr_triples();
}
void dyn_ack_manager::reset_app_pairs() {
@ -189,7 +189,7 @@ namespace smt {
m_num_propagations_since_last_gc = 0;
m_triple.m_app2num_occs.reset();
reset_app_triples();
reset_expr_triples();
m_triple.m_to_instantiate.reset();
m_triple.m_qhead = 0;
}
@ -230,7 +230,7 @@ namespace smt {
}
}
void dyn_ack_manager::eq_eh(app * n1, app * n2, app* r) {
void dyn_ack_manager::eq_eh(expr * n1, expr * n2, expr* r) {
if (n1 == n2 || r == n1 || r == n2 || m.is_bool(n1)) {
return;
}
@ -238,7 +238,7 @@ namespace smt {
std::swap(n1,n2);
TRACE(dyn_ack,
tout << mk_pp(n1, m) << " = " << mk_pp(n2, m) << " = " << mk_pp(r, m) << "\n";);
app_triple tr(n1, n2, r);
expr_triple tr(n1, n2, r);
if (m_triple.m_instantiated.contains(tr)) {
return;
}
@ -361,7 +361,7 @@ namespace smt {
SASSERT(!m_app_pair2num_occs.contains(a1, a2));
return;
}
app_triple tr(0,0,0);
expr_triple tr(0,0,0);
if (m_triple.m_clause2apps.find(cls, tr)) {
[[maybe_unused]] auto [a1, a2, a3] = tr;
SASSERT(a1 && a2 && a3);
@ -451,9 +451,8 @@ namespace smt {
m_triple.m_clause2apps.reset();
}
void dyn_ack_manager::reset_app_triples() {
for (app_triple& p : m_triple.m_apps) {
auto [a1, a2, a3] = p;
void dyn_ack_manager::reset_expr_triples() {
for (auto &[a1,a2,a3] : m_triple.m_apps) {
m.dec_ref(a1);
m.dec_ref(a2);
m.dec_ref(a3);
@ -461,7 +460,7 @@ namespace smt {
m_triple.m_apps.reset();
}
void dyn_ack_manager::instantiate(app * n1, app * n2, app* r) {
void dyn_ack_manager::instantiate(expr * n1, expr * n2, expr* r) {
context& ctx = m_context;
SASSERT(m_params.m_dack != dyn_ack_strategy::DACK_DISABLED);
SASSERT(n1 != n2 && n1 != r && n2 != r);
@ -471,7 +470,7 @@ namespace smt {
<< mk_pp(n2, m) << "\n"
<< mk_pp(r, m) << "\n";
);
app_triple tr(n1, n2, r);
expr_triple tr(n1, n2, r);
SASSERT(m_triple.m_app2num_occs.contains(n1, n2, r));
m_triple.m_app2num_occs.erase(n1, n2, r);
// pair n1,n2 is still in m_triple.m_apps
@ -504,22 +503,22 @@ namespace smt {
}
struct app_triple_lt {
typedef triple<app *, app *, app*> app_triple;
typedef obj_triple_map<app, app, app, unsigned> app_triple2num_occs;
app_triple2num_occs & m_app_triple2num_occs;
struct expr_triple_lt {
typedef triple<expr *, expr *,expr *> expr_triple;
typedef obj_triple_map<expr, expr, expr, unsigned> expr_triple2num_occs;
expr_triple2num_occs & m_expr_triple2num_occs;
app_triple_lt(app_triple2num_occs & m):
m_app_triple2num_occs(m) {
expr_triple_lt(expr_triple2num_occs & m):
m_expr_triple2num_occs(m) {
}
bool operator()(app_triple const & p1, app_triple const & p2) const {
bool operator()(expr_triple const & p1, expr_triple const & p2) const {
auto [a1_1, a1_2, a1_3] = p1;
auto [a2_1, a2_2, a2_3] = p2;
unsigned n1 = 0;
unsigned n2 = 0;
m_app_triple2num_occs.find(a1_1, a1_2, a1_3, n1);
m_app_triple2num_occs.find(a2_1, a2_2, a2_3, n2);
m_expr_triple2num_occs.find(a1_1, a1_2, a1_3, n1);
m_expr_triple2num_occs.find(a2_1, a2_2, a2_3, n2);
SASSERT(n1 > 0);
SASSERT(n2 > 0);
return n1 > n2;
@ -530,11 +529,11 @@ namespace smt {
TRACE(dyn_ack, tout << "dyn_ack GC\n";);
m_triple.m_to_instantiate.reset();
m_triple.m_qhead = 0;
svector<app_triple>::iterator it = m_triple.m_apps.begin();
svector<app_triple>::iterator end = m_triple.m_apps.end();
svector<app_triple>::iterator it2 = it;
svector<expr_triple>::iterator it = m_triple.m_apps.begin();
svector<expr_triple>::iterator end = m_triple.m_apps.end();
svector<expr_triple>::iterator it2 = it;
for (; it != end; ++it) {
app_triple & p = *it;
expr_triple & p = *it;
auto [a1, a2, a3] = p;
if (m_triple.m_instantiated.contains(p)) {
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
@ -548,7 +547,7 @@ namespace smt {
m_triple.m_app2num_occs.find(a1, a2, a3, num_occs);
// The following invariant is not true. a1 and
// a2 may have been instantiated, and removed from
// m_app_triple2num_occs, but not from m_app_triples.
// m_triple.m_app2num_occs, but not from m_triple.m_apps.
//
// SASSERT(num_occs > 0);
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
@ -568,8 +567,8 @@ namespace smt {
m_triple.m_to_instantiate.push_back(p);
}
m_triple.m_apps.set_end(it2);
app_triple_lt f(m_triple.m_app2num_occs);
// app_triple_lt is not a total order
expr_triple_lt f(m_triple.m_app2num_occs);
// expr_triple_lt is not a total order
std::stable_sort(m_triple.m_to_instantiate.begin(), m_triple.m_to_instantiate.end(), f);
}
@ -588,4 +587,4 @@ namespace smt {
}
#endif
};
}

30
src/smt/dyn_ack.h
View file

@ -36,11 +36,11 @@ namespace smt {
typedef obj_pair_hashtable<app, app> app_pair_set;
typedef obj_map<clause, app_pair> clause2app_pair;
typedef triple<app *, app *,app *> app_triple;
typedef obj_triple_map<app, app, app, unsigned> app_triple2num_occs;
typedef svector<app_triple> app_triple_vector;
typedef obj_triple_hashtable<app, app, app> app_triple_set;
typedef obj_map<clause, app_triple> clause2app_triple;
typedef triple<expr *, expr *,expr *> expr_triple;
typedef obj_triple_map<expr, expr, expr, unsigned> expr_triple2num_occs;
typedef svector<expr_triple> expr_triple_vector;
typedef obj_triple_hashtable<expr, expr, expr> expr_triple_set;
typedef obj_map<clause, expr_triple> clause2expr_triple;
context & m_context;
ast_manager & m;
@ -55,14 +55,14 @@ namespace smt {
clause2app_pair m_clause2app_pair;
struct _triple {
app_triple2num_occs m_app2num_occs;
app_triple_vector m_apps;
app_triple_vector m_to_instantiate;
expr_triple2num_occs m_app2num_occs;
expr_triple_vector m_apps;
expr_triple_vector m_to_instantiate;
unsigned m_qhead;
unsigned m_num_instances;
unsigned m_num_propagations_since_last_gc;
app_triple_set m_instantiated;
clause2app_triple m_clause2apps;
expr_triple_set m_instantiated;
clause2expr_triple m_clause2apps;
};
_triple m_triple;
@ -76,9 +76,9 @@ namespace smt {
literal mk_eq(expr * n1, expr * n2);
void cg_eh(app * n1, app * n2);
void eq_eh(app * n1, app * n2, app* r);
void instantiate(app * n1, app * n2, app* r);
void reset_app_triples();
void eq_eh(expr * n1, expr * n2, expr* r);
void instantiate(expr * n1, expr * n2, expr* r);
void reset_expr_triples();
void gc_triples();
public:
@ -112,7 +112,7 @@ namespace smt {
/**
\brief This method is invoked when equalities are used during conflict resolution.
*/
void used_eq_eh(app * n1, app * n2, app* r) {
void used_eq_eh(expr * n1, expr * n2, expr* r) {
if (m_params.m_dack_eq)
eq_eh(n1, n2, r);
}
@ -130,6 +130,6 @@ namespace smt {
#endif
};
};
}

10
src/smt/expr_context_simplifier.cpp
View file

@ -401,10 +401,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result)
args.push_back(arg);
}
}
else if (!m.is_bool(arg)) {
args.push_back(arg);
}
else if (!n2) {
else if (!n2 && m.is_bool(arg)) {
n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
todo.push_back(arg);
parent_ids.push_back(self_pos);
@ -677,10 +674,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
args.push_back(arg);
}
}
else if (!m.is_bool(arg)) {
args.push_back(arg);
}
else if (!n2) {
else if (!n2 && m.is_bool(arg)) {
n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
todo.push_back(arg);
parent_ids.push_back(self_pos);

16
src/smt/fingerprints.cpp
View file

@ -20,10 +20,9 @@ Revision History:
namespace smt {
fingerprint::fingerprint(region & r, void * d, unsigned d_h, expr* def, unsigned n, enode * const * args):
fingerprint::fingerprint(region & r, void * d, unsigned d_h, unsigned n, enode * const * args):
m_data(d),
m_data_hash(d_h),
m_def(def),
m_num_args(n),
m_args(nullptr) {
m_args = new (r) enode*[n];
@ -62,7 +61,7 @@ namespace smt {
}
fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) {
fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
struct arg_data {
unsigned data_hash;
@ -93,9 +92,8 @@ namespace smt {
return nullptr;
}
TRACE(fingerprint_bug, tout << "inserting @" << m_scopes.size() << " " << *d;);
fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, def, num_args, d->m_args);
fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, num_args, d->m_args);
m_fingerprints.push_back(f);
m_defs.push_back(def);
m_set.insert(f);
return f;
}
@ -106,15 +104,12 @@ namespace smt {
return true;
for (unsigned i = 0; i < num_args; ++i)
d->m_args[i] = d->m_args[i]->get_root();
if (m_set.contains(d))
return true;
return false;
return m_set.contains(d);
}
void fingerprint_set::reset() {
m_set.reset();
m_fingerprints.reset();
m_defs.reset();
}
void fingerprint_set::push_scope() {
@ -134,7 +129,6 @@ namespace smt {
m_set.erase(m_fingerprints[i]);
}
m_fingerprints.shrink(old_size);
m_defs.shrink(old_size);
m_scopes.shrink(new_lvl);
TRACE(fingerprint_bug, tout << "pop @" << m_scopes.size() << "\n";);
}
@ -171,4 +165,4 @@ namespace smt {
#endif
};
}

11
src/smt/fingerprints.h
View file

@ -27,16 +27,14 @@ namespace smt {
protected:
void* m_data = nullptr;
unsigned m_data_hash = 0;
expr* m_def = nullptr;
unsigned m_num_args = 0;
enode** m_args = nullptr;
friend class fingerprint_set;
fingerprint() = default;
public:
fingerprint(region & r, void * d, unsigned d_hash, expr* def, unsigned n, enode * const * args);
fingerprint(region & r, void * d, unsigned d_hash, unsigned n, enode * const * args);
void * get_data() const { return m_data; }
expr * get_def() const { return m_def; }
unsigned get_data_hash() const { return m_data_hash; }
unsigned get_num_args() const { return m_num_args; }
enode * const * get_args() const { return m_args; }
@ -59,7 +57,6 @@ namespace smt {
region & m_region;
set m_set;
ptr_vector<fingerprint> m_fingerprints;
expr_ref_vector m_defs;
unsigned_vector m_scopes;
ptr_vector<enode> m_tmp;
fingerprint m_dummy;
@ -67,8 +64,8 @@ namespace smt {
fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
public:
fingerprint_set(ast_manager& m, region & r): m_region(r), m_defs(m) {}
fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def);
fingerprint_set(ast_manager& m, region & r): m_region(r) {}
fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
unsigned size() const { return m_fingerprints.size(); }
bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
void reset();
@ -79,6 +76,6 @@ namespace smt {
bool slow_contains(void const * data, unsigned data_hash, unsigned num_args, enode * const * args) const;
#endif
};
};
}

54
src/smt/mam.cpp
View file

@ -1114,8 +1114,9 @@ namespace {
best_j = j;
}
}
if (best == nullptr)
continue;
m_mp_already_processed[best_j] = true;
SASSERT(best != 0);
app * p = best;
func_decl * lbl = p->get_decl();
unsigned short num_args = p->get_num_args();
@ -1225,7 +1226,11 @@ namespace {
SASSERT(head->m_next == 0);
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
unsigned num_decls = m_qa->get_num_decls();
unsigned_vector var_regs(num_decls);
for (unsigned i = 0; i < num_decls; ++i)
var_regs[i] = static_cast<unsigned>(m_vars[i]);
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, num_decls, var_regs.data()));
for (instruction* curr : m_seq) {
head->m_next = curr;
@ -1360,6 +1365,7 @@ namespace {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}
@ -1875,7 +1881,7 @@ namespace {
}
void update_max_generation(enode * n, enode * prev) {
m_max_generation = std::max(m_max_generation, n->get_generation());
m_max_generation = std::max(m_max_generation, m_context.get_generation(n));
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
m_used_enodes.push_back(std::make_tuple(prev, n));
@ -1908,6 +1914,7 @@ namespace {
return nullptr;
}
/**
\brief Execute the is_cgr instruction.
Return true if succeeded, and false if backtracking is needed.
@ -2043,7 +2050,7 @@ namespace {
void get_min_max_top_generation(unsigned& min, unsigned& max) {
SASSERT(!m_pattern_instances.empty());
if (m_min_top_generation.empty()) {
min = max = m_pattern_instances[0]->get_generation();
min = max = m_context.get_generation(m_pattern_instances[0]);
m_min_top_generation.push_back(min);
m_max_top_generation.push_back(max);
}
@ -2052,7 +2059,7 @@ namespace {
max = m_max_top_generation.back();
}
for (unsigned i = m_min_top_generation.size(); i < m_pattern_instances.size(); ++i) {
unsigned curr = m_pattern_instances[i]->get_generation();
unsigned curr = m_context.get_generation(m_pattern_instances[i]);
min = std::min(min, curr);
m_min_top_generation.push_back(min);
max = std::max(max, curr);
@ -2293,7 +2300,8 @@ namespace {
m_min_top_generation.reset();
m_max_top_generation.reset();
m_pattern_instances.push_back(n);
m_max_generation = n->get_generation();
m_max_generation = m_context.get_generation(n);
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) {
m_used_enodes.reset();
@ -2533,7 +2541,7 @@ namespace {
case YIELD1:
m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
#define ON_MATCH(NUM) \
m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
m_max_generation = std::max(m_max_generation, m_context.get_max_generation(NUM, m_bindings.begin())); \
if (m_context.get_cancel_flag()) { \
return false; \
} \
@ -2737,7 +2745,7 @@ namespace {
#define BBIND_COMMON() m_b = static_cast<const bind*>(bp.m_instr); \
m_n1 = m_registers[m_b->m_ireg]; \
m_app = get_next_f_app(m_b->m_label, m_b->m_num_args, m_n1, bp.m_curr); \
if (m_app == 0) { \
if (!m_app) { \
m_top--; \
goto backtrack; \
} \
@ -2908,6 +2916,8 @@ namespace {
SASSERT(m.is_pattern(mp));
SASSERT(first_idx < mp->get_num_args());
app * p = to_app(mp->get_arg(first_idx));
if (is_ground(p))
return;
func_decl * lbl = p->get_decl();
unsigned lbl_id = lbl->get_small_id();
m_trees.reserve(lbl_id+1, nullptr);
@ -3735,7 +3745,7 @@ namespace {
}
void match_new_patterns() {
TRACE(mam_new_pat, tout << "matching new patterns:\n";);
TRACE(mam, tout << "matching new patterns:\n";);
m_tmp_trees_to_delete.reset();
for (auto const& kv : m_new_patterns) {
if (m_context.get_cancel_flag()) {
@ -3781,8 +3791,14 @@ namespace {
for (unsigned i = 0; i < num_patterns; ++i) {
app * pat = to_app(mp->get_arg(i));
TRACE(mam_pat, tout << mk_ismt2_pp(qa, m) << "\npat:\n" << mk_ismt2_pp(pat, m) << "\n";);
SASSERT(!pat->is_ground());
todo.push_back(pat);
if (pat->is_ground()) {
enode * e = mk_enode(m_context, qa, pat);
m_context.mark_as_relevant(e);
m_context.push_trail(add_shared_enode_trail(*this, e));
m_shared_enodes.insert(e);
}
else
todo.push_back(pat);
}
while (!todo.empty()) {
app * n = todo.back();
@ -3833,10 +3849,10 @@ namespace {
// Ground patterns are discarded.
// However, the simplifier may turn a non-ground pattern into a ground one.
// So, we should check it again here.
unsigned num_patterns = mp->get_num_args();
for (unsigned i = 0; i < num_patterns; ++i)
if (is_ground(mp->get_arg(i)))
return; // ignore multi-pattern containing ground pattern.
if (all_of(*mp, [](expr *arg) { return is_ground(arg); }))
return; // ignore multi-pattern containing only ground pattern.
if (any_of(*mp, [](expr *arg) { return has_quantifiers(arg); }))
return; // patterns with quantifiers are not handled.
update_filters(qa, mp);
collect_ground_exprs(qa, mp);
m_new_patterns.push_back(qp_pair(qa, mp));
@ -3844,7 +3860,7 @@ namespace {
// e-matching. So, for a multi-pattern [ p_1, ..., p_n ],
// we have to make n insertions. In the i-th insertion,
// the pattern p_i is assumed to be the first one.
for (unsigned i = 0; i < num_patterns; ++i)
for (unsigned i = 0; i < mp->get_num_args(); ++i)
m_trees.add_pattern(qa, mp, i);
}
@ -3940,15 +3956,11 @@ namespace {
}
return;
}
DEBUG_CODE(
for (unsigned i = 0; i < num_bindings; ++i) {
SASSERT(bindings[i]->get_generation() <= max_generation);
});
#endif
unsigned min_gen = 0, max_gen = 0;
m_interpreter.get_min_max_top_generation(min_gen, max_gen);
m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes);
m_context.add_instance(qa, pat, num_bindings, bindings, max_generation, min_gen, max_gen, used_enodes);
}
bool is_shared(enode * n) const override {

2
src/smt/mam.h
View file

@ -69,5 +69,5 @@ namespace smt {
};
mam * mk_mam(context & ctx);
};
}

7
src/smt/qi_queue.cpp
View file

@ -140,7 +140,7 @@ namespace smt {
tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight()
<< ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n";
for (unsigned i = 0; i < f->get_num_args(); ++i) {
tout << "#" << f->get_arg(i)->get_expr_id() << " d:" << f->get_arg(i)->get_expr()->get_depth() << " ";
tout << "#" << f->get_arg(i)->get_expr_id() << " d:" << get_depth(f->get_arg(i)->get_expr()) << " ";
}
tout << "\n";);
TRACE(new_entries_bug, tout << "[qi:insert]\n";);
@ -331,9 +331,6 @@ namespace smt {
unsigned gen = get_new_gen(q, generation, ent.m_cost);
display_instance_profile(f, q, num_bindings, bindings, proof_id, gen);
m_context.internalize_instance(lemma, pr1, gen);
if (f->get_def()) {
m_context.internalize(f->get_def(), true);
}
TRACE_CODE({
static unsigned num_useless = 0;
if (m.is_or(lemma)) {
@ -521,5 +518,5 @@ namespace smt {
#endif
}
};
}

2
src/smt/qi_queue.h
View file

@ -101,6 +101,6 @@ namespace smt {
m_on_binding = on_binding;
}
};
};
}

2
src/smt/seq_axioms.h
View file

@ -105,5 +105,5 @@ namespace smt {
};
};
}

2
src/smt/seq_eq_solver.cpp
View file

@ -189,7 +189,7 @@ bool theory_seq::len_based_split(depeq const& e) {
expr_ref_vector const& rs = e.rs;
int offset = 0;
if (!has_len_offset(ls, rs, offset))
if (!has_len_offset(ls, rs, offset) || offset == 0)
return false;
TRACE(seq, tout << "split based on length\n";);

2
src/smt/seq_offset_eq.h
View file

@ -53,5 +53,5 @@ namespace smt {
void pop_scope_eh(unsigned num_scopes);
};
};
}

272
src/smt/seq_regex.cpp
View file

@ -21,6 +21,7 @@ Author:
#include "ast/expr_abstract.h"
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/seq_regex_bisim.h"
#include <ast/rewriter/expr_safe_replace.h>
namespace smt {
@ -127,6 +128,30 @@ namespace smt {
return;
}
if (th.get_fparams().m_seq_regex_factorization_enabled) {
unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold;
if (threshold == 0)
threshold = UINT_MAX;
split_set result;
auto [head, tail] = seq_rw().split_membership(s, r, threshold, result);
if (head) {
SASSERT(tail);
// propagate all cases
expr_ref_vector cases(m);
expr_ref_vector branches(m);
for (auto [pre, post] : result) {
expr_ref mem_head(re().mk_in_re(head, pre), m);
expr_ref mem_tail(re().mk_in_re(tail, post), m);
cases.push_back(m.mk_and(mem_head, mem_tail));
}
const expr_ref cases_expr(m.mk_or(cases), m);
ctx.internalize(cases_expr, false);
th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr));
return;
}
// fallthrough; decomposition failed
}
// Convert a non-ground sequence into an additional regex and
// strengthen the original regex constraint into an intersection
// for example:
@ -223,6 +248,17 @@ namespace smt {
th.add_axiom(~lit);
return true;
}
// Fall back to antimirov NFA reachability. The lazy state graph
// keys states by AST identity and cannot close on intersections /
// complements whose derivative product states do not canonicalize,
// so it never detects their emptiness. re_is_empty decides
// emptiness directly (the same procedure propagate_eq already uses
// for re.none equalities).
if (re_is_empty(r) == l_true) {
STRACE(seq_regex_brief, tout << "(empty:re) ";);
th.add_axiom(~lit);
return true;
}
}
return false;
}
@ -460,6 +496,41 @@ namespace smt {
if (re().is_empty(r))
//trivially true
return;
// When one side is re.none the equation is a pure emptiness check on
// the other regex (symmetric_diff already returned it as r). Decide
// it directly by antimirov NFA reachability instead of running the
// bisimulation/XOR closure, which would build large un-canonicalized
// product states for intersections of contains-patterns.
if ((re().is_empty(r1) || re().is_empty(r2)) && is_ground(r)) {
switch (re_is_empty(r)) {
case l_true:
STRACE(seq_regex_brief, tout << "empty:eq ";);
return; // languages equal (both empty): trivially true
case l_false:
STRACE(seq_regex_brief, tout << "empty:neq ";);
th.add_axiom(~th.mk_eq(r1, r2, false), false_literal);
return;
case l_undef:
break;
}
}
// Try the bisimulation procedure on ground regexes first. If it
// returns a definite answer, dispatch the corresponding axiom and
// bypass the symbolic emptiness/derivative closure.
if (is_ground(r1) && is_ground(r2)) {
seq::regex_bisim bisim(seq_rw());
switch (bisim.are_equivalent(r1, r2)) {
case l_true:
STRACE(seq_regex_brief, tout << "bisim:eq ";);
return; // trivially true
case l_false:
STRACE(seq_regex_brief, tout << "bisim:neq ";);
th.add_axiom(~th.mk_eq(r1, r2, false), false_literal);
return;
case l_undef:
break;
}
}
expr_ref emp(re().mk_empty(r->get_sort()), m);
expr_ref f(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref is_empty = sk().mk_is_empty(r, r, f);
@ -478,6 +549,20 @@ namespace smt {
sort* seq_sort = nullptr;
VERIFY(u().is_re(r1, seq_sort));
expr_ref r = symmetric_diff(r1, r2);
if (is_ground(r1) && is_ground(r2)) {
seq::regex_bisim bisim(seq_rw());
switch (bisim.are_equivalent(r1, r2)) {
case l_true:
STRACE(seq_regex_brief, tout << "bisim:eq ";);
th.add_axiom(th.mk_eq(r1, r2, false), false_literal);
return;
case l_false:
STRACE(seq_regex_brief, tout << "bisim:neq ";);
return; // trivially satisfied
case l_undef:
break;
}
}
expr_ref emp(re().mk_empty(r->get_sort()), m);
expr_ref n(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n);
@ -530,16 +615,16 @@ namespace smt {
lits.push_back(null_lit);
expr_ref_pair_vector cofactors(m);
get_cofactors(d, cofactors);
for (auto const& p : cofactors) {
if (is_member(p.second, u))
seq_rw().get_cofactors(hd, d, cofactors);
for (auto const& [c, r] : cofactors) {
if (is_member(r, u))
continue;
expr_ref cond(p.first, m);
expr_ref cond(c, m);
seq_rw().elim_condition(hd, cond);
rewrite(cond);
if (m.is_false(cond))
continue;
expr_ref next_non_empty = sk().mk_is_non_empty(p.second, re().mk_union(u, p.second), n);
expr_ref next_non_empty = sk().mk_is_non_empty(r, re().mk_union(u, r), n);
if (!m.is_true(cond))
next_non_empty = m.mk_and(cond, next_non_empty);
lits.push_back(th.mk_literal(next_non_empty));
@ -640,88 +725,113 @@ namespace smt {
}
/*
Return a list of all target regexes in the derivative of a regex r,
ignoring the conditions along each path.
Decide emptiness of a ground regex r via antimirov-mode NFA
reachability.
The derivative construction uses (:var 0) and tries
to eliminate unsat condition paths but it does not perform
full satisfiability checks and it is not guaranteed
that all targets are actually reachable
The symbolic derivative engine runs in antimirov mode, so the
derivative of an intersection distributes into a *set* of individual
product states inter(A_i, B_j) (each a small, ground regex) rather
than one giant union-of-intersections term. get_derivative_targets
enumerates these NFA successor states.
We short-circuit to l_false (non-empty) as soon as a reachable state
is nullable (accepts the empty word) or classical (a regex built only
from to_re/all/union/concat/star/plus/opt/loop, hence non-empty). An
intersection itself is never classical, but once one operand reduces
to Σ* the intersection collapses (via the derivative's subset
simplification) to the other, classical, operand.
If the worklist is exhausted with no such state, r is empty (l_true).
Returns l_undef if a step bound is hit, so callers can fall back to
the general procedure.
*/
lbool seq_regex::re_is_empty(expr* r) {
if (re().is_empty(r))
return l_true;
expr_ref_vector pinned(m);
obj_hashtable<expr> visited;
ptr_vector<expr> work;
work.push_back(r);
visited.insert(r);
pinned.push_back(r);
unsigned const bound = 100000;
unsigned steps = 0;
while (!work.empty()) {
if (++steps > bound)
return l_undef;
expr* s = work.back();
work.pop_back();
auto info = re().get_info(s);
if (!info.is_known())
return l_undef;
// ε ∈ L(s) or s is a non-empty classical regex ⇒ L(r) non-empty.
if (info.nullable == l_true || info.classical)
return l_false;
// Dead state: prune (min_length == UINT_MAX means no word is
// accepted from here).
if (info.min_length == UINT_MAX)
continue;
expr_ref_vector targets(m);
get_derivative_targets(s, targets);
for (expr* t : targets) {
if (visited.contains(t))
continue;
visited.insert(t);
pinned.push_back(t);
work.push_back(t);
}
}
return l_true;
}
/*
Return a list of all reachable target regexes in the derivative of a
regex r.
The derivative is taken wrt (:var 0) and its reachable leaves are
enumerated with the path-aware cofactor engine, which conjoins the
ITE-path conditions and prunes infeasible character-range combinations
(e.g. a nested branch requiring elem = 'a' and elem = 'B'). Each leaf
is re-normalized with the path-aware smart constructors so that
semantically equal states stay syntactically identical (essential for
state dedup in the emptiness closure).
Without this pruning the naive ITE-tree DFS would reach infeasible
leaves; an infeasible classical (intersection/complement-free) leaf
would then be misjudged as a non-empty residual.
*/
void seq_regex::get_derivative_targets(expr* r, expr_ref_vector& targets) {
// constructs the derivative wrt (:var 0)
expr_ref d(seq_rw().mk_derivative(r), m);
// use DFS to collect all the targets (leaf regexes) in d.
expr* _1 = nullptr, * e1 = nullptr, * e2 = nullptr;
obj_hashtable<expr>::entry* _2 = nullptr;
vector<expr*> workset;
workset.push_back(d);
obj_hashtable<expr> done;
done.insert(d);
while (workset.size() > 0) {
expr* e = workset.back();
workset.pop_back();
if (m.is_ite(e, _1, e1, e2) || re().is_union(e, e1, e2)) {
if (done.insert_if_not_there_core(e1, _2))
workset.push_back(e1);
if (done.insert_if_not_there_core(e2, _2))
workset.push_back(e2);
}
else if (!re().is_empty(e))
targets.push_back(e);
expr_ref_pair_vector cofactors(m);
seq_rw().brz_derivative_cofactors(r, cofactors);
for (auto const& [c, t] : cofactors) {
if (!re().is_empty(t))
targets.push_back(t);
}
}
/*
Return a list of all (cond, leaf) pairs in a given derivative
expression r.
expression r, where elem is the character symbol the derivative was
taken with respect to.
Note: this implementation is inefficient: it simply collects all expressions under an if and
iterates over all combinations.
The transition regexes produced by the symbolic derivative engine are
ITE-trees over character predicates ci on elem (equalities such as
elem = 'A', and ranges such as 'a' <= elem <= 'z'). These predicates
are typically mutually exclusive, so the number of feasible truth
assignments to {c1,..,ck} ("minterms") is small.
This method is still used by:
The enumeration is delegated to seq::derive (via seq_rw().get_cofactors)
so it reuses the very same path/interval context that the derivative
engine uses while hoisting ITEs: each feasible path through the ITE-tree
yields one (path_condition, leaf) cofactor, infeasible character-range
combinations are pruned, and the leaf is simplified with the path-aware
smart constructors.
This is used by:
propagate_is_empty
propagate_is_non_empty
*/
void seq_regex::get_cofactors(expr* r, expr_ref_pair_vector& result) {
obj_hashtable<expr> ifs;
expr* cond = nullptr, * r1 = nullptr, * r2 = nullptr;
for (expr* e : subterms::ground(expr_ref(r, m)))
if (m.is_ite(e, cond, r1, r2))
ifs.insert(cond);
expr_ref_vector rs(m);
vector<expr_ref_vector> conds;
conds.push_back(expr_ref_vector(m));
rs.push_back(r);
for (expr* c : ifs) {
unsigned sz = conds.size();
expr_safe_replace rep1(m);
expr_safe_replace rep2(m);
rep1.insert(c, m.mk_true());
rep2.insert(c, m.mk_false());
expr_ref r2(m);
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector cs = conds[i];
cs.push_back(mk_not(m, c));
conds.push_back(cs);
conds[i].push_back(c);
expr_ref r1(rs.get(i), m);
rep1(r1, r2);
rs[i] = r2;
rep2(r1, r2);
rs.push_back(r2);
}
}
for (unsigned i = 0; i < conds.size(); ++i) {
expr_ref conj = mk_and(conds[i]);
expr_ref r(rs.get(i), m);
ctx.get_rewriter()(r);
if (!m.is_false(conj) && !re().is_empty(r))
result.push_back(conj, r);
}
}
/*
is_empty(r, u) => ~is_nullable(r)
@ -749,11 +859,11 @@ namespace smt {
d = mk_derivative_wrapper(hd, r);
literal_vector lits;
expr_ref_pair_vector cofactors(m);
get_cofactors(d, cofactors);
for (auto const& p : cofactors) {
if (is_member(p.second, u))
seq_rw().get_cofactors(hd, d, cofactors);
for (auto const& [c, r] : cofactors) {
if (is_member(r, u))
continue;
expr_ref cond(p.first, m);
expr_ref cond(c, m);
seq_rw().elim_condition(hd, cond);
rewrite(cond);
if (m.is_false(cond))
@ -762,9 +872,11 @@ namespace smt {
lits.push_back(~lit);
if (!m.is_true(cond)) {
expr_ref ncond(mk_not(m, cond), m);
lits.push_back(th.mk_literal(mk_forall(m, hd, ncond)));
expr_ref facond = mk_forall(m, hd, ncond);
ctx.internalize(facond, true); // make sure fa is internalized, and assumed in positive polarity only.
lits.push_back(th.mk_literal(facond));
}
expr_ref is_empty1 = sk().mk_is_empty(p.second, re().mk_union(u, p.second), n);
expr_ref is_empty1 = sk().mk_is_empty(r, re().mk_union(u, r), n);
lits.push_back(th.mk_literal(is_empty1));
th.add_axiom(lits);
}

9
src/smt/seq_regex.h
View file

@ -164,7 +164,12 @@ namespace smt {
// returned by derivative_wrapper
expr_ref mk_deriv_accept(expr* s, unsigned i, expr* r);
void get_derivative_targets(expr* r, expr_ref_vector& targets);
void get_cofactors(expr* r, expr_ref_pair_vector& result);
// Decide emptiness of a ground regex by antimirov-mode NFA
// reachability: explore derivative target states, short-circuiting to
// "non-empty" on the first reachable nullable or classical state.
// Returns l_true (empty), l_false (non-empty), l_undef (gave up).
lbool re_is_empty(expr* r);
/*
Pretty print the regex of the state id to the out stream,
@ -209,4 +214,4 @@ namespace smt {
};
};
}

4
src/smt/smt_almost_cg_table.cpp
View file

@ -77,7 +77,7 @@ namespace smt {
}
bool almost_cg_table::cg_eq::operator()(enode * n1, enode * n2) const {
if (n1->get_expr()->get_decl() != n2->get_expr()->get_decl())
if (n1->get_decl() != n2->get_decl() || !n1->is_app())
return false;
unsigned num_args = n1->get_num_args();
if (num_args != n2->get_num_args())
@ -124,4 +124,4 @@ namespace smt {
return result;
}
};
}

2
src/smt/smt_almost_cg_table.h
View file

@ -65,6 +65,6 @@ namespace smt {
bool empty() const { return m_table.empty(); }
};
};
}

8
src/smt/smt_arith_value.cpp
View file

@ -163,4 +163,10 @@ namespace smt {
return th->final_check_eh(level);
}
};
lbool arith_value::check_lp_feasible(vector<std::pair<bool, expr_ref>>& ineqs, literal_vector& lit_core,
enode_pair_vector& eq_core) {
if (!m_thr)
return l_undef;
return m_thr->check_lp_feasible(ineqs, lit_core, eq_core);
}
}

4
src/smt/smt_arith_value.h
View file

@ -48,5 +48,7 @@ namespace smt {
expr_ref get_up(expr* e) const;
expr_ref get_fixed(expr* e) const;
final_check_status final_check(unsigned );
lbool check_lp_feasible(vector<std::pair<bool, expr_ref>> &ineqs, literal_vector &lit_core,
enode_pair_vector &eq_core);
};
};
}

2
src/smt/smt_b_justification.h
View file

@ -99,6 +99,6 @@ namespace smt {
}
typedef std::pair<literal, b_justification> justified_literal;
};
}

2
src/smt/smt_bool_var_data.h
View file

@ -131,6 +131,6 @@ namespace smt {
m_atom = false;
}
};
};
}

7
src/smt/smt_case_split_queue.cpp
View file

@ -1012,7 +1012,7 @@ namespace {
stack.pop_back();
if (m_context.e_internalized(curr)) {
gen = m_context.get_enode(curr)->get_generation();
gen = m_context.get_generation(m_context.get_enode(curr));
if (gen > maxgen)
maxgen = gen;
if (gen < mingen)
@ -1046,7 +1046,7 @@ namespace {
void operator()(expr * e) {
if (m_context.e_internalized(e)) {
enode * n = m_context.get_enode(e);
n->set_generation(m_context, m_generation);
m_context.set_generation(n, m_generation);
}
}
};
@ -1069,7 +1069,8 @@ namespace {
stack.pop_back();
if (m_context.e_internalized(curr)) {
unsigned curr_gen = m_context.get_enode(curr)->get_generation();
enode * n = m_context.get_enode(curr);
unsigned curr_gen = m_context.get_generation(n);
if (curr_gen > gen) {
// Lower it.
set_generation_rec(e, gen);

2
src/smt/smt_case_split_queue.h
View file

@ -52,6 +52,6 @@ namespace smt {
};
case_split_queue * mk_case_split_queue(context & ctx, smt_params & p);
};
}

2
src/smt/smt_cg_table.cpp
View file

@ -258,5 +258,5 @@ namespace smt {
return true;
}
};
}

2
src/smt/smt_cg_table.h
View file

@ -216,6 +216,6 @@ namespace smt {
bool check_invariant() const;
};
};
}

50
src/smt/smt_checker.cpp
View file

@ -22,23 +22,25 @@ Revision History:
namespace smt {
bool checker::all_args(app * a, bool is_true) {
bool checker::all_args(app *a, unsigned depth, bool is_true) {
for (expr* arg : *a) {
if (!check(arg, is_true))
if (!check(arg, depth + 1, is_true))
return false;
}
return true;
}
bool checker::any_arg(app * a, bool is_true) {
bool checker::any_arg(app *a, unsigned depth, bool is_true) {
for (expr* arg : *a) {
if (check(arg, is_true))
if (check(arg, depth + 1, is_true))
return true;
}
return false;
}
bool checker::check_core(expr * n, bool is_true) {
bool checker::check_core(expr *n, unsigned depth, bool is_true) {
if (depth > 600)
return false;
SASSERT(m_manager.is_bool(n));
if (m_context.b_internalized(n) && m_context.is_relevant(n)) {
lbool val = m_context.get_assignment(n);
@ -54,11 +56,11 @@ namespace smt {
case OP_FALSE:
return !is_true;
case OP_NOT:
return check(a->get_arg(0), !is_true);
return check(a->get_arg(0), depth + 1, !is_true);
case OP_OR:
return is_true ? any_arg(a, true) : all_args(a, false);
return is_true ? any_arg(a, depth, true) : all_args(a, depth, false);
case OP_AND:
return is_true ? all_args(a, true) : any_arg(a, false);
return is_true ? all_args(a, depth, true) : any_arg(a, depth, false);
case OP_EQ:
if (!m_manager.is_iff(a)) {
enode * lhs = get_enode_eq_to(a->get_arg(0));
@ -74,27 +76,27 @@ namespace smt {
}
else if (is_true) {
return
(check(a->get_arg(0), true) &&
check(a->get_arg(1), true)) ||
(check(a->get_arg(0), false) &&
check(a->get_arg(1), false));
(check(a->get_arg(0), depth + 1, true) &&
check(a->get_arg(1), depth + 1, true)) ||
(check(a->get_arg(0), depth + 1, false) &&
check(a->get_arg(1), depth + 1, false));
}
else {
return
(check(a->get_arg(0), true) &&
check(a->get_arg(1), false)) ||
(check(a->get_arg(0), false) &&
check(a->get_arg(1), true));
(check(a->get_arg(0), depth + 1, true) &&
check(a->get_arg(1), depth + 1, false)) ||
(check(a->get_arg(0), depth + 1, false) &&
check(a->get_arg(1), depth + 1, true));
}
case OP_ITE: {
if (m_context.lit_internalized(a->get_arg(0)) && m_context.is_relevant(a->get_arg(0))) {
switch (m_context.get_assignment(a->get_arg(0))) {
case l_false: return check(a->get_arg(2), is_true);
case l_false: return check(a->get_arg(2), depth + 1, is_true);
case l_undef: return false;
case l_true: return check(a->get_arg(1), is_true);
case l_true: return check(a->get_arg(1), depth + 1, is_true);
}
}
return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true);
return check(a->get_arg(1), depth + 1, is_true) && check(a->get_arg(2), depth + 1, is_true);
}
default:
break;
@ -108,11 +110,11 @@ namespace smt {
return false;
}
bool checker::check(expr * n, bool is_true) {
bool checker::check(expr *n, unsigned depth, bool is_true) {
bool r;
if (n->get_ref_count() > 1 && m_is_true_cache[is_true].find(n, r))
return r;
r = check_core(n, is_true);
r = check_core(n, depth, is_true);
if (n->get_ref_count() > 1)
m_is_true_cache[is_true].insert(n, r);
return r;
@ -156,7 +158,7 @@ namespace smt {
bool checker::is_sat(expr * n, unsigned num_bindings, enode * const * bindings) {
flet<unsigned> l1(m_num_bindings, num_bindings);
flet<enode * const *> l2(m_bindings, bindings);
bool r = check(n, true);
bool r = check(n, 0, true);
m_is_true_cache[0].reset();
m_is_true_cache[1].reset();
m_to_enode_cache.reset();
@ -166,7 +168,7 @@ namespace smt {
bool checker::is_unsat(expr * n, unsigned num_bindings, enode * const * bindings) {
flet<unsigned> l1(m_num_bindings, num_bindings);
flet<enode * const *> l2(m_bindings, bindings);
bool r = check(n, false);
bool r = check(n, 0,false);
m_is_true_cache[0].reset();
m_is_true_cache[1].reset();
m_to_enode_cache.reset();
@ -180,7 +182,7 @@ namespace smt {
m_bindings(nullptr) {
}
};
}

10
src/smt/smt_checker.h
View file

@ -37,10 +37,10 @@ namespace smt {
unsigned m_num_bindings;
enode * const * m_bindings;
bool all_args(app * a, bool is_true);
bool any_arg(app * a, bool is_true);
bool check_core(expr * n, bool is_true);
bool check(expr * n, bool is_true);
bool all_args(app *a, unsigned depth, bool is_true);
bool any_arg(app *a, unsigned depth, bool is_true);
bool check_core(expr * n, unsigned depth, bool is_true);
bool check(expr *n, unsigned depth, bool is_true);
enode * get_enode_eq_to_core(app * n);
enode * get_enode_eq_to(expr * n);
@ -50,6 +50,6 @@ namespace smt {
bool is_unsat(expr * n, unsigned num_bindings = 0, enode * const * bindings = nullptr);
};
};
}

2
src/smt/smt_clause.cpp
View file

@ -126,4 +126,4 @@ namespace smt {
return out << mk_pp(disj, m, 3);
}
};
}

2
src/smt/smt_clause.h
View file

@ -279,6 +279,6 @@ namespace smt {
typedef ptr_vector<clause> clause_vector;
typedef obj_hashtable<clause> clause_set;
};
}

9
src/smt/smt_clause_proof.cpp
View file

@ -151,15 +151,16 @@ namespace smt {
update(st, m_lits, pr);
}
void clause_proof::propagate(literal lit, justification const& jst, literal_vector const& ante) {
void clause_proof::propagate(literal lit, justification * jst, literal_vector const& ante) {
if (!is_enabled())
return;
m_lits.reset();
for (literal l : ante)
m_lits.push_back(ctx.literal2expr(~l));
m_lits.push_back(ctx.literal2expr(lit));
proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
update(clause_proof::status::th_lemma, m_lits, pr);
auto st = clause_proof::status::th_lemma;
auto pr = justification2proof(st, jst);
update(st, m_lits, pr);
}
void clause_proof::del(clause& c) {
@ -290,6 +291,6 @@ namespace smt {
}
}
};
}

4
src/smt/smt_clause_proof.h
View file

@ -82,7 +82,7 @@ namespace smt {
void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr);
void add(clause& c, literal_buffer const* simp_lits = nullptr);
void add(unsigned n, literal const* lits, clause_kind k, justification* j);
void propagate(literal lit, justification const& j, literal_vector const& ante);
void propagate(literal lit, justification* j, literal_vector const& ante);
void del(clause& c);
proof_ref get_proof(bool inconsistent);
bool is_enabled() const { return m_enabled; }
@ -94,6 +94,6 @@ namespace smt {
};
std::ostream& operator<<(std::ostream& out, clause_proof::status st);
};
}

18
src/smt/smt_conflict_resolution.cpp
View file

@ -126,7 +126,7 @@ namespace smt {
break;
case eq_justification::CONGRUENCE: {
CTRACE(dyn_ack_target, !lhs->is_eq(), tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";);
m_dyn_ack_manager.used_cg_eh(lhs->get_expr(), rhs->get_expr());
m_dyn_ack_manager.used_cg_eh(lhs->get_app(), rhs->get_app());
unsigned num_args = lhs->get_num_args();
SASSERT(num_args == rhs->get_num_args());
if (js.used_commutativity()) {
@ -347,7 +347,7 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
justification2literals_core(js, antecedents);
m_ctx.get_clause_proof().propagate(consequent, *js, antecedents);
m_ctx.get_clause_proof().propagate(consequent, js, antecedents);
for (literal l : antecedents)
process_antecedent(l, num_marks);
(void)consequent;
@ -787,8 +787,8 @@ namespace smt {
SASSERT(m.has_fact(pr));
expr* f1 = nullptr, *f2 = nullptr;
app * fact = to_app(m.get_fact(pr));
app * n1_owner = n1->get_expr();
app * n2_owner = n2->get_expr();
expr * n1_owner = n1->get_expr();
expr * n2_owner = n2->get_expr();
bool is_eq = m.is_eq(fact, f1, f2);
if (is_eq && is_quantifier(f1)) {
f1 = m_ctx.get_enode(f1)->get_expr();
@ -855,7 +855,7 @@ namespace smt {
case eq_justification::CONGRUENCE:
num_args = n1->get_num_args();
SASSERT(num_args == n2->get_num_args());
SASSERT(n1->get_expr()->get_decl() == n2->get_expr()->get_decl());
SASSERT(n1->get_decl() == n2->get_decl());
if (js.used_commutativity()) {
bool visited = true;
SASSERT(num_args == 2);
@ -878,8 +878,8 @@ namespace smt {
}
if (!visited)
return nullptr;
app * e1 = n1->get_expr();
app * e2 = n2->get_expr();
app * e1 = n1->get_app();
app * e2 = n2->get_app();
app * e2_prime = m.mk_app(e2->get_decl(), e2->get_arg(1), e2->get_arg(0));
proof * pr1 = nullptr;
if (!prs.empty()) {
@ -910,7 +910,7 @@ namespace smt {
}
if (!visited)
return nullptr;
proof * pr = m.mk_congruence(n1->get_expr(), n2->get_expr(), prs.size(), prs.data());
proof * pr = m.mk_congruence(n1->get_app(), n2->get_app(), prs.size(), prs.data());
m_new_proofs.push_back(pr);
return pr;
}
@ -1485,5 +1485,5 @@ namespace smt {
return alloc(conflict_resolution, m, ctx, dack_manager, params, assigned_literals, watches);
}
};
}

2
src/smt/smt_conflict_resolution.h
View file

@ -276,6 +276,6 @@ namespace smt {
);
};
}

217
src/smt/smt_context.cpp
View file

@ -66,10 +66,9 @@ namespace smt {
m_progress_callback(nullptr),
m_next_progress_sample(0),
m_clause_proof(*this),
m_fingerprints(m, m_region),
m_fingerprints(m, get_region()),
m_b_internalized_stack(m),
m_e_internalized_stack(m),
m_l_internalized_stack(m),
m_final_check_idx(0),
m_cg_table(m),
m_conflict(null_b_justification),
@ -81,7 +80,6 @@ namespace smt {
m_unsat_core(m),
m_mk_bool_var_trail(*this),
m_mk_enode_trail(*this),
m_mk_lambda_trail(*this),
m_lemma_visitor(m) {
SASSERT(m_scope_lvl == 0);
@ -120,6 +118,13 @@ namespace smt {
if (!m_setup.already_configured()) {
m_fparams.updt_params(p);
}
else {
// selected parameters are safe to update after initialization
m_fparams.m_max_conflicts = p.get_uint("max_conflicts", m_fparams.m_max_conflicts);
}
for (auto th : m_theory_set)
if (th)
th->updt_params();
}
unsigned context::relevancy_lvl() const {
@ -213,7 +218,7 @@ namespace smt {
}
ast_translation tr(src_ctx.m, m, false);
for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) {
app* e = src_ctx.m_user_propagator->get_expr(i);
auto e = src_ctx.m_user_propagator->get_expr(i);
m_user_propagator->add_expr(tr(e), true);
}
}
@ -285,8 +290,13 @@ namespace smt {
if (!decision && d.m_phase == l.sign())
m_agility += (1.0 - m_fparams.m_agility_factor);
}
bool new_phase = !l.sign();
m_stats.m_num_assignments++;
if (d.m_phase_available && d.m_phase != new_phase)
m_birthdate[l.var()] = m_stats.m_num_assignments; // reset birthdate when phase changes
d.m_phase_available = true;
d.m_phase = !l.sign();
d.m_phase = new_phase;
TRACE(assign_core, tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_smt2(tout, l) << "\n";
tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
@ -527,7 +537,8 @@ namespace smt {
mark_as_relevant(r1);
}
push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents()));
unsigned r2_num_parents = r2->get_num_parents();
m_qmanager->add_eq_eh(r1, r2);
@ -557,6 +568,10 @@ namespace smt {
SASSERT(r1->get_root() == r2);
reinsert_parents_into_cg_table(r1, r2, n1, n2, js);
// We push the add_eq_trail after reinsert_parents_into_cg_table because the latter may push merge_cgc_generations trails,
// and we want add_eq to be undone before merge_cgc_generations is undone.
push_trail(add_eq_trail(*this, r1, n1, r2_num_parents));
if (n2->is_bool())
propagate_bool_enode_assignment(r1, r2, n1, n2);
@ -584,6 +599,8 @@ namespace smt {
must be removed from the congruence table since their hash code will change.
*/
void context::remove_parents_from_cg_table(enode * r1) {
SASSERT(m_r1_parent_generations.empty());
// Remove parents from the congruence table
for (enode * parent : enode::parents(r1)) {
CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";);
@ -593,7 +610,8 @@ namespace smt {
tout << "\n";
tout << "contains: " << m_cg_table.contains(parent) << "\n";
if (m_cg_table.contains(parent)) {
tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n";
enode* owner = m_cg_table.find(parent);
tout << "owner: " << owner->get_owner_id() << "\n";
}
m_cg_table.display(tout);
);
@ -604,6 +622,8 @@ namespace smt {
SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent));
parent->set_mark();
if (parent->is_cgc_enabled()) {
if (!parent->is_eq()) // we don't track generations of equalities.
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
m_cg_table.erase(parent);
SASSERT(!m_cg_table.contains_ptr(parent));
}
@ -611,6 +631,20 @@ namespace smt {
}
}
// Sticky update to the generation number of the congruence class
// Goes out of scope when n is garbage collected.
void context::set_generation_sticky(enode * n, unsigned generation) {
SASSERT(n->uses_cg_table());
SASSERT(!n->is_eq());
// Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops.
SASSERT(generation < get_generation(n));
set_generation(n, generation);
m_sticky_generation_updates.insert(n, generation);
}
/**
\brief Reinsert the parents of r1 that were removed from the
cg_table at remove_parents_from_cg_table. Some of these parents will
@ -628,6 +662,7 @@ namespace smt {
enode_vector & r2_parents = r2->m_parents;
enode_vector & r1_parents = r1->m_parents;
unsigned num_r1_parents = r1_parents.size();
unsigned generation_cache_idx = 0;
for (unsigned i = 0; i < num_r1_parents; ++i) {
enode* parent = r1_parents[i];
if (!parent->is_marked())
@ -645,29 +680,43 @@ namespace smt {
lbool val = get_assignment(v);
if (val != l_true) {
if (val == l_false && js.get_kind() == eq_justification::CONGRUENCE)
m_dyn_ack_manager.cg_conflict_eh(n1->get_expr(), n2->get_expr());
m_dyn_ack_manager.cg_conflict_eh(n1->get_app(), n2->get_app());
assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
}
// It is not necessary to reinsert the equality to the congruence table
// (because the only congruence propagations that could lead to are already handled by the assign() here).
continue;
}
}
if (parent->is_cgc_enabled()) {
// Look up the generation cache
unsigned parent_generation = 0; // Just use generation 0 for equalities
if (!parent->is_eq()) {
auto [p, g] = m_r1_parent_generations[generation_cache_idx++];
SASSERT(p == parent);
parent_generation = g;
}
auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);
if (parent_prime == parent) {
SASSERT(parent);
SASSERT(parent->is_cgr());
SASSERT(parent->is_cgr());
SASSERT(m_cg_table.contains_ptr(parent));
parent->m_generation = parent_generation;
r2_parents.push_back(parent);
continue;
}
parent->m_cg = parent_prime;
SASSERT(!m_cg_table.contains_ptr(parent));
merge_cgc_generations(parent, parent_generation, parent_prime);
if (parent_prime->m_root != parent->m_root) {
TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id()
<< " used_commutativity: " << used_commutativity << "\n";);
push_new_congruence(parent, parent_prime, used_commutativity);
}
}
else {
// If congruence closure is not enabled for parent, then I just copy it
@ -675,6 +724,7 @@ namespace smt {
r2_parents.push_back(parent);
}
}
m_r1_parent_generations.reset();
}
/**
@ -797,7 +847,7 @@ namespace smt {
}
else {
// uncommon case: r2 will have two theory_vars attached to it.
r2->add_th_var(v1, t1, m_region);
r2->add_th_var(v1, t1, get_region());
push_new_th_diseqs(r2, v1, get_theory(t1));
push_new_th_diseqs(r1, v2, get_theory(t2));
}
@ -848,7 +898,7 @@ namespace smt {
theory_var v2 = r2->get_th_var(t1);
TRACE(merge_theory_vars, tout << get_theory(t1)->get_name() << ": " << v2 << " == " << v1 << "\n");
if (v2 == null_theory_var) {
r2->add_th_var(v1, t1, m_region);
r2->add_th_var(v1, t1, get_region());
push_new_th_diseqs(r2, v1, get_theory(t1));
}
l1 = l1->get_next();
@ -911,7 +961,7 @@ namespace smt {
lbool val2 = get_assignment(v2);
if (val2 != val) {
if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0)
m_dyn_ack_manager.cg_conflict_eh(source->get_expr(), target->get_expr());
m_dyn_ack_manager.cg_conflict_eh(source->get_app(), target->get_app());
assign(literal(v2, sign), mk_justification(mp_iff_justification(source, target)));
}
target = target->get_next();
@ -930,6 +980,8 @@ namespace smt {
// unmerge "equivalence" classes
std::swap(r1->m_next, r2->m_next);
SASSERT(m_r1_parent_generations.empty());
// remove the parents of r1 that remained as congruence roots
enode_vector::iterator it = r2->begin_parents();
enode_vector::iterator end = r2->end_parents();
@ -946,6 +998,8 @@ namespace smt {
display(tout << "\n"););
SASSERT(parent->is_cgr());
SASSERT(m_cg_table.contains_ptr(parent));
if (!parent->is_eq())
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
m_cg_table.erase(parent);
}
}
@ -960,22 +1014,52 @@ namespace smt {
// restore parents of r2
r2->m_parents.shrink(r2_num_parents);
unsigned generation_cache_idx = 0;
// try to reinsert parents of r1 that are not cgr
for (enode * parent : enode::parents(r1)) {
TRACE(add_eq_parents, tout << "visiting: #" << parent->get_owner_id() << "\n";);
if (parent->is_cgc_enabled()) {
enode * cg = parent->m_cg;
if (!parent->is_true_eq() &&
(parent == cg || // parent was root of the congruence class before and after the merge
!congruent(parent, cg) // parent was root of the congruence class before but not after the merge
)) {
(parent == cg || // parent was root of the congruence class before and after the merge
!congruent(parent, cg)) // parent was root of the congruence class before but not after the merge
) {
unsigned gen;
if (parent->is_eq()) {
gen = 0;
} else if (parent == cg) {
enode *p = nullptr;
unsigned parent_generation;
if (generation_cache_idx < m_r1_parent_generations.size()) {
std::tie(p, parent_generation) = m_r1_parent_generations[generation_cache_idx];
}
if (p == parent) {
generation_cache_idx++;
gen = parent_generation;
} else {
SASSERT(m_cg_table.contains_ptr(parent));
continue;
}
} else {
// Insert at some dummy generation here. An undo_merge_cgr will immediately follow to set the generation.
unsigned dummy_generation = 100000; // NOT UINT_MAX. In case this goes badly overflows would be hell to debug.
gen = dummy_generation;
}
auto [parent_cg, used_commutativity] = m_cg_table.insert(parent);
(void)used_commutativity;
parent->m_cg = parent_cg;
if (parent_cg == parent)
// parent is (again) the congruence root: restore its generation.
parent->m_generation = gen;
}
}
}
m_r1_parent_generations.reset();
// restore theory vars
if (r2->m_th_var_list.get_next() == nullptr) {
// common case: r2 has at most one variable
@ -1010,6 +1094,28 @@ namespace smt {
CASSERT("add_eq", check_invariant());
}
void context::undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) {
// TODO: optimization: don't bother unrolling e1 if e1 is an enode about to be garbage collected.
set_generation(e1, e1_generation);
set_generation(e2, e2_generation);
apply_sticky_updates(e1, e1_generation, e2, e2_generation);
}
void context::apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) {
SASSERT(e1->uses_cg_table());
SASSERT(e2->uses_cg_table());
// optimization opportunity: we actually just need to look at updates above the current decision level.
// Then we wouldn't have to check for minimum either.
for (auto const& [t, generation] : m_sticky_generation_updates) {
if (generation < e1_generation && congruent(t, e1)) {
set_generation(e1, generation);
} else if (generation < e2_generation && congruent(t, e2)) {
set_generation(e2, generation);
}
}
}
/**
\brief Auxiliary method for undo_add_eq.
It restores the theory variables of a given root enode.
@ -1129,7 +1235,7 @@ namespace smt {
m.inc_ref(eq);
_this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq);
}
else if (m_is_diseq_tmp->get_expr()->get_arg(0)->get_sort() != n1->get_sort()) {
else if (m_is_diseq_tmp->get_app()->get_arg(0)->get_sort() != n1->get_sort()) {
m.dec_ref(m_is_diseq_tmp->get_expr());
app * eq = m.mk_eq(n1->get_expr(), n2->get_expr());
m.inc_ref(eq);
@ -1273,17 +1379,17 @@ namespace smt {
*/
enode * context::get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) {
enode * tmp = m_tmp_enode.set(f, num_args, args);
enode * r = m_cg_table.find(tmp);
enode * r = m_cg_table.find(tmp);
#ifdef Z3DEBUG
if (r != nullptr) {
SASSERT(r->get_expr()->get_decl() == f);
SASSERT(r->get_decl() == f);
SASSERT(r->get_num_args() == num_args);
if (r->is_commutative()) {
// TODO
}
else {
for (unsigned i = 0; i < num_args; ++i) {
expr * arg = r->get_expr()->get_arg(i);
expr * arg = r->get_arg(i)->get_expr();
SASSERT(e_internalized(arg));
enode * _arg = get_enode(arg);
CTRACE(eq_to_bug, args[i]->get_root() != _arg->get_root(),
@ -1523,16 +1629,24 @@ namespace smt {
}
lbool context::find_assignment(expr * n) const {
if (m.is_false(n))
return l_false;
expr* arg = nullptr;
if (m.is_not(n, arg)) {
if (b_internalized(arg))
return ~get_assignment_core(arg);
if (m.is_false(arg))
return l_true;
if (m.is_true(arg))
return l_false;
return l_undef;
}
if (b_internalized(n))
return get_assignment(n);
if (m.is_false(n))
return l_false;
if (m.is_true(n))
return l_true;
return l_undef;
}
@ -1761,9 +1875,11 @@ namespace smt {
return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings);
}
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, //expr* def,
unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
return m_qmanager->add_instance(q, pat, num_bindings, bindings,
max_generation, min_top_generation, max_top_generation, used_enodes);
}
void context::rescale_bool_var_activity() {
@ -1938,13 +2054,13 @@ namespace smt {
m_scope_lvl++;
m_region.push_scope();
get_trail_stack().push_scope();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
// TRACE(context, tout << "push " << m_scope_lvl << "\n";);
m_relevancy_propagator->push();
s.m_assigned_literals_lim = m_assigned_literals.size();
s.m_trail_stack_lim = m_trail_stack.size();
s.m_aux_clauses_lim = m_aux_clauses.size();
s.m_justifications_lim = m_justifications.size();
s.m_units_to_reassert_lim = m_units_to_reassert.size();
@ -1960,12 +2076,6 @@ namespace smt {
CASSERT("context", check_invariant());
}
/**
\brief Execute generic undo-objects.
*/
void context::undo_trail_stack(unsigned old_size) {
::undo_trail_stack(m_trail_stack, old_size);
}
/**
\brief Remove watch literal idx from the given clause.
@ -2232,8 +2342,9 @@ namespace smt {
unsigned ilvl = e->get_iscope_lvl();
if (ilvl <= new_scope_lvl)
continue; // node and its children will not be recreated during backtracking
TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";);
m_cached_generation.insert(n, e->get_generation());
unsigned generation = get_generation(e);
TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << generation << "\n";);
m_cached_generation.insert(n, generation);
}
for (expr * arg : *to_app(n)) {
if (is_app(arg) || is_quantifier(arg))
@ -2452,23 +2563,25 @@ namespace smt {
m_relevancy_propagator->pop(num_scopes);
m_fingerprints.pop_scope(num_scopes);
unassign_vars(s.m_assigned_literals_lim);
undo_trail_stack(s.m_trail_stack_lim);
m_trail_stack.pop_scope(num_scopes);
for (theory* th : m_theory_set)
th->pop_scope_eh(num_scopes);
del_justifications(m_justifications, s.m_justifications_lim);
m_asserted_formulas.pop_scope(num_scopes);
CTRACE(propagate_atoms, !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";);
m_eq_propagation_queue.reset();
m_th_eq_propagation_queue.reset();
m_region.pop_scope(num_scopes);
m_th_diseq_propagation_queue.reset();
m_atom_propagation_queue.reset();
m_region.pop_scope(num_scopes);
m_scopes.shrink(new_lvl);
m_conflict_resolution->reset();
@ -3056,7 +3169,7 @@ namespace smt {
del_clauses(m_lemmas, 0);
del_justifications(m_justifications, 0);
reset_tmp_clauses();
undo_trail_stack(0);
m_trail_stack.reset();
m_qmanager = nullptr;
if (m_is_diseq_tmp) {
m_is_diseq_tmp->del_eh(m, false);
@ -3640,6 +3753,13 @@ namespace smt {
}
}
void context::setup_for_parallel() {
// Native SMT parallel configures the parent context before cloning workers.
// context::copy then configures/internalizes each worker copy while
// preprocessing is still enabled.
setup_context(m_fparams.m_auto_config);
}
config_mode context::get_config_mode(bool use_static_features) const {
if (!m_fparams.m_auto_config)
return CFG_BASIC;
@ -4160,9 +4280,17 @@ namespace smt {
return FC_CONTINUE;
}
if (m_final_check_idx == old_idx) {
if (level >= max_level || result == FC_DONE || can_propagate())
if (level >= max_level || result == FC_DONE || result == FC_CONTINUE || can_propagate())
break;
++level;
// Re-evaluate at the higher level: clear the give-up state
// accumulated at lower levels so a level that succeeds is
// not masked by a previous FC_GIVEUP. See e.g. theory_lra
// whose level 2 invokes the full nlsat (m_nra.check) that
// is skipped at level 1.
result = FC_DONE;
f = OK;
m_incomplete_theories.reset();
}
}
@ -4642,7 +4770,7 @@ namespace smt {
return false;
}
case 1: {
if (m_qmanager->is_shared(n) && !m.is_lambda_def(n->get_expr()) && !m_lambdas.contains(n))
if (m_qmanager->is_shared(n) && !m_lambdas.contains(n))
return true;
// the variable is shared if the equivalence class of n
@ -4652,8 +4780,7 @@ namespace smt {
theory_id th_id = l->get_id();
for (enode * parent : enode::parents(n)) {
app* p = parent->get_expr();
family_id fid = p->get_family_id();
family_id fid = parent->get_family_id();
if (fid != th_id && fid != m.get_basic_family_id()) {
if (is_beta_redex(parent, n))
continue;
@ -4701,7 +4828,7 @@ namespace smt {
}
bool context::is_beta_redex(enode* p, enode* n) const {
family_id th_id = p->get_expr()->get_family_id();
family_id th_id = p->get_family_id();
theory * th = get_theory(th_id);
return th && th->is_beta_redex(p, n);
}
@ -4854,7 +4981,7 @@ namespace smt {
m_model->add_rec_funs();
}
};
}
#ifdef Z3DEBUG

126
src/smt/smt_context.h
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#pragma once
#include <atomic>
#include "ast/quantifier_stat.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "smt/smt_clause.h"
@ -45,6 +46,7 @@ Revision History:
#include "util/ref.h"
#include "util/timer.h"
#include "util/statistics.h"
#include "util/map.h"
#include "smt/fingerprints.h"
#include "smt/proto_model/proto_model.h"
#include "smt/theory_user_propagator.h"
@ -63,6 +65,10 @@ namespace smt {
class model_generator;
class context;
class kernel;
// Hash table for storing enode -> generation mappings
typedef ptr_addr_map<enode, unsigned> enode_generation_table;
struct oom_exception : public z3_error {
oom_exception() : z3_error(ERR_MEMOUT) {}
@ -84,6 +90,7 @@ namespace smt {
friend class model_generator;
friend class lookahead;
friend class parallel;
friend class kernel;
public:
statistics m_stats;
@ -101,6 +108,7 @@ namespace smt {
setup m_setup;
unsigned m_relevancy_lvl;
timer m_timer;
region m_region;
asserted_formulas m_asserted_formulas;
th_rewriter m_rewriter;
scoped_ptr<quantifier_manager> m_qmanager;
@ -113,7 +121,6 @@ namespace smt {
progress_callback * m_progress_callback;
unsigned m_next_progress_sample;
clause_proof m_clause_proof;
region m_region;
fingerprint_set m_fingerprints;
expr_ref_vector m_b_internalized_stack; // stack of the boolean expressions already internalized.
@ -121,7 +128,6 @@ namespace smt {
// enodes. Examples: boolean expression nested in an
// uninterpreted function.
expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes.
quantifier_ref_vector m_l_internalized_stack;
ptr_vector<justification> m_justifications;
@ -137,6 +143,7 @@ namespace smt {
scoped_ptr<base_dependent_expr_state> m_fmls;
svector<double> m_lit_scores[2];
svector<unsigned> m_birthdate;
// -----------------------------------
@ -153,6 +160,8 @@ namespace smt {
vector<enode_vector> m_decl2enodes; // decl -> enode (for decls with arity > 0)
enode_vector m_empty_vector;
cg_table m_cg_table;
enode_generation_table m_sticky_generation_updates;
vector<std::pair<enode*, unsigned>> m_r1_parent_generations; // temporary field used to cache generations between remove_parents_from_cg_table and reinsert_parents_into_cg_table
struct new_eq {
enode * m_lhs;
enode * m_rhs;
@ -290,6 +299,10 @@ namespace smt {
return m_fparams;
}
smt_params const& get_fparams() const {
return m_fparams;
}
params_ref const & get_params() {
return m_params;
}
@ -450,6 +463,8 @@ namespace smt {
svector<double> const & get_activity_vector() const { return m_activity; }
double get_activity(bool_var v) const { return m_activity[v]; }
unsigned get_num_assignments() const { return m_stats.m_num_assignments; }
unsigned get_birthdate(bool_var v) const { return m_birthdate[v]; }
void set_activity(bool_var v, double act) { m_activity[v] = act; }
@ -536,6 +551,8 @@ namespace smt {
return m_scope_lvl == m_search_lvl;
}
void pop_to_search_level() { pop_to_search_lvl(); }
bool tracking_assumptions() const {
return !m_assumptions.empty() && m_search_lvl > m_base_lvl;
}
@ -603,6 +620,26 @@ namespace smt {
return m_qmanager->get_generation(q);
}
unsigned get_generation(enode * e) const {
// We don't support patterns with equality so there is no need to track generations for them.
if (e->is_eq())
return 0;
return get_cg_root(e)->m_generation;
}
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) {
unsigned max = 0;
for (unsigned i = 0; i < num_enodes; ++i) {
unsigned curr = get_generation(enodes[i]);
if (curr > max)
max = curr;
}
return max;
}
void set_generation(enode * e, unsigned generation);
/**
\brief Return true if the logical context internalized universal quantifiers.
*/
@ -617,8 +654,8 @@ namespace smt {
return m_asserted_formulas.has_quantifiers();
}
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) {
return m_fingerprints.insert(data, data_hash, num_args, args, def);
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
return m_fingerprints.insert(data, data_hash, num_args, args);
}
theory_id get_var_theory(bool_var v) const {
@ -643,7 +680,6 @@ namespace smt {
//
// -----------------------------------
protected:
typedef ptr_vector<trail > trail_stack;
trail_stack m_trail_stack;
#ifdef Z3DEBUG
bool m_trail_enabled { true };
@ -653,11 +689,15 @@ namespace smt {
template<typename TrailObject>
void push_trail(const TrailObject & obj) {
SASSERT(m_trail_enabled);
m_trail_stack.push_back(new (m_region) TrailObject(obj));
m_trail_stack.push(obj);
}
void push_trail_ptr(trail * ptr) {
m_trail_stack.push_back(ptr);
m_trail_stack.push_ptr(ptr);
}
trail_stack& get_trail_stack() {
return m_trail_stack;
}
protected:
@ -667,7 +707,6 @@ namespace smt {
unsigned m_search_lvl { 0 }; // It is greater than m_base_lvl when assumptions are used. Otherwise, it is equals to m_base_lvl
struct scope {
unsigned m_assigned_literals_lim;
unsigned m_trail_stack_lim;
unsigned m_aux_clauses_lim;
unsigned m_justifications_lim;
unsigned m_units_to_reassert_lim;
@ -687,8 +726,6 @@ namespace smt {
void pop_scope(unsigned num_scopes);
void undo_trail_stack(unsigned old_size);
void unassign_vars(unsigned old_lim);
void remove_watch_literal(clause * cls, unsigned idx);
@ -782,6 +819,13 @@ namespace smt {
return get_bdata(get_bool_var(n));
}
void update_generation(enode * n);
void update_generation(expr * e) {
if (is_app(e) && e_internalized(e))
update_generation(get_enode(to_app(e)));
}
typedef std::pair<expr *, bool> expr_bool_pair;
void ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited);
@ -860,18 +904,8 @@ namespace smt {
mk_enode_trail m_mk_enode_trail;
void undo_mk_enode();
friend class mk_lambda_trail;
class mk_lambda_trail : public trail {
context& ctx;
public:
mk_lambda_trail(context& ctx) :ctx(ctx) {}
void undo() override { ctx.undo_mk_lambda(); }
};
mk_lambda_trail m_mk_lambda_trail;
void undo_mk_lambda();
void apply_sort_cnstr(app * term, enode * e);
void apply_sort_cnstr(expr * term, enode * e);
bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits);
@ -949,6 +983,8 @@ namespace smt {
void internalize(expr * n, bool gate_ctx, unsigned generation);
enode *non_ground_internalize(expr *e);
clause * mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k = CLS_AUX, clause_del_eh * del_eh = nullptr);
void mk_clause(literal l1, literal l2, justification * j);
@ -1015,13 +1051,13 @@ namespace smt {
bool_var mk_bool_var(expr * n);
enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled);
enode * mk_enode(expr * n, bool suppress_args, bool merge_tf, bool cgc_enabled);
void attach_th_var(enode * n, theory * th, theory_var v);
template<typename Justification>
justification * mk_justification(Justification const & j) {
justification * js = new (m_region) Justification(j);
justification * js = new (get_region()) Justification(j);
SASSERT(js->in_region());
if (js->has_del_eh())
m_justifications.push_back(js);
@ -1103,8 +1139,8 @@ namespace smt {
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings,
unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
void set_global_generation(unsigned generation) { m_generation = generation; }
@ -1122,12 +1158,16 @@ namespace smt {
void push_new_th_diseq(theory_id th, theory_var lhs, theory_var rhs);
friend class add_eq_trail;
friend class merge_cgc_generations_trail;
void remove_parents_from_cg_table(enode * r1);
void reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js);
void merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2);
void set_generation_sticky(enode * e, unsigned generation);
void invert_trans(enode * n);
theory_var get_closest_var(enode * n, theory_id th_id);
@ -1138,13 +1178,17 @@ namespace smt {
void propagate_bool_enode_assignment_core(enode * source, enode * target);
void undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation);
void apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation);
void undo_add_eq(enode * r1, enode * n1, unsigned r2_num_parents);
void restore_theory_vars(enode * r2, enode * r1);
void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
if (lhs->get_root() != rhs->get_root()) {
SASSERT(lhs->get_expr()->get_sort() == rhs->get_expr()->get_sort());
SASSERT(lhs->get_sort() == rhs->get_sort());
m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
}
}
@ -1184,6 +1228,18 @@ namespace smt {
static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); }
enode * get_cg_root(enode * n) const {
if (!n->uses_cg_table())
return n;
// Fast path: if e is already the congruence root, avoid table lookup.
// This is important for performance, since get_cg_root is called on every generation lookup.
if (n->is_cgr())
return n;
auto r = m_cg_table.find(n);
SASSERT(r != nullptr);
return r;
}
bool is_diseq(enode * n1, enode * n2) const;
bool is_diseq_slow(enode * n1, enode * n2) const;
@ -1698,6 +1754,8 @@ namespace smt {
lbool setup_and_check(bool reset_cancel = true);
void setup_for_parallel();
void reduce_assertions();
bool resource_limits_exceeded();
@ -1722,8 +1780,16 @@ namespace smt {
void internalize_instance(expr * body, proof * pr, unsigned generation) {
internalize_assertion(body, pr, generation);
if (relevancy())
if (relevancy()) {
// if the instantiation creates a conflict, we backtrack immediately.
// to retain the conflict clause being relevant we mark it here.
// if the instantiation does not create a conflict, default relevancy propagation applies.
if (inconsistent() && is_app(body)) {
for (auto arg : *to_app(body))
mark_as_relevant(arg);
}
m_case_split_queue->internalize_instance_eh(body, generation);
}
}
unsigned get_unsat_core_size() const {
@ -1913,6 +1979,4 @@ namespace smt {
std::ostream& operator<<(std::ostream& out, enode_pp const& p);
};
}

2
src/smt/smt_context_inv.cpp
View file

@ -420,5 +420,5 @@ namespace smt {
}
}
};
}

7
src/smt/smt_context_pp.cpp
View file

@ -423,6 +423,7 @@ namespace smt {
st.update("minimized lits", m_stats.m_num_minimized_lits);
st.update("num checks", m_stats.m_num_checks);
st.update("mk bool var", m_stats.m_num_mk_bool_var ? m_stats.m_num_mk_bool_var - 1 : 0);
st.update("random seed", m_fparams.m_random_seed);
m_qmanager->collect_statistics(st);
m_asserted_formulas.collect_statistics(st);
for (theory* th : m_theory_set) {
@ -544,14 +545,14 @@ namespace smt {
out << std::left << n->get_owner_id() << " #";
out.width(5);
out << n->get_root()->get_owner_id() << " := " << std::right;
unsigned num = n->get_expr()->get_num_args();
unsigned num = n->get_num_args();
if (num > 0)
out << "(";
out << n->get_decl()->get_name();
if (!n->get_decl()->private_parameters())
display_parameters(out, n->get_decl()->get_num_parameters(), n->get_decl()->get_parameters());
for (unsigned i = 0; i < num; ++i) {
expr * arg = n->get_expr()->get_arg(i);
expr * arg = n->get_arg(i)->get_expr();
if (e_internalized(arg)) {
enode * n = get_enode(arg)->get_root();
out << " #" << n->get_owner_id();
@ -785,5 +786,5 @@ namespace smt {
IF_VERBOSE(2, verbose_stream() << str);
}
};
}

2
src/smt/smt_context_stat.cpp
View file

@ -145,4 +145,4 @@ namespace smt {
if (m_fparams.m_profile_res_sub)
display_profile_res_sub(out);
}
};
}

56
src/smt/smt_enode.cpp
View file

@ -21,11 +21,11 @@ Revision History:
#include "smt/smt_enode.h"
namespace smt {
/**
\brief Initialize an enode in the given memory position.
*/
enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner,
enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
@ -42,7 +42,7 @@ namespace smt {
n->m_interpreted = false;
n->m_suppress_args = suppress_args;
n->m_eq = m.is_eq(owner);
n->m_commutative = n->get_num_args() == 2 && owner->get_decl()->is_commutative();
n->m_commutative = n->get_num_args() == 2 && n->get_decl()->is_commutative();
n->m_bool = m.is_bool(owner);
n->m_merge_tf = merge_tf;
n->m_cgc_enabled = cgc_enabled;
@ -52,7 +52,7 @@ namespace smt {
n->m_is_shared = 2;
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
enode * arg = app2enode[owner->get_arg(i)->get_id()];
enode * arg = app2enode[to_app(owner)->get_arg(i)->get_id()];
n->m_args[i] = arg;
arg->get_root()->m_is_shared = 2;
SASSERT(n->get_arg(i) == arg);
@ -64,11 +64,11 @@ namespace smt {
return n;
}
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
unsigned sz = get_enode_size(suppress_args ? 0 : owner->get_num_args());
unsigned sz = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args());
void * mem = r.allocate(sz);
return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
}
@ -131,19 +131,6 @@ namespace smt {
m_th_var_list.del_var(id);
}
/**
\brief Push old value of generation on the context trail stack
and update the generation.
*/
void enode::set_generation(context & ctx, unsigned generation) {
if (m_generation == generation)
return;
ctx.push_trail(value_trail<unsigned>(m_generation));
m_generation = generation;
}
void enode::set_lbl_hash(context & ctx) {
SASSERT(m_lbl_hash == -1);
// m_lbl_hash should be different from -1, if and only if,
@ -160,16 +147,17 @@ namespace smt {
}
}
enode * enode::get_eq_enode_with_min_gen() {
if (m_generation == 0)
return this;
enode * enode::get_eq_enode_with_min_gen(context * ctx) {
enode * r = this;
enode * curr = this;
unsigned r_gen = ctx->get_generation(r);
do {
if (curr->m_generation < r->m_generation) {
unsigned curr_gen = ctx->get_generation(curr);
if (curr_gen == 0)
return curr;
if (curr_gen < r_gen) {
r = curr;
if (r->m_generation == 0)
return r;
r_gen = curr_gen;
}
curr = curr->m_next;
}
@ -279,7 +267,7 @@ namespace smt {
bool congruent(enode * n1, enode * n2, bool & comm) {
comm = false;
if (n1->get_expr()->get_decl() != n2->get_expr()->get_decl())
if (!n1->is_app() || n1->get_decl() != n2->get_decl())
return false;
unsigned num_args = n1->get_num_args();
if (num_args != n2->get_num_args())
@ -306,16 +294,6 @@ namespace smt {
}
}
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) {
unsigned max = 0;
for (unsigned i = 0; i < num_enodes; ++i) {
unsigned curr = enodes[i]->get_generation();
if (curr > max)
max = curr;
}
return max;
}
void unmark_enodes(unsigned num_enodes, enode * const * enodes) {
for (unsigned i = 0; i < num_enodes; ++i)
enodes[i]->unset_mark();
@ -373,5 +351,5 @@ namespace smt {
get_enode()->m_func_decl_id = UINT_MAX;
}
};
}

50
src/smt/smt_enode.h
View file

@ -59,12 +59,12 @@ namespace smt {
equality propagation, and the theory central bus of equalities.
*/
class enode {
app * m_owner; //!< The application that 'owns' this enode.
expr * m_owner; //!< The application that 'owns' this enode.
enode * m_root; //!< Representative of the equivalence class
enode * m_next; //!< Next element in the equivalence class.
enode * m_cg;
unsigned m_class_size; //!< Size of the equivalence class if the enode is the root.
unsigned m_generation; //!< Tracks how many quantifier instantiation rounds were needed to generate this enode.
unsigned m_generation; //!< Cached generation of the congruence class. Valid when is_cgr(), or when the enode does not use the cg_table (constants/leaves/true-eq nodes), where it directly stores the enode's generation.
unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing.
@ -102,7 +102,7 @@ namespace smt {
approx_set m_lbls;
approx_set m_plbls;
enode * m_args[0]; //!< Cached args
friend class context;
friend class conflict_resolution;
friend class quantifier_manager;
@ -132,7 +132,7 @@ namespace smt {
friend class tmp_enode;
static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner,
static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
public:
@ -141,9 +141,9 @@ namespace smt {
return sizeof(enode) + num_args * sizeof(enode*);
}
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
@ -166,16 +166,28 @@ namespace smt {
void del_eh(ast_manager & m, bool update_children_parent = true);
app * get_expr() const { return m_owner; }
app * get_app() const { SASSERT(is_app()); return to_app(m_owner); }
expr *get_expr() const {
return m_owner;
}
bool is_app() const {
return ::is_app(m_owner);
}
unsigned get_owner_id() const { return m_owner->get_id(); }
unsigned get_expr_id() const { return m_owner->get_id(); }
func_decl * get_decl() const { return m_owner->get_decl(); }
unsigned get_decl_id() const { return m_owner->get_decl()->get_small_id(); }
func_decl * get_decl() const { return is_app() ? to_app(m_owner)->get_decl() : nullptr; }
unsigned get_decl_id() const { return is_app() ? to_app(m_owner)->get_decl()->get_small_id() : 43; }
sort* get_sort() const { return m_owner->get_sort(); }
family_id get_family_id() const {
return is_app() ? to_app(m_owner)->get_family_id() : basic_family_id;
}
unsigned hash() const {
return m_owner->hash();
}
@ -213,7 +225,7 @@ namespace smt {
}
unsigned get_num_args() const {
return m_suppress_args ? 0 : m_owner->get_num_args();
return m_suppress_args || !is_app() ? 0 : to_app(m_owner)->get_num_args();
}
enode * get_arg(unsigned idx) const {
@ -302,6 +314,10 @@ namespace smt {
return m_cg;
}
bool uses_cg_table() const {
return get_num_args() > 0 && is_cgc_enabled() && !is_true_eq();
}
bool is_cgc_enabled() const {
return m_cgc_enabled;
}
@ -381,18 +397,12 @@ namespace smt {
trans_justification get_trans_justification() {
return m_trans;
}
unsigned get_generation() const {
return m_generation;
}
void set_generation(context & ctx, unsigned generation);
/**
\brief Return the enode n that is in the eqc of *this, and has the minimal generation.
That is, there is no other enode with smaller generation.
*/
enode * get_eq_enode_with_min_gen();
enode * get_eq_enode_with_min_gen(context * ctx);
unsigned get_iscope_lvl() const {
return m_iscope_lvl;
@ -447,8 +457,6 @@ namespace smt {
bool aux;
return congruent(n1, n2, aux);
}
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes);
void unmark_enodes(unsigned num_enodes, enode * const * enodes);
@ -468,6 +476,6 @@ namespace smt {
};
inline mk_pp pp(enode* n, ast_manager& m) { return mk_pp(n->get_expr(), m); }
};
}

2
src/smt/smt_eq_justification.h
View file

@ -78,6 +78,6 @@ namespace smt {
};
const eq_justification null_eq_justification(static_cast<justification*>(nullptr));
};
}

2
src/smt/smt_failure.h
View file

@ -35,5 +35,5 @@ namespace smt {
QUANTIFIERS //!< Logical context contains universal quantifiers.
};
};
}

2
src/smt/smt_for_each_relevant_expr.cpp
View file

@ -295,4 +295,4 @@ namespace smt {
m_manager.is_label(n, pos, m_buffer); // copy symbols to buffer
}
};
}

4
src/smt/smt_for_each_relevant_expr.h
View file

@ -35,7 +35,7 @@ namespace smt {
unsigned count_at_labels_lit(expr* n, bool polarity);
public:
check_at_labels(ast_manager& m) : m_manager(m) {};
check_at_labels(ast_manager& m) : m_manager(m) {}
/**
\brief Check that 'n' as a formula contains at most one @ label within each and-or path.
@ -105,6 +105,6 @@ namespace smt {
void operator()(expr * n) override;
};
};
}

2
src/smt/smt_implied_equalities.h
View file

@ -36,6 +36,6 @@ namespace smt {
unsigned* class_ids);
};
}

166
src/smt/smt_internalizer.cpp
View file

@ -101,6 +101,63 @@ namespace smt {
}
}
void context::update_generation(enode * e) {
// We don't support patterns with equality so there is no need to track generations for them.
if (e->is_eq())
return;
if (0 < m_generation && m_generation < get_generation(e)) {
if (e->uses_cg_table())
set_generation_sticky(e, m_generation);
else
set_generation(e, m_generation);
}
}
void context::set_generation(enode * e, unsigned generation) {
// We don't support patterns with equality so there is no need to track generations for them.
if (e->is_eq())
return;
// The class generation is stored in the congruence root's m_generation field.
enode * cgr = get_cg_root(e);
cgr->m_generation = generation;
}
class merge_cgc_generations_trail : public trail {
context& ctx;
enode* m_e1;
unsigned m_e1_generation;
enode* m_e2;
unsigned m_e2_generation;
public:
merge_cgc_generations_trail(context& ctx, enode* e1, unsigned e1_generation, enode* e2, unsigned e2_generation):
ctx(ctx),
m_e1(e1),
m_e1_generation(e1_generation),
m_e2(e2),
m_e2_generation(e2_generation) {
}
void undo() override {
ctx.undo_merge_cgc_generations(m_e1, m_e1_generation, m_e2, m_e2_generation);
}
};
void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2) {
SASSERT(e2->is_cgr());
SASSERT(!m_cg_table.contains_ptr(e1));
SASSERT(m_cg_table.contains_ptr(e2));
// Push trail even if we have a no-op. Otherwise we can't restore e1's generation after unmerging.
push_trail(merge_cgc_generations_trail(*this, e1, e1_generation, e2, e2->m_generation));
if (e1_generation >= e2->m_generation)
return; // no-op
e2->m_generation = e1_generation;
}
void context::ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited) {
if (get_color(tcolors, fcolors, n, gate_ctx) == White) {
todo.push_back(expr_bool_pair(n, gate_ctx));
@ -115,12 +172,16 @@ namespace smt {
return true;
SASSERT(is_app(n));
if (m.is_bool(n)) {
if (b_internalized(n))
if (b_internalized(n)) {
update_generation(n);
return true;
}
}
else {
if (e_internalized(n))
update_generation(n);
if (e_internalized(n))
return true;
}
bool visited = true;
@ -358,6 +419,28 @@ namespace smt {
internalize_rec(n, gate_ctx);
}
enode *context::non_ground_internalize(expr *e) {
if (e_internalized(e))
return get_enode(e);
if (is_ground(e)) {
internalize(e, false);
return get_enode(e);
}
for (auto arg : subterms::ground(expr_ref(e, m))) {
if ((is_forall(arg) || is_exists(arg)) && !e_internalized(arg)) {
expr_ref fn(m.mk_fresh_const("proxy-expr", e->get_sort()), m);
expr_ref eq(m.mk_eq(fn, e), m);
assert_expr(eq);
internalize_assertions();
if (!e_internalized(fn))
internalize(fn, false);
return get_enode(fn);
}
}
internalize(e, false);
return get_enode(e);
}
void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
internalize_deep(exprs, num_exprs);
for (unsigned i = 0; i < num_exprs; ++i)
@ -404,6 +487,8 @@ namespace smt {
bool_var v = get_bool_var(n);
TRACE(internalize_bug, tout << "#" << n->get_id() << " already has bool_var v" << v << "\n";);
update_generation(n);
// n was already internalized as boolean, but an enode was
// not associated with it. So, an enode is necessary, if
// n is not in the context of a gate and is an application.
@ -586,31 +671,10 @@ namespace smt {
SASSERT(is_lambda(q));
if (e_internalized(q))
return;
app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
app_ref eq(m), lam_app(m);
expr_ref_vector vars(m);
vars.push_back(lam_name);
unsigned sz = q->get_num_decls();
for (unsigned i = 0; i < sz; ++i)
vars.push_back(m.mk_var(sz - i - 1, q->get_decl_sort(i)));
array_util autil(m);
lam_app = autil.mk_select(vars.size(), vars.data());
eq = m.mk_eq(lam_app, q->get_expr());
quantifier_ref fa(m);
expr * patterns[1] = { m.mk_pattern(lam_app) };
fa = m.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m.lambda_def_qid(), symbol::null, 1, patterns);
internalize_quantifier(fa, true);
if (!e_internalized(lam_name))
internalize_uninterpreted(lam_name);
enode* lam_node = get_enode(lam_name);
push_trail(insert_obj_map<enode, quantifier*>(m_lambdas, lam_node));
m_lambdas.insert(lam_node, q);
m_app2enode.setx(q->get_id(), lam_node, nullptr);
m_l_internalized_stack.push_back(q);
m_trail_stack.push_back(&m_mk_lambda_trail);
bool_var bv = get_bool_var(fa);
assign(literal(bv, false), nullptr);
mark_as_relevant(bv);
auto e = mk_enode(q, true, /* do suppress args */
false, /* it is a term, so it should not be merged with true/false */
true);
apply_sort_cnstr(q, e);
}
bool context::has_lambda() {
@ -810,6 +874,8 @@ namespace smt {
*/
void context::internalize_term(app * n) {
if (e_internalized(n)) {
enode * e = get_enode(n);
update_generation(e);
theory * th = m_theories.get_plugin(n->get_family_id());
if (th != nullptr) {
// This code is necessary because some theories may decide
@ -822,7 +888,6 @@ namespace smt {
// Later, the core tries to internalize (f (* 2 x)).
// Now, (* 2 x) is not internal to arithmetic anymore,
// and a theory variable must be created for it.
enode * e = get_enode(n);
if (!th->is_attached_to_var(e))
th->internalize_term(n);
}
@ -935,6 +1000,8 @@ namespace smt {
m_lit_scores[0].reserve(v + 1);
m_lit_scores[1].reserve(v + 1);
m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
m_birthdate.reserve(v+1);
m_birthdate[v] = 0;
literal l(v, false);
literal not_l(v, true);
@ -958,7 +1025,7 @@ namespace smt {
m_activity[v] = 0.0;
m_case_split_queue->mk_var_eh(v);
m_b_internalized_stack.push_back(n);
m_trail_stack.push_back(&m_mk_bool_var_trail);
m_trail_stack.push_ptr(&m_mk_bool_var_trail);
m_stats.m_num_mk_bool_var++;
SASSERT(check_bool_var_vector_sizes());
return v;
@ -997,7 +1064,7 @@ namespace smt {
\remark If suppress_args is true, then the enode is viewed as a constant
in the egraph.
*/
enode * context::mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled) {
enode * context::mk_enode(expr * n, bool suppress_args, bool merge_tf, bool cgc_enabled) {
TRACE(mk_enode_detail, tout << mk_pp(n, m) << "\nsuppress_args: " << suppress_args << ", merge_tf: " <<
merge_tf << ", cgc_enabled: " << cgc_enabled << "\n";);
SASSERT(!e_internalized(n));
@ -1009,7 +1076,8 @@ namespace smt {
CTRACE(cached_generation, generation != m_generation,
tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
}
enode * e = enode::mk(m, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl,
cgc_enabled, true);
TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
if (m.is_unique_value(n))
e->mark_as_interpreted();
@ -1017,7 +1085,7 @@ namespace smt {
TRACE(generation, tout << "mk_enode: " << id << " " << generation << "\n";);
m_app2enode.setx(id, e, nullptr);
m_e_internalized_stack.push_back(n);
m_trail_stack.push_back(&m_mk_enode_trail);
m_trail_stack.push_ptr(&m_mk_enode_trail);
m_enodes.push_back(e);
if (e->get_num_args() > 0) {
if (e->is_true_eq()) {
@ -1031,6 +1099,9 @@ namespace smt {
auto [e_prime, used_commutativity] = m_cg_table.insert(e);
if (e != e_prime) {
e->m_cg = e_prime;
// We don't support patterns with equality so there is no need to track generations for them.
if (!e->is_eq())
merge_cgc_generations(e, generation, e_prime);
push_new_congruence(e, e_prime, used_commutativity);
}
else {
@ -1042,12 +1113,13 @@ namespace smt {
}
}
if (!e->is_eq()) {
unsigned decl_id = n->get_decl()->get_small_id();
unsigned decl_id = e->get_decl_id();
if (decl_id >= m_decl2enodes.size())
m_decl2enodes.resize(decl_id+1);
m_decl2enodes[decl_id].push_back(e);
}
}
SASSERT(e_internalized(n));
m_stats.m_num_mk_enode++;
TRACE(mk_enode, tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n";
@ -1058,19 +1130,11 @@ namespace smt {
SCTRACE(causality, m_coming_from_quant, tout << "EN: #" << e->get_owner_id() << "\n";);
if (m.has_trace_stream())
m.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";
m.trace_stream() << "[attach-enode] #" << n->get_id() << " " << generation << "\n";
return e;
}
void context::undo_mk_lambda() {
SASSERT(!m_l_internalized_stack.empty());
m_stats.m_num_del_enode++;
quantifier * n = m_l_internalized_stack.back();
m_app2enode[n->get_id()] = nullptr;
m_l_internalized_stack.pop_back();
}
void context::undo_mk_enode() {
SASSERT(!m_e_internalized_stack.empty());
m_stats.m_num_del_enode++;
@ -1078,15 +1142,15 @@ namespace smt {
TRACE(undo_mk_enode, tout << "undo_enode: #" << n->get_id() << "\n" << mk_pp(n, m) << "\n";);
TRACE(mk_var_bug, tout << "undo_mk_enode: " << n->get_id() << "\n";);
unsigned n_id = n->get_id();
SASSERT(is_app(n));
enode * e = m_app2enode[n_id];
m_app2enode[n_id] = nullptr;
if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {
if (e->is_cgr() && e->uses_cg_table()) {
SASSERT(m_cg_table.contains_ptr(e));
m_cg_table.erase(e);
}
SASSERT(!(e->get_num_args() > 0 && m_cg_table.contains_ptr(e)));
if (e->get_num_args() > 0 && !e->is_eq()) {
unsigned decl_id = to_app(n)->get_decl()->get_small_id();
unsigned decl_id = e->get_decl_id();
SASSERT(decl_id < m_decl2enodes.size());
SASSERT(m_decl2enodes[decl_id].back() == e);
m_decl2enodes[decl_id].pop_back();
@ -1095,13 +1159,14 @@ namespace smt {
SASSERT(m_e_internalized_stack.size() == m_enodes.size());
m_enodes.pop_back();
m_e_internalized_stack.pop_back();
m_sticky_generation_updates.erase(e);
}
/**
\brief Apply sort constraints on e.
*/
void context::apply_sort_cnstr(app * term, enode * e) {
sort * s = term->get_decl()->get_range();
void context::apply_sort_cnstr(expr * term, enode * e) {
sort * s = term->get_sort();
theory * th = m_theories.get_plugin(s->get_family_id());
if (th) {
th->apply_sort_cnstr(e, s);
@ -1859,11 +1924,11 @@ namespace smt {
if (old_v == null_theory_var) {
enode * r = n->get_root();
theory_var v2 = r->get_th_var(th_id);
n->add_th_var(v, th_id, m_region);
n->add_th_var(v, th_id, get_region());
push_trail(add_th_var_trail(n, th_id));
if (v2 == null_theory_var) {
if (r != n)
r->add_th_var(v, th_id, m_region);
r->add_th_var(v, th_id, get_region());
push_new_th_diseqs(r, v, th);
}
else if (r != n) {
@ -1882,5 +1947,4 @@ namespace smt {
}
SASSERT(th->is_attached_to_var(n));
}
};
}

5
src/smt/smt_justification.cpp
View file

@ -351,8 +351,9 @@ namespace smt {
proof * ext_theory_propagation_justification::mk_proof(conflict_resolution & cr) {
ptr_buffer<proof> prs;
if (!antecedent2proof(cr, prs))
if (!antecedent2proof(cr, prs)) {
return nullptr;
}
context & ctx = cr.get_context();
ast_manager & m = cr.get_manager();
expr_ref fact(m);
@ -439,5 +440,5 @@ namespace smt {
return m.mk_th_lemma(m_th_id, m.mk_or(lits), 0, nullptr, m_params.size(), m_params.data());
}
};
}

2
src/smt/smt_justification.h
View file

@ -423,6 +423,6 @@ namespace smt {
char const * get_name() const override { return "theory-lemma"; }
};
};
}

14
src/smt/smt_kernel.cpp
View file

@ -280,10 +280,22 @@ namespace smt {
smt_params_helper::collect_param_descrs(d);
}
void kernel::pop_to_base_level() {
m_imp->m_kernel.pop_to_base_lvl();
}
void kernel::set_preprocess(bool f) {
m_imp->m_kernel.get_fparams().m_preprocess = f;
}
context & kernel::get_context() {
return m_imp->m_kernel;
}
context const& kernel::get_context() const {
return m_imp->m_kernel;
}
void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
m_imp->m_kernel.get_levels(vars, depth);
}
@ -340,4 +352,4 @@ namespace smt {
m_imp->m_kernel.user_propagate_initialize_value(var, value);
}
};
}

8
src/smt/smt_kernel.h
View file

@ -300,6 +300,10 @@ namespace smt {
*/
static void collect_param_descrs(param_descrs & d);
void pop_to_base_level();
void set_preprocess(bool f);
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause);
/**
@ -340,6 +344,6 @@ namespace smt {
\warning This method should not be used in new code.
*/
context & get_context();
context const& get_context() const;
};
};
}

2
src/smt/smt_literal.cpp
View file

@ -116,5 +116,5 @@ namespace smt {
}
};
}

2
src/smt/smt_literal.h
View file

@ -54,6 +54,6 @@ namespace smt {
bool backward_subsumption(unsigned num_lits1, literal const * lits1, unsigned num_lits2, literal const * lits2);
};
}

69
src/smt/smt_model_checker.cpp
View file

@ -109,7 +109,7 @@ namespace smt {
for (auto const& kv : *m_root2value) {
enode * n = kv.m_key;
expr * val = kv.m_value;
n = n->get_eq_enode_with_min_gen();
n = n->get_eq_enode_with_min_gen(m_context);
expr* e = n->get_expr();
if (!m.is_value(e))
m_value2expr.insert(val, e);
@ -203,7 +203,7 @@ namespace smt {
unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q.
SASSERT(sks.size() >= num_decls);
expr_ref_vector bindings(m), defs(m);
expr_ref_vector bindings(m);
expr_ref def(m);
bindings.resize(num_decls);
unsigned max_generation = 0;
@ -219,10 +219,11 @@ namespace smt {
if (use_inv) {
unsigned sk_term_gen = 0;
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, *cex, sk_term_gen);
if (sk_term != nullptr) {
TRACE(model_checker, tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
SASSERT(!m.is_model_value(sk_term));
// get_inv may return a model value in polymorphic settings;
// this is handled downstream by get_type_compatible_term.
max_generation = std::max(sk_term_gen, max_generation);
sk_value = sk_term;
}
@ -233,15 +234,10 @@ namespace smt {
}
else {
expr * sk_term = get_term_from_ctx(sk_value);
func_decl * f = nullptr;
if (sk_term != nullptr) {
TRACE(model_checker, tout << "sk term " << mk_pp(sk_term, m) << "\n");
sk_value = sk_term;
}
// last ditch: am I an array?
else if (false && autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_array_interp(f)) {
sk_value = cex->get_func_interp(f)->get_array_interp(f);
}
}
if (contains_model_value(sk_value)) {
@ -249,6 +245,7 @@ namespace smt {
sk_value = get_type_compatible_term(sk_value);
}
func_decl * f = nullptr;
expr_ref sk_term(sk_value, m);
if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_interp()) {
expr_ref body(cex->get_func_interp(f)->get_interp(), m);
if (contains_model_value(body))
@ -257,30 +254,25 @@ namespace smt {
svector<symbol> names;
for (unsigned i = 0; i < f->get_arity(); ++i)
names.push_back(symbol(i));
defined_names dn(m);
body = replace_value_from_ctx(body);
body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), body);
// sk_value = m.mk_fresh_const(0, m.get_sort(sk_value)); // get rid of as-array
body = dn.mk_definition(body, to_app(sk_value));
defs.push_back(body);
sk_term = body;
}
bindings.set(num_decls - i - 1, sk_value);
bindings.set(num_decls - i - 1, sk_term);
}
TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\ndefs:\n" << defs << "\n";);
if (!defs.empty()) def = mk_and(defs);
TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n");
max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation, def.get());
add_instance(q, bindings, max_generation);
return true;
}
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation, expr* def) {
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
SASSERT(q->get_num_decls() == bindings.size());
unsigned offset = m_pinned_exprs.size();
m_pinned_exprs.append(bindings);
m_pinned_exprs.push_back(q);
m_pinned_exprs.push_back(def);
m_new_instances.push_back(instance(q, offset, def, max_generation));
m_new_instances.push_back(instance(q, offset, max_generation));
}
void model_checker::operator()(expr *n) {
@ -354,7 +346,8 @@ namespace smt {
return false;
TRACE(model_checker, tout << "skolems:\n" << sks << "\n";);
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
flet<bool> l1(m_aux_context->get_fparams().m_array_fake_support, true);
flet<bool> l2(m_aux_context->get_fparams().m_preprocess, true);
lbool r = m_aux_context->check();
TRACE(model_checker, tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
@ -371,7 +364,8 @@ namespace smt {
unsigned num_new_instances = 0;
while (true) {
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
flet<bool> l1(m_aux_context->get_fparams().m_array_fake_support, true);
flet<bool> l2(m_aux_context->get_fparams().m_preprocess, true);
lbool r = m_aux_context->check();
TRACE(model_checker, tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r != l_true)
@ -457,12 +451,6 @@ namespace smt {
TRACE(model_checker, tout << "MODEL_CHECKER INVOKED\n";
tout << "model:\n"; model_pp(tout, *m_curr_model););
for (quantifier* q : *m_qm)
if (m.is_lambda_def(q)) {
md->add_lambda_defs();
break;
}
md->compress();
@ -518,8 +506,7 @@ namespace smt {
for (quantifier * q : *m_qm) {
if (!(m_qm->mbqi_enabled(q) &&
m_context->is_relevant(q) &&
m_context->get_assignment(q) == l_true &&
(!m_context->get_fparams().m_ematching || !m.is_lambda_def(q)))) {
m_context->get_assignment(q) == l_true)) {
if (!m_qm->mbqi_enabled(q))
++num_failures;
continue;
@ -588,30 +575,14 @@ namespace smt {
bindings.push_back(m_context->get_enode(b));
}
if (inst.m_def) {
unsigned n = 1;
expr* const* args = &inst.m_def;
if (m.is_and(inst.m_def)) {
n = to_app(inst.m_def)->get_num_args();
args = to_app(inst.m_def)->get_args();
}
for (unsigned i = 0; i < n; ++i) {
proof* pr = nullptr;
expr* arg = args[i];
if (m.proofs_enabled())
pr = m.mk_def_intro(arg);
m_context->internalize_assertion(arg, pr, gen);
}
}
TRACE(model_checker_bug_detail, tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
tout << "inconsistent: " << m_context->inconsistent() << "\n";
tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.data() + offset) << "\n";
tout << "def " << mk_pp(inst.m_def, m) << "\n";);
m_context->add_instance(q, nullptr, num_decls, bindings.data(), inst.m_def, gen, gen, gen, dummy);
);
m_context->add_instance(q, nullptr, num_decls, bindings.data(), gen, gen, gen, dummy);
TRACE(model_checker_bug_detail, tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";);
}
}
}
};
}

8
src/smt/smt_model_checker.h
View file

@ -23,7 +23,6 @@ Revision History:
#include "util/obj_hashtable.h"
#include "ast/ast.h"
#include "ast/array_decl_plugin.h"
#include "ast/normal_forms/defined_names.h"
#include "params/qi_params.h"
#include "params/smt_params.h"
@ -70,9 +69,8 @@ namespace smt {
struct instance {
quantifier * m_q;
unsigned m_generation;
expr * m_def;
unsigned m_bindings_offset;
instance(quantifier * q, unsigned offset, expr* def, unsigned gen):m_q(q), m_generation(gen), m_def(def), m_bindings_offset(offset) {}
instance(quantifier * q, unsigned offset, unsigned gen):m_q(q), m_generation(gen), m_bindings_offset(offset) {}
};
svector<instance> m_new_instances;
@ -86,7 +84,7 @@ namespace smt {
struct is_model_value {};
expr_mark m_visited;
bool contains_model_value(expr * e);
void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation, expr * def);
void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation);
bool is_safe_for_mbqi(quantifier * q) const;
public:
@ -106,5 +104,5 @@ namespace smt {
void operator()(expr* e);
};
};
}

216
src/smt/smt_model_finder.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include "util/backtrackable_set.h"
#include "ast/ast_util.h"
#include "ast/has_free_vars.h"
#include "ast/macros/macro_util.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
@ -31,14 +32,17 @@ Revision History:
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "ast/ast_smt2_pp.h"
#include "ast/rewriter/term_enumeration.h"
#include "model/model_pp.h"
#include "model/model_macro_solver.h"
#include "smt/smt_model_finder.h"
#include "smt/smt_context.h"
#include "tactic/tactic_exception.h"
#include "util/statistics.h"
namespace smt {
namespace mf {
// -----------------------------------
@ -107,9 +111,15 @@ namespace smt {
}
}
expr* get_inv(expr* v) const {
expr* get_inv(expr* v, model& mdl) const {
expr* t = nullptr;
m_inv.find(v, t);
if (!t) {
for (auto [k, term] : m_inv) {
if (mdl.are_equal(k, v))
return term;
}
}
return t;
}
@ -120,14 +130,11 @@ namespace smt {
}
void mk_inverse(evaluator& ev) {
for (auto const& kv : m_elems) {
expr* t = kv.m_key;
for (auto const &[t, gen] : m_elems) {
SASSERT(!contains_model_value(t));
unsigned gen = kv.m_value;
expr* t_val = ev.eval(t, true);
if (!t_val) break;
TRACE(model_finder, tout << mk_pp(t, m) << " " << mk_pp(t_val, m) << "\n";);
expr* old_t = nullptr;
if (m_inv.find(t_val, old_t)) {
unsigned old_t_gen = 0;
@ -187,14 +194,14 @@ namespace smt {
\brief Base class used to solve model construction constraints.
*/
class node {
unsigned m_id;
node* m_find{ nullptr };
unsigned m_eqc_size{ 1 };
unsigned m_id = 0;
node* m_find = nullptr;
unsigned m_eqc_size = 1;
sort* m_sort; // sort of the elements in the instantiation set.
sort* m_sort = nullptr; // sort of the elements in the instantiation set.
bool m_mono_proj{ false }; // relevant for integers & reals & bit-vectors
bool m_signed_proj{ false }; // relevant for bit-vectors.
bool m_mono_proj = false; // relevant for integers & reals & bit-vectors
bool m_signed_proj = false; // relevant for bit-vectors.
ptr_vector<node> m_avoid_set;
ptr_vector<expr> m_exceptions;
@ -291,8 +298,8 @@ namespace smt {
}
void insert(expr* n, unsigned generation) {
SASSERT(is_ground(n));
get_root()->m_set->insert(n, generation);
if (is_ground(n) || (has_quantifiers(n) && !has_free_vars(n))) // this is a closed term
get_root()->m_set->insert(n, generation);
}
void display(std::ostream& out, ast_manager& m) const {
@ -599,7 +606,10 @@ namespace smt {
}
else {
r = tmp;
TRACE(model_finder, tout << "eval\n" << mk_pp(n, m) << "\n----->\n" << mk_pp(r, m) << "\n";);
TRACE(model_finder, tout << "eval-failed\n" << mk_pp(n, m) << "\n----->\n" << mk_pp(r, m) << "\n";);
if (is_lambda(tmp)) {
r = m.mk_fresh_const("lambda", tmp->get_sort());
}
}
m_eval_cache[model_completion].insert(n, r);
m_eval_cache_range.push_back(r);
@ -1159,6 +1169,7 @@ namespace smt {
virtual char const* get_kind() const = 0;
virtual bool is_equal(qinfo const* qi) const = 0;
virtual void display(std::ostream& out) const { out << "[" << get_kind() << "]"; }
virtual void collect_statistics(::statistics &st) const {}
// AUF fragment solver
virtual void process_auf(quantifier* q, auf_solver& s, context* ctx) = 0;
@ -1227,7 +1238,7 @@ namespace smt {
// a necessary instantiation.
enode* e_arg = n->get_arg(m_arg_i);
expr* arg = e_arg->get_expr();
A_f_i->insert(arg, e_arg->get_generation());
A_f_i->insert(arg, ctx->get_generation(e_arg));
}
}
}
@ -1235,8 +1246,8 @@ namespace smt {
void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector<instantiation_set>& uvar_inst_sets, context* ctx) override {
if (m_f != mhead)
return;
uvar_inst_sets.reserve(m_var_j + 1, 0);
if (uvar_inst_sets[m_var_j] == 0)
uvar_inst_sets.reserve(m_var_j + 1, nullptr);
if (uvar_inst_sets[m_var_j] == nullptr)
uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager());
instantiation_set* s = uvar_inst_sets[m_var_j];
SASSERT(s != nullptr);
@ -1245,7 +1256,7 @@ namespace smt {
if (ctx->is_relevant(n)) {
enode* e_arg = n->get_arg(m_arg_i);
expr* arg = e_arg->get_expr();
s->insert(arg, e_arg->get_generation());
s->insert(arg, ctx->get_generation(e_arg));
}
}
}
@ -1301,7 +1312,7 @@ namespace smt {
bv_rw.mk_sub(arg, m_offset, arg_minus_k);
else
arith_rw.mk_sub(arg, m_offset, arg_minus_k);
S_j->insert(arg_minus_k, e_arg->get_generation());
S_j->insert(arg_minus_k, ctx->get_generation(e_arg));
}
}
}
@ -1369,6 +1380,94 @@ namespace smt {
};
class ho_var : public qinfo {
unsigned m_var_i;
unsigned m_ho_var_term_enum = 0;
public:
ho_var(ast_manager& m, unsigned i) : qinfo(m), m_var_i(i) {
}
void collect_statistics(::statistics &st) const override {
st.update("mbqi.ho-var-term-enum", m_ho_var_term_enum);
}
char const *get_kind() const override {
return "ho_var";
}
bool is_equal(qinfo const *qi) const override {
if (qi->get_kind() != get_kind())
return false;
ho_var const *other = static_cast<ho_var const *>(qi);
return m_var_i == other->m_var_i;
}
void display(std::ostream &out) const override {
out << "(" << "ho-var: " << m_var_i << ")";
}
void process_auf(quantifier *q, auf_solver &s, context *ctx) override {
/* node * S_i = */ s.get_uvar(q, m_var_i);
}
void populate_inst_sets(quantifier *q, auf_solver &s, context *ctx) override {
bool use_term_enum = ctx->get_fparams().m_term_enumeration;
if (!use_term_enum)
return;
node *S = s.get_uvar(q, m_var_i);
sort *srt = S->get_sort();
IF_VERBOSE(3, verbose_stream() << "ho_var::populate_inst_sets: " << q->get_id() << " " << mk_pp(srt, m) << "\n";);
term_enumeration tn(m);
// Add ground terms of type S.
// Add productions for functions in E-graph
// add other possible relevant functions such as equality over srt, Boolean operators
ast_mark visited;
tn.add_production(m.mk_true());
tn.add_production(m.mk_false());
for (enode *n : ctx->enodes()) {
if (!ctx->is_relevant(n))
continue;
auto e = n->get_expr();
if (srt == n->get_sort()) {
TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n");
S->insert(e, ctx->get_generation(n));
}
else if (!use_term_enum)
continue;
else if (is_app(e) && to_app(e)->get_decl()->is_skolem())
;
else if (is_uninterp_const(e)) {
TRACE(model_finder, tout << "add production " << mk_pp(e, m) << "\n");
tn.add_production(e);
}
else if (is_uninterp(e)) {
auto f = to_app(e)->get_decl();
if (visited.is_marked(f))
continue;
visited.mark(f, true);
TRACE(model_finder, tout << "add function " << mk_pp(f, m) << "\n");
tn.add_production(f);
}
}
unsigned max_count = 20;
for (auto t : tn.enum_terms(srt)) {
if (max_count == 0)
break;
--max_count;
unsigned generation = 0; // todo - inherited from sub-term of t?
TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m)
<< " to instantiation set of S" << std::endl;);
++m_ho_var_term_enum;
S->insert(t, generation);
}
}
};
/**
\brief auf_arr is a term (pattern) of the form:
@ -1378,7 +1477,7 @@ namespace smt {
Store in arrays, all enodes that match the pattern
*/
void get_auf_arrays(app* auf_arr, context* ctx, ptr_buffer<enode>& arrays) {
void get_auf_arrays(expr* auf_arr, context* ctx, ptr_buffer<enode>& arrays) {
if (is_ground(auf_arr)) {
if (ctx->e_internalized(auf_arr)) {
enode* e = ctx->get_enode(auf_arr);
@ -1387,8 +1486,8 @@ namespace smt {
}
}
}
else {
app* nested_array = to_app(auf_arr->get_arg(0));
else if (is_app(auf_arr)) {
app* nested_array = to_app(to_app(auf_arr)->get_arg(0));
ptr_buffer<enode> nested_arrays;
get_auf_arrays(nested_array, ctx, nested_arrays);
for (enode* curr : nested_arrays) {
@ -1396,7 +1495,7 @@ namespace smt {
enode_vector::iterator end2 = curr->end_parents();
for (; it2 != end2; ++it2) {
enode* p = *it2;
if (ctx->is_relevant(p) && p->get_expr()->get_decl() == auf_arr->get_decl()) {
if (ctx->is_relevant(p) && p->get_decl() == to_app(auf_arr)->get_decl()) {
arrays.push_back(p);
}
}
@ -1411,9 +1510,9 @@ namespace smt {
unsigned m_arg_i;
unsigned m_var_j;
app* get_array() const { return to_app(m_select->get_arg(0)); }
expr* get_array() const { return m_select->get_arg(0); }
func_decl* get_array_func_decl(app* ground_array, auf_solver& s) {
func_decl* get_array_func_decl(expr* ground_array, auf_solver& s) {
TRACE(model_evaluator, tout << expr_ref(ground_array, m) << "\n";);
expr* ground_array_interp = s.eval(ground_array, false);
if (ground_array_interp && m_array.is_as_array(ground_array_interp))
@ -1449,7 +1548,7 @@ namespace smt {
});
node* n1 = s.get_uvar(q, m_var_j);
for (enode* n : arrays) {
app* ground_array = n->get_expr();
auto ground_array = n->get_expr();
func_decl* f = get_array_func_decl(ground_array, s);
if (f) {
SASSERT(m_arg_i >= 1);
@ -1463,7 +1562,7 @@ namespace smt {
ptr_buffer<enode> arrays;
get_auf_arrays(get_array(), ctx, arrays);
for (enode* curr : arrays) {
app* ground_array = curr->get_expr();
auto ground_array = curr->get_expr();
func_decl* f = get_array_func_decl(ground_array, s);
if (f) {
node* A_f_i = s.get_A_f_i(f, m_arg_i - 1);
@ -1471,10 +1570,10 @@ namespace smt {
enode_vector::iterator end2 = curr->end_parents();
for (; it2 != end2; ++it2) {
enode* p = *it2;
if (ctx->is_relevant(p) && p->get_expr()->get_decl() == m_select->get_decl()) {
SASSERT(m_arg_i < p->get_expr()->get_num_args());
if (ctx->is_relevant(p) && p->get_decl() == m_select->get_decl()) {
SASSERT(m_arg_i < p->get_num_args());
enode* e_arg = p->get_arg(m_arg_i);
A_f_i->insert(e_arg->get_expr(), e_arg->get_generation());
A_f_i->insert(e_arg->get_expr(), ctx->get_generation(e_arg));
}
}
}
@ -1603,7 +1702,7 @@ namespace smt {
node* S_q_i = slv.get_uvar(q, m_var_i);
for (enode* n : ctx->enodes()) {
if (ctx->is_relevant(n) && n->get_expr()->get_sort() == s) {
S_q_i->insert(n->get_expr(), n->get_generation());
S_q_i->insert(n->get_expr(), ctx->get_generation(n));
}
}
}
@ -1689,8 +1788,13 @@ namespace smt {
public:
typedef ptr_vector<cond_macro>::const_iterator macro_iterator;
void collect_statistics(::statistics &st) const {
for (auto *qi : m_qinfo_vect)
qi->collect_statistics(st);
}
static quantifier_ref mk_flat(ast_manager& m, quantifier* q) {
if (has_quantifiers(q->get_expr()) && !m.is_lambda_def(q)) {
if (has_quantifiers(q->get_expr())) {
proof_ref pr(m);
expr_ref new_q(m);
pull_quant pull(m);
@ -2105,7 +2209,10 @@ namespace smt {
process_app(to_app(curr));
}
else if (is_var(curr)) {
m_info->m_is_auf = false; // unexpected occurrence of variable.
if (m_array_util.is_array(curr)) {
insert_qinfo(alloc(ho_var, m, to_var(curr)->get_idx()));
}
m_info->m_is_auf = false;
}
else {
SASSERT(is_lambda(curr));
@ -2163,7 +2270,6 @@ namespace smt {
}
SASSERT(is_quantifier(atom));
UNREACHABLE();
}
void process_literal(expr* atom, polarity pol) {
@ -2203,9 +2309,15 @@ namespace smt {
if (is_app(curr)) {
if (to_app(curr)->get_family_id() == m.get_basic_family_id() && m.is_bool(curr)) {
switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
case OP_IMPLIES:
case OP_IMPLIES:
process_literal(to_app(curr)->get_arg(0), neg(pol));
process_literal(to_app(curr)->get_arg(1), pol);
break;
case OP_XOR:
UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs
for (expr *arg : *to_app(curr)) {
visit_formula(arg, pol);
visit_formula(arg, neg(pol));
}
break;
case OP_OR:
case OP_AND:
@ -2279,7 +2391,6 @@ namespace smt {
void operator()(quantifier_info* d) {
m_info = d;
quantifier* q = d->get_flat_q();
if (m.is_lambda_def(q)) return;
expr* e = q->get_expr();
reset_cache();
if (!m.inc()) return;
@ -2324,6 +2435,13 @@ namespace smt {
reset();
}
void model_finder::collect_statistics(::statistics & st) const {
// Retrieve the ho-var term-enumeration counters from the embedded
// qinfo objects (mf::ho_var) held by each registered quantifier_info.
for (auto const &[k, v] : m_q2info)
v->collect_statistics(st);
}
void model_finder::checkpoint() {
checkpoint("model_finder");
}
@ -2516,11 +2634,12 @@ namespace smt {
Store in generation the generation of the result
*/
expr* model_finder::get_inv(quantifier* q, unsigned i, expr* val, unsigned& generation) {
expr* model_finder::get_inv(quantifier* q, unsigned i, expr* val, model& mdl,unsigned& generation) {
instantiation_set const* s = get_uvar_inst_set(q, i);
if (s == nullptr)
return nullptr;
expr* t = s->get_inv(val);
expr* t = s->get_inv(val, mdl);
if (m_auf_solver->is_default_representative(t))
return val;
if (t != nullptr) {
@ -2556,16 +2675,27 @@ namespace smt {
obj_map<expr, expr*> const& inv = s->get_inv_map();
if (inv.empty())
continue; // nothing to do
ptr_buffer<expr> eqs;
for (auto const& [val, _] : inv) {
if (val->get_sort() == sk->get_sort())
eqs.push_back(m.mk_eq(sk, val));
expr_ref_vector eqs(m), defs(m);
for (auto const& [val, term] : inv) {
if (val->get_sort() == sk->get_sort()) {
if (is_lambda(term)) {
eqs.push_back(m.mk_eq(sk, val));
defs.push_back(m.mk_eq(val, term));
}
else
eqs.push_back(m.mk_eq(sk, val));
}
}
if (!eqs.empty()) {
expr_ref new_cnstr(m);
new_cnstr = m.mk_or(eqs);
TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";);
aux_ctx->assert_expr(new_cnstr);
for (auto def : defs) {
TRACE(model_finder, tout << "assert_def:\n" << mk_pp(def, m) << "\n";);
aux_ctx->assert_expr(def);
}
asserted_something = true;
}
}

11
src/smt/smt_model_finder.h
View file

@ -52,6 +52,7 @@ Revision History:
#include "tactic/tactic_exception.h"
class model_instantiation_set;
class statistics;
namespace smt {
class context;
@ -64,7 +65,7 @@ namespace smt {
class hint_solver;
class non_auf_macro_solver;
class instantiation_set;
};
}
class model_finder : public quantifier2macro_infos {
typedef mf::quantifier_analyzer quantifier_analyzer;
@ -113,7 +114,7 @@ namespace smt {
void fix_model(proto_model * m);
quantifier * get_flat_quantifier(quantifier * q);
expr * get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation);
expr * get_inv(quantifier * q, unsigned i, expr * val, model& m, unsigned & generation);
bool restrict_sks_to_inst_set(context * aux_ctx, quantifier * q, expr_ref_vector const & sks);
void restart_eh();
@ -122,6 +123,8 @@ namespace smt {
quantifier_macro_info* operator()(quantifier* q) override;
};
};
void collect_statistics(::statistics & st) const;
};
}

8
src/smt/smt_model_generator.cpp
View file

@ -105,7 +105,7 @@ namespace smt {
proc = alloc(expr_wrapper_proc, m.mk_false());
}
else if (m.is_model_value(r->get_expr()))
proc = alloc(expr_wrapper_proc, r->get_expr());
proc = alloc(expr_wrapper_proc, r->get_app());
else {
family_id fid = s->get_family_id();
theory * th = m_context->get_theory(fid);
@ -384,7 +384,7 @@ namespace smt {
// send model
for (enode * n : m_context->enodes()) {
if (is_uninterp_const(n->get_expr()) && m_context->is_relevant(n)) {
func_decl * d = n->get_expr()->get_decl();
func_decl * d = n->get_decl();
TRACE(mg_top_sort, tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";);
if (m_hidden_ufs.contains(d)) continue;
expr * val = get_value(n);
@ -428,6 +428,8 @@ namespace smt {
if (!m_context->is_relevant(t))
continue;
enode * n = m_context->get_enode(t);
if (!n->is_app())
continue;
unsigned num_args = n->get_num_args();
func_decl * f = n->get_decl();
if (num_args == 0 && include_func_interp(f)) {
@ -531,4 +533,4 @@ namespace smt {
return m_model.get();
}
};
}

2
src/smt/smt_model_generator.h
View file

@ -240,7 +240,7 @@ namespace smt {
}
}
};
};
}

1603
src/smt/smt_parallel.cpp
View file

File diff suppressed because it is too large Load diff

275
src/smt/smt_parallel.h
View file

@ -21,8 +21,10 @@ Revision History:
#include "smt/smt_context.h"
#include "util/search_tree.h"
#include "ast/sls/sls_smt_solver.h"
#include <atomic>
#include <thread>
#include <mutex>
#include <condition_variable>
namespace smt {
@ -30,25 +32,56 @@ namespace smt {
struct cube_config {
using literal = expr_ref;
static bool literal_is_null(expr_ref const& l) { return l == nullptr; }
static bool same_atom(expr_ref const& a, expr_ref const& b) {
expr* atom_a = a.get();
expr* atom_b = b.get();
a.get_manager().is_not(atom_a, atom_a);
b.get_manager().is_not(atom_b, atom_b);
return atom_a == atom_b;
}
static std::ostream& display_literal(std::ostream& out, expr_ref const& l) { return out << mk_bounded_pp(l, l.get_manager()); }
};
class parallel {
context& ctx;
unsigned num_threads;
bool m_should_run_sls = false;
class core_minimizer_worker;
using node = search_tree::node<cube_config>;
struct shared_clause {
unsigned source_worker_id;
expr_ref clause;
};
struct bb_candidate {
expr_ref lit;
double age;
unsigned hits; // how many cubes reported it
bb_candidate(ast_manager& m, expr* e, double s, unsigned h) : lit(e, m), age(s), hits(h) {}
};
using bb_candidates = vector<bb_candidate>;
struct node_lease {
node* leased_node = nullptr;
// Cancellation generation counter for this node/subtree.
// Incremented when the node is closed; used to signal that all
// workers holding leases on this node (or its descendants)
// must abandon work immediately.
unsigned cancel_epoch = 0;
// Guards against multiple inc_cancel() calls for the same lease.
// Set when cancel_lease() is signaled; cleared when a new lease is assigned.
bool cancel_signaled = false;
};
class batch_manager {
enum state {
is_running,
is_sat,
is_unsat,
is_unknown,
is_exception_msg,
is_exception_code
};
@ -56,22 +89,51 @@ namespace smt {
struct stats {
unsigned m_max_cube_depth = 0;
unsigned m_num_cubes = 0;
unsigned m_backbones_found = 0;
unsigned m_core_min_jobs_enqueued = 0;
unsigned m_core_min_jobs_published = 0;
unsigned m_core_min_jobs_skipped = 0;
unsigned m_core_min_global_unsat = 0;
};
struct core_min_job {
node* source = nullptr;
expr_ref_vector core;
core_min_job(ast_manager& m, node* source) : source(source), core(m) {}
};
ast_manager& m;
parallel& p;
std::mutex mux;
state m_state = state::is_running;
stats m_stats;
using node = search_tree::node<cube_config>;
search_tree::tree<cube_config> m_search_tree;
vector<node_lease> m_worker_leases;
unsigned m_exception_code = 0;
std::string m_exception_msg;
std::string m_reason_unknown;
vector<shared_clause> shared_clause_trail; // store all shared clauses with worker IDs
obj_hashtable<expr> shared_clause_set; // for duplicate filtering on per-thread clause expressions
bb_candidates m_bb_candidates;
unsigned m_max_global_bb_candidates = 100;
unsigned m_bb_batch_size = 150;
obj_hashtable<expr> m_global_backbones;
std::atomic<unsigned> m_bb_candidate_epoch = 0;
// Backbone job queue
std::condition_variable m_bb_cv;
bb_candidates m_bb_current_batch;
unsigned m_bb_batch_id = 0;
unsigned m_num_global_bb_threads = 0;
unsigned_vector m_bb_last_batch_processed;
unsigned m_bb_cancel_epoch = 0; // When a backbone worker finishes early, it increments m_bb_cancel_epoch and notifies all
// Core minimization job queue
std::condition_variable m_core_min_cv;
scoped_ptr_vector<core_min_job> m_core_min_jobs;
bool m_ablate_backtracking = false;
// called from batch manager to cancel other workers if we've reached a verdict
void cancel_workers() {
IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
@ -86,32 +148,118 @@ namespace smt {
p.m_sls_worker->cancel();
}
void cancel_background_threads() {
cancel_workers();
cancel_sls_worker();
void cancel_backbones_worker() {
IF_VERBOSE(1, verbose_stream() << "Canceling backbones workers\n");
for (auto* w : p.m_global_backbones_workers)
w->cancel();
}
void init_parameters_state();
std::atomic<bool> m_canceled = false;
void cancel_background_threads() {
if (m_canceled.exchange(true))
return; // already canceled
cancel_workers();
cancel_sls_worker();
if (!p.m_global_backbones_workers.empty()) {
cancel_backbones_worker();
m_bb_cv.notify_all();
}
if (p.m_core_minimizer_worker) {
p.m_core_minimizer_worker->cancel();
m_core_min_cv.notify_all();
}
}
// to avoid deadlock
bool is_global_backbone_unlocked(ast_translation& l2g, expr* bb_cand) {
expr_ref cand(l2g(bb_cand), l2g.to());
return m_global_backbones.contains(cand.get());
}
bool is_global_backbone_or_negation_unlocked(ast_translation& l2g, expr* bb_cand) {
expr_ref cand(l2g(bb_cand), l2g.to());
expr_ref neg_cand(mk_not(l2g.to(), cand), l2g.to());
return m_global_backbones.contains(cand.get()) || m_global_backbones.contains(neg_cand.get());
}
void backtrack_unlocked(ast_translation& l2g, unsigned worker_id, expr_ref_vector const& core,
node_lease* lease = nullptr, vector<node_lease> const* targets = nullptr);
void collect_clause_unlocked(ast_translation &l2g, unsigned source_worker_id, expr *clause);
void set_canceled_unlocked();
void release_worker_lease_unlocked(unsigned worker_id, node_lease& lease);
bool attempt_release_canceled_lease_unlocked(unsigned worker_id, node_lease& lease);
void cancel_closed_leases_unlocked(unsigned source_worker_id);
void collect_matching_targets_unlocked(node* source, expr* lit, vector<cube_config::literal> const& core,
vector<node_lease>& targets);
node* find_core_source_unlocked(ast_translation& l2g, node* source, expr_ref_vector const& core);
unsigned select_best_core_min_job_unlocked() const;
public:
batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { }
void initialize();
void initialize(unsigned num_global_bb_threads, unsigned initial_max_thread_conflicts = 1000); // TODO: pass in from worker config
void set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core);
void set_sat(ast_translation& l2g, model& m);
void set_unknown(std::string const& reason);
void set_canceled();
void set_exception(std::string const& msg);
void set_exception(unsigned error_code);
void collect_statistics(::statistics& st) const;
bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n);
void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n);
void split(ast_translation& l2g, unsigned id, node* n, expr* atom);
void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates);
void collect_backbone_evidence(ast_translation& l2g, expr* lit, double delta);
bool collect_global_backbone(ast_translation& l2g, expr_ref const& backbone, unsigned source_worker_id = UINT_MAX);
bool wait_for_backbone_job(unsigned bb_thread_id, ast_translation& g2l, vector<parallel::bb_candidate>& out, reslimit& lim);
bool has_new_backbone_candidates(unsigned epoch) {
return m_bb_candidate_epoch.load(std::memory_order_acquire) != epoch;
}
unsigned get_bb_candidate_epoch() const {
return m_bb_candidate_epoch.load(std::memory_order_acquire);
}
expr_ref_vector get_global_backbones_snapshot(ast_translation& g2l) {
std::scoped_lock lock(mux);
expr_ref_vector snapshot(g2l.to());
for (expr* gb : m_global_backbones)
snapshot.push_back(g2l(gb));
return snapshot;
}
bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, bool is_first_run, node_lease& lease);
void backtrack(ast_translation& l2g, unsigned worker_id, expr_ref_vector const& core, node_lease& lease);
void enqueue_core_minimization(ast_translation& l2g, node* source, expr_ref_vector const& core);
bool wait_for_core_min_job(ast_translation& g2l, node*& source,
expr_ref_vector& core, reslimit& lim);
void publish_minimized_core(ast_translation& l2g, expr_ref_vector const& asms, node* source,
unsigned original_core_size, expr_ref_vector const& minimized_core);
void try_split(ast_translation& l2g, unsigned worker_id, node_lease& lease, expr* atom, unsigned effort);
bool checkpoint_worker(unsigned worker_id, node_lease& lease, bool& lease_canceled);
bool lease_canceled(node_lease const& lease);
void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause);
expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
lbool get_result() const;
std::string const& get_reason_unknown() const { return m_reason_unknown; }
bool is_global_backbone_or_negation(ast_translation& l2g, expr* bb_cand) {
std::scoped_lock lock(mux);
return is_global_backbone_or_negation_unlocked(l2g, bb_cand);
}
void cancel_current_backbone_batch() {
std::scoped_lock lock(mux);
m_bb_cancel_epoch++;
m_bb_cv.notify_all();
}
unsigned get_cancel_epoch() {
std::scoped_lock lock(mux);
return m_bb_cancel_epoch;
}
lbool check(expr_ref_vector const &asms, context &ctx);
};
class worker {
@ -123,14 +271,16 @@ namespace smt {
bool m_share_units_initial_only = true;
double m_max_conflict_mul = 1.5;
bool m_inprocessing = false;
bool m_global_backbones = false;
bool m_local_backbones = false;
bool m_sls = false;
unsigned m_inprocessing_delay = 1;
unsigned m_max_cube_depth = 20;
unsigned m_max_conflicts = UINT_MAX;
bool m_core_minimize = false;
bool m_ablate_backtracking = false;
};
using node = search_tree::node<cube_config>;
unsigned id; // unique identifier for the worker
parallel& p;
batch_manager& b;
@ -141,8 +291,9 @@ namespace smt {
random_gen m_rand;
scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
uint_set m_known_units;
unsigned m_num_shared_units = 0;
unsigned m_shared_units_prefix = 0;
unsigned m_num_initial_atoms = 0;
unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
@ -152,10 +303,14 @@ namespace smt {
void share_units();
void update_max_thread_conflicts() {
m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
} // allow for backoff scheme of conflicts within the thread for cube timeouts.
// allow for backoff scheme of conflicts within the thread for cube timeouts.
// Use saturating arithmetic to avoid unsigned overflow / undefined behaviour.
double next = m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts;
m_config.m_threads_max_conflicts = (next >= (double)UINT_MAX) ? UINT_MAX : (unsigned)next;
}
void simplify();
bb_candidates find_backbone_candidates(unsigned k = 10);
public:
worker(unsigned id, parallel& p, expr_ref_vector const& _asms);
@ -164,6 +319,7 @@ namespace smt {
void collect_shared_clauses();
void cancel();
void cancel_lease();
void collect_statistics(::statistics& st) const;
reslimit& limit() {
@ -191,16 +347,93 @@ namespace smt {
}
};
class core_minimizer_worker {
batch_manager &b;
ast_manager m;
expr_ref_vector asms;
smt_params m_smt_params;
scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
unsigned m_num_core_minimize_calls = 0;
unsigned m_num_core_minimize_undef = 0;
unsigned m_num_core_minimize_refined = 0;
unsigned m_num_core_minimize_lits_removed = 0;
unsigned m_num_core_minimize_found_sat = 0;
unsigned m_core_minimize_conflict_budget = 5000;
unsigned m_shared_clause_limit = 0;
void minimize_unsat_core(expr_ref_vector& core);
void collect_shared_clauses();
public:
core_minimizer_worker(parallel& p, expr_ref_vector const& _asms);
void run();
void cancel();
void collect_statistics(::statistics& st) const;
reslimit& limit() { return m.limit(); }
};
class backbones_worker {
struct stats {
unsigned m_batches_total = 0;
unsigned m_candidates_total = 0;
unsigned m_singleton_backbones = 0;
unsigned m_backbones_detected = 0;
unsigned m_internal_backbones_found = 0;
unsigned m_retry_backbones_found = 0;
unsigned m_bb_retries = 0;
unsigned m_fallback_singleton_checks = 0;
unsigned m_fallback_reason_chunk_exhausted = 0;
unsigned m_fallback_reason_undef = 0;
unsigned m_core_refinement_rounds = 0;
unsigned m_lits_removed_by_core = 0;
unsigned m_num_chunk_increases = 0;
};
enum bb_mode {
bb_negated,
bb_positive
};
unsigned id; // unique identifier for the worker
batch_manager& b;
ast_manager m;
expr_ref_vector asms;
smt_params m_smt_params;
scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
unsigned m_bb_chunk_size = 20;
unsigned m_bb_conflicts_per_chunk = 1000;
uint_set m_known_units;
bool m_use_failed_literal_test;
stats m_stats;
bb_mode m_mode;
unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
unsigned m_shared_units_prefix = 0;
unsigned m_num_initial_atoms = 0;
bool try_get_unit_backbone(expr* candidate, expr_ref& backbone);
void run_batch_mode();
void run_failed_literal_mode();
lbool probe_literal(bool_var v, expr *e, bool is_retry);
public:
backbones_worker(unsigned id, parallel &p, expr_ref_vector const &_asms);
void cancel();
void collect_statistics(::statistics& st) const;
void run();
void collect_shared_clauses();
reslimit &limit() { return m.limit(); }
};
batch_manager m_batch_manager;
scoped_ptr_vector<worker> m_workers;
scoped_ptr<sls_worker> m_sls_worker;
scoped_ptr<core_minimizer_worker> m_core_minimizer_worker;
scoped_ptr_vector<backbones_worker> m_global_backbones_workers;
public:
parallel(context& ctx) :
ctx(ctx),
num_threads(std::min(
(unsigned)std::thread::hardware_concurrency(),
ctx.get_fparams().m_threads)),
m_batch_manager(ctx.m, *this) {}
lbool operator()(expr_ref_vector const& asms);

183
src/smt/smt_quantifier.cpp
View file

@ -19,6 +19,10 @@ Revision History:
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/quantifier_stat.h"
#include "ast/euf/ho_matcher.h"
#include "ast/rewriter/var_subst.h"
#include "ast/well_sorted.h"
#include "ast/has_free_vars.h"
#include "smt/smt_quantifier.h"
#include "smt/smt_context.h"
#include "smt/smt_model_finder.h"
@ -26,6 +30,7 @@ Revision History:
#include "smt/smt_quick_checker.h"
#include "smt/mam.h"
#include "smt/qi_queue.h"
#include "util/statistics.h"
#include "util/obj_hashtable.h"
namespace smt {
@ -154,7 +159,8 @@ namespace smt {
}
unsigned get_generation(quantifier * q) const {
return get_stat(q)->get_generation();
auto* s = m_quantifier_stat.find_core(q);
return s ? s->get_data().get_value()->get_generation() : 0;
}
void add(quantifier * q, unsigned generation) {
@ -215,9 +221,7 @@ namespace smt {
STRACE(triggers, tout <<", Pat: "<< expr_ref(pat, m()););
STRACE(causality, tout <<", Father:";);
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
for (auto [orig, substituted] : used_enodes) {
(void) substituted;
if (orig == nullptr) {
STRACE(causality, tout << " #" << substituted->get_owner_id(););
@ -247,24 +251,19 @@ namespace smt {
trace_stream() << "\n";
} else {
std::ostream & out = trace_stream();
obj_hashtable<enode> already_visited;
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
// is used. We need to make sure that all of these equalities appear in the log.
for (unsigned i = 0; i < num_bindings; ++i) {
log_justification_to_root(out, bindings[i], already_visited, m_context, m());
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
for (auto [orig, substituted] : used_enodes) {
if (orig != nullptr) {
log_justification_to_root(out, orig, already_visited, m_context, m());
log_justification_to_root(out, substituted, already_visited, m_context, m());
}
}
// At this point all relevant equalities for the match are logged.
out << "[new-match] " << f->get_data_hash() << " #" << q->get_id() << " #" << pat->get_id();
for (unsigned i = 0; i < num_bindings; ++i) {
@ -285,20 +284,28 @@ namespace smt {
out << "\n";
}
}
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
expr* def,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
vector<std::tuple<enode *, enode *>> & used_enodes) {
// Try higher-order refinement first
if (pat && m_plugin->refine_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes))
return true;
if (!m_quantifier_stat.contains(q)) {
IF_VERBOSE(2, verbose_stream() << "add_instance: quantifier not in stat map: " << mk_pp(q, m()) << "\n");
return false;
}
max_generation = std::max(max_generation, get_generation(q));
get_stat(q)->update_max_generation(max_generation);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
if (f) {
if (is_trace_enabled(TraceTag::causality)) {
log_causality(f,pat,used_enodes);
@ -472,17 +479,17 @@ namespace smt {
bool quantifier_manager::add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
expr* def,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
vector<std::tuple<enode *, enode *>> & used_enodes) {
return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes);
return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes);
}
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
vector<std::tuple<enode *, enode *>> tmp;
return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp);
return add_instance(q, nullptr, num_bindings, bindings,
generation, generation, generation, tmp);
}
void quantifier_manager::init_search_eh() {
@ -569,6 +576,7 @@ namespace smt {
void quantifier_manager::collect_statistics(::statistics & st) const {
m_imp->m_qi_queue.collect_statistics(st);
m_imp->m_plugin->collect_statistics(st);
}
void quantifier_manager::reset_statistics() {
@ -599,9 +607,26 @@ namespace smt {
scoped_ptr<mam> m_lazy_mam;
scoped_ptr<model_finder> m_model_finder;
scoped_ptr<model_checker> m_model_checker;
scoped_ptr<euf::ho_matcher> m_ho_matcher;
unsigned m_new_enode_qhead;
unsigned m_lazy_matching_idx;
bool m_active;
// State for higher-order match refinement callback
struct ho_match_state {
quantifier* m_q = nullptr;
app* m_pat = nullptr;
unsigned m_num_bindings = 0;
enode* const* m_bindings = nullptr;
unsigned m_max_generation = 0;
unsigned m_min_top_generation = 0;
unsigned m_max_top_generation = 0;
vector<std::tuple<enode*, enode*>>* m_used_enodes = nullptr;
vector<std::pair<quantifier*, expr_ref_vector>> m_matches;
};
ho_match_state m_ho_state;
unsigned m_stat_ho_refine = 0; // number of times ho-matching refinement is invoked
unsigned m_stat_ho_instances = 0; // number of instances added via ho-matching
public:
default_qm_plugin():
m_qm(nullptr),
@ -625,12 +650,111 @@ namespace smt {
m_model_finder->set_context(m_context);
m_model_checker->set_qm(qm);
if (m_fparams->m_ho_matching) {
m_ho_matcher = alloc(euf::ho_matcher, m, m_context->get_trail_stack());
m_ho_matcher->set_max_iterations(m_fparams->m_ho_matching_bound);
std::function<void(euf::ho_subst&)> on_match = [this](euf::ho_subst& s) {
on_ho_match(s);
};
m_ho_matcher->set_on_match(on_match);
}
}
quantifier_manager_plugin * mk_fresh() override { return alloc(default_qm_plugin); }
void on_ho_match(euf::ho_subst &s) {
auto &st = m_ho_state;
auto *hoq = st.m_q;
auto *q = m_ho_matcher->hoq2q(hoq);
auto const &binding = s.get_binding(q);
st.m_matches.push_back({ q, binding });
}
void consume_ho_matches() {
for (auto const &[q, binding] : m_ho_state.m_matches)
consume_ho_match(q, binding);
m_ho_state.m_matches.reset();
}
void consume_ho_match(quantifier * q, expr_ref_vector const& binding) {
auto &st = m_ho_state;
// Create enodes for the refined bindings and add instance
ptr_buffer<enode> new_bindings;
unsigned max_gen = st.m_max_generation;
TRACE(ho_matching, tout << binding << "\n");
for (expr* e : binding) {
if (!e)
return; // incomplete binding
if (has_free_vars(e))
return;
if (!m_context->e_internalized(e)) {
m_context->internalize(e, false);
}
enode* n = m_context->get_enode(e);
new_bindings.push_back(n);
unsigned gen = m_context->get_generation(n);
if (gen > max_gen)
max_gen = gen;
}
TRACE(ho_matching,
ast_manager &m = m_context->get_manager();
tout << "ho_match refined for " << mk_pp(q, m) << "\n";
for (unsigned i = 0; i < new_bindings.size(); ++i)
tout << " binding[" << i << "] = " << mk_bounded_pp(new_bindings[i]->get_expr(), m) << "\n";);
vector<std::tuple<enode*, enode*>> used_enodes;
m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(),
max_gen, st.m_min_top_generation, st.m_max_top_generation, used_enodes);
++m_stat_ho_instances;
}
bool try_ho_refine(quantifier* qa, app* pat, unsigned num_bindings, enode* const* bindings,
unsigned max_generation, unsigned min_top_gen, unsigned max_top_gen,
vector<std::tuple<enode*, enode*>>& used_enodes) {
if (!m_ho_matcher || !m_ho_matcher->is_ho_pattern(pat))
return false;
ast_manager& m = m_context->get_manager();
expr_ref_vector s(m);
// With var_subst(std_order=true): var idx maps to s[s.size()-idx-1]
// SMT MAM bindings: bindings[i] = var at index (num_bindings-1-i)
// So bindings[i] corresponds to s[i] with std_order
for (unsigned i = 0; i < num_bindings; ++i)
s.push_back(bindings[i]->get_expr());
m_ho_state.m_q = qa;
m_ho_state.m_pat = pat;
m_ho_state.m_num_bindings = num_bindings;
m_ho_state.m_bindings = bindings;
m_ho_state.m_max_generation = max_generation;
m_ho_state.m_min_top_generation = min_top_gen;
m_ho_state.m_max_top_generation = max_top_gen;
m_ho_state.m_used_enodes = &used_enodes;
m_ho_state.m_matches.reset();
IF_VERBOSE(10, verbose_stream() << "try_ho_refine: q=" << mk_pp(qa, m) << "\n pat=" << mk_pp(pat, m) << "\n";
for (unsigned i = 0; i < num_bindings; ++i)
verbose_stream() << " s[" << i << "] = " << mk_pp(s.get(i), m) << " sort=" << mk_pp(s.get(i)->get_sort(), m) << "\n";);
m_ho_matcher->refine_ho_match(pat, s);
consume_ho_matches();
++m_stat_ho_refine;
return true;
}
bool model_based() const override { return m_fparams->m_mbqi; }
void collect_statistics(::statistics & st) const override {
if (m_fparams->m_ho_matching) {
st.update("ho-matching refinements", m_stat_ho_refine);
st.update("ho-matching instances", m_stat_ho_instances);
}
if (m_model_finder)
m_model_finder->collect_statistics(st);
}
bool mbqi_enabled(quantifier *q) const override {
if (!m_fparams->m_mbqi_id) return true;
const symbol &s = q->get_qid();
@ -656,13 +780,13 @@ namespace smt {
void push() override {
m_mam->push_scope();
m_lazy_mam->push_scope();
m_model_finder->push_scope();
m_model_finder->push_scope();
}
void pop(unsigned num_scopes) override {
m_mam->pop_scope(num_scopes);
m_lazy_mam->pop_scope(num_scopes);
m_model_finder->pop_scope(num_scopes);
m_model_finder->pop_scope(num_scopes);
}
void init_search_eh() override {
@ -704,6 +828,14 @@ namespace smt {
TRACE(quantifier, tout << "adding:\n" << expr_ref(mp, m) << "\n";);
m_mam->add_pattern(q, mp);
}
// Compile HO pattern and also register the compiled version with MAM
if (m_ho_matcher) {
auto [q1, p1] = m_ho_matcher->compile_ho_pattern(q, mp);
if (p1 != mp) {
IF_VERBOSE(10, verbose_stream() << "ho_matching: q=" << q->get_qid() << " p1= " << mk_pp(p1, m) << "\n");
m_lazy_mam->add_pattern(q1, p1);
}
}
if (!unary)
j++;
}
@ -713,6 +845,13 @@ namespace smt {
return m_fparams->m_ematching && !m_qm->empty();
}
bool refine_instance(quantifier* q, app* pat, unsigned num_bindings, enode* const* bindings,
unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation,
vector<std::tuple<enode*, enode*>>& used_enodes) override {
return try_ho_refine(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes);
}
void add_eq_eh(enode * e1, enode * e2) override {
if (use_ematching())
m_mam->add_eq_eh(e1, e2);
@ -726,7 +865,9 @@ namespace smt {
}
bool can_propagate() const override {
return m_active && m_mam->has_work();
bool r = m_active && m_mam->has_work();
IF_VERBOSE(11, if (r) verbose_stream() << "ho_matching: can_propagate=true\n");
return r;
}
void restart_eh() override {
@ -814,4 +955,4 @@ namespace smt {
return alloc(default_qm_plugin);
}
};
}

15
src/smt/smt_quantifier.h
View file

@ -60,12 +60,11 @@ namespace smt {
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
expr* def,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
void init_search_eh();
void assign_eh(quantifier * q);
@ -178,8 +177,16 @@ namespace smt {
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
/**
\brief Try to refine a match using higher-order matching.
Returns true if the pattern was an HO pattern and refinement was attempted.
In that case, the plugin handles adding instances via the refined bindings.
*/
virtual bool refine_instance(quantifier* q, app* pat, unsigned num_bindings, enode* const* bindings,
unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation,
vector<std::tuple<enode*, enode*>>& used_enodes) { return false; }
virtual void collect_statistics(::statistics & st) const {}
};
};
}

6
src/smt/smt_quick_checker.cpp
View file

@ -235,8 +235,8 @@ namespace smt {
TRACE(quick_checker, tout << "found new candidate\n";);
TRACE(quick_checker_sizes, tout << "found new candidate\n";
for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";);
unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.data());
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), nullptr,
unsigned max_generation = m_context.get_max_generation(m_num_bindings, m_bindings.data());
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(),
max_generation,
0, // min_top_generation is only available for instances created by the MAM
0, // max_top_generation is only available for instances created by the MAM
@ -404,5 +404,5 @@ namespace smt {
return new_expr;
}
};
}

2
src/smt/smt_quick_checker.h
View file

@ -98,6 +98,6 @@ namespace smt {
bool instantiate_not_sat(quantifier * q);
bool instantiate_not_sat(quantifier * q, unsigned num_candidates, expr * const * candidates);
};
};
}

27
src/smt/smt_relevancy.cpp
View file

@ -141,6 +141,13 @@ namespace smt {
typedef list<relevancy_eh *> relevancy_ehs;
obj_map<expr, relevancy_ehs *> m_relevant_ehs;
obj_map<expr, relevancy_ehs *> m_watches[2];
// Over-approximating membership filter for m_watches: contains a superset
// of the expr ids that have (or ever had) a watch list for the given phase.
// It is monotonic (never cleared on erase/pop), so it can only yield false
// positives, never false negatives. This lets get_watches() skip the
// obj_map pointer-hash probe for the common unwatched-literal case at the
// assign_eh hotspot.
uint_set m_is_watched[2];
struct eh_trail {
enum class kind { POS_WATCH, NEG_WATCH, HANDLER };
kind m_kind;
@ -185,17 +192,23 @@ namespace smt {
}
relevancy_ehs * get_watches(expr * n, bool val) {
unsigned idx = val ? 1 : 0;
if (!m_is_watched[idx].contains(n->get_id()))
return nullptr;
relevancy_ehs * r = nullptr;
m_watches[val ? 1 : 0].find(n, r);
SASSERT(m_watches[val ? 1 : 0].contains(n) || r == 0);
m_watches[idx].find(n, r);
SASSERT(m_watches[idx].contains(n) || r == 0);
return r;
}
void set_watches(expr * n, bool val, relevancy_ehs * ehs) {
unsigned idx = val ? 1 : 0;
if (ehs == nullptr)
m_watches[val ? 1 : 0].erase(n);
else
m_watches[val ? 1 : 0].insert(n, ehs);
m_watches[idx].erase(n);
else {
m_watches[idx].insert(n, ehs);
m_is_watched[idx].insert(n->get_id());
}
}
void push_trail(eh_trail const & t) {
@ -254,7 +267,7 @@ namespace smt {
}
}
bool is_relevant_core(expr * n) const { return m_is_relevant.contains(n->get_id()); }
bool is_relevant_core(expr * n) const { SASSERT(n); return m_is_relevant.contains(n->get_id()); }
bool is_relevant(expr * n) const override {
return !enabled() || is_relevant_core(n);
@ -720,6 +733,6 @@ namespace smt {
}
relevancy_propagator * mk_relevancy_propagator(context & ctx) { return alloc(relevancy_propagator_imp, ctx); }
};
}

2
src/smt/smt_relevancy.h
View file

@ -196,6 +196,6 @@ namespace smt {
relevancy_propagator * mk_relevancy_propagator(context & ctx);
};
}

9
src/smt/smt_setup.cpp
View file

@ -40,6 +40,7 @@ Revision History:
#include "smt/theory_pb.h"
#include "smt/theory_fpa.h"
#include "smt/theory_polymorphism.h"
#include "smt/theory_finite_set.h"
namespace smt {
@ -784,6 +785,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_char, m_context));
}
void setup::setup_finite_set() {
m_context.register_plugin(alloc(smt::theory_finite_set, m_context));
}
void setup::setup_special_relations() {
m_context.register_plugin(alloc(smt::theory_special_relations, m_context, m_manager));
}
@ -807,6 +812,7 @@ namespace smt {
setup_dl();
setup_seq_str(st);
setup_fpa();
setup_finite_set();
setup_special_relations();
setup_polymorphism();
setup_relevancy(st);
@ -839,6 +845,7 @@ namespace smt {
setup_bv();
setup_dl();
setup_seq_str(st);
setup_finite_set();
setup_fpa();
setup_recfuns();
setup_special_relations();
@ -934,6 +941,6 @@ namespace smt {
setup_unknown();
}
};
}

3
src/smt/smt_setup.h
View file

@ -102,6 +102,7 @@ namespace smt {
void setup_seq_str(static_features const & st);
void setup_seq();
void setup_char();
void setup_finite_set();
void setup_card();
void setup_sls();
void setup_i_arith();
@ -123,6 +124,6 @@ namespace smt {
symbol const & get_logic() const { return m_logic; }
void operator()(config_mode cm);
};
};
}

144
src/smt/smt_solver.cpp
View file

@ -22,12 +22,15 @@ Notes:
#include "ast/for_each_expr.h"
#include "ast/ast_pp.h"
#include "ast/func_decl_dependencies.h"
#include "smt/smt_context.h"
#include "smt/smt_kernel.h"
#include "params/smt_params.h"
#include "params/smt_params_helper.hpp"
#include "solver/solver_na2as.h"
#include "solver/mus.h"
#include <algorithm>
namespace {
class smt_solver : public solver_na2as {
@ -61,6 +64,7 @@ namespace {
smt_params m_smt_params;
smt::kernel m_context;
cuber* m_cuber;
random_gen m_rand;
symbol m_logic;
bool m_minimizing_core;
bool m_core_extend_patterns;
@ -84,16 +88,19 @@ namespace {
updt_params(p);
}
solver * translate(ast_manager & m, params_ref const & p) override {
ast_translation translator(get_manager(), m);
solver * translate(ast_manager & target, params_ref const & p) override {
ast_translation translator(get_manager(), target);
params_ref init;
init.copy(get_params());
init.copy(p);
smt_solver * result = alloc(smt_solver, m, p, m_logic);
smt_solver* result = alloc(smt_solver, target, init, m_logic);
smt::kernel::copy(m_context, result->m_context, true);
if (mc0())
if (mc0())
result->set_model_converter(mc0()->translate(translator));
for (auto & [k, v] : m_name2assertion) {
for (auto& [k, v] : m_name2assertion) {
expr* val = translator(k);
expr* key = translator(v);
result->assert_expr(val, key);
@ -142,7 +149,7 @@ namespace {
insert_ctrl_c(r);
}
void collect_statistics(statistics & st) const override {
void collect_statistics_core(statistics & st) const override {
m_context.collect_statistics(st);
}
@ -212,6 +219,97 @@ namespace {
return m_context.get_trail(max_level);
}
expr_ref_vector get_assigned_literals() override {
expr_ref_vector result(m);
auto const& ctx = m_context.get_context();
for (auto lit : ctx.assigned_literals()) {
expr* atom = ctx.bool_var2expr(lit.var());
if (!atom)
continue;
result.push_back(lit.sign() ? m.mk_not(atom) : atom);
}
return result;
}
unsigned get_assign_level(expr* e) const override {
auto const& ctx = m_context.get_context();
get_manager().is_not(e, e);
if (!ctx.b_internalized(e))
return UINT_MAX;
return ctx.get_assign_level(ctx.get_bool_var(e));
}
bool is_relevant(expr* e) const override {
auto const& ctx = m_context.get_context();
get_manager().is_not(e, e);
return ctx.b_internalized(e) && ctx.is_relevant(e);
}
unsigned get_num_bool_vars() const override {
return m_context.get_context().get_num_bool_vars();
}
sat::bool_var get_bool_var(expr* e) const override {
auto const& ctx = m_context.get_context();
get_manager().is_not(e, e);
return ctx.b_internalized(e) ? ctx.get_bool_var(e) : sat::null_bool_var;
}
void pop_to_base_level() override {
m_context.pop_to_base_level();
}
void setup_for_parallel() override {
m_context.get_context().setup_for_parallel();
}
void set_preprocess(bool f) override {
m_context.set_preprocess(f);
}
void set_max_conflicts(unsigned max_conflicts) override {
auto& ctx = m_context.get_context();
ctx.get_fparams().m_max_conflicts = max_conflicts;
}
unsigned get_max_conflicts() const override {
return m_context.get_context().get_fparams().m_max_conflicts;
}
void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
ast_manager& m = get_manager();
auto& ctx = m_context.get_context();
unsigned curr_time = ctx.get_num_assignments();
vector<solver::scored_literal> all;
for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
if (ctx.get_assignment(v) != l_undef && ctx.get_assign_level(v) == ctx.get_base_level())
continue;
expr* candidate = ctx.bool_var2expr(v);
if (!candidate)
continue;
auto const& d = ctx.get_bdata(v);
if (d.m_phase_available && !d.m_phase)
candidate = m.mk_not(candidate);
double age = static_cast<double>(curr_time - ctx.get_birthdate(v));
all.push_back(solver::scored_literal(m, candidate, age));
}
std::stable_sort(
all.begin(),
all.end(),
[](solver::scored_literal const& a, solver::scored_literal const& b) {
return a.score > b.score;
});
unsigned n = std::min<unsigned>(max_num, all.size());
for (unsigned i = 0; i < n; ++i)
candidates.push_back(all[i]);
}
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
m_context.register_on_clause(ctx, on_clause);
}
@ -368,6 +466,39 @@ namespace {
return lits;
}
expr_ref cube_vsids(expr_ref_vector const& invalid_split_atoms) override {
ast_manager& m = get_manager();
auto& ctx = m_context.get_context();
obj_hashtable<expr> invalid_split_atoms_set;
for (expr* e : invalid_split_atoms) {
expr* atom = e;
m.is_not(e, atom);
invalid_split_atoms_set.insert(atom);
}
expr_ref result(m);
double score = 0.0;
unsigned n = 0;
ctx.pop_to_search_level();
for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
if (ctx.get_assignment(v) != l_undef)
continue;
expr* e = ctx.bool_var2expr(v);
if (!e)
continue;
expr* atom = e;
m.is_not(e, atom);
if (invalid_split_atoms_set.contains(atom))
continue;
double new_score = ctx.get_activity(v);
if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) {
score = new_score;
result = e;
}
}
return result;
}
struct collect_fds_proc {
ast_manager & m;
func_decl_set & m_fds;
@ -537,4 +668,3 @@ public:
solver_factory * mk_smt_solver_factory() {
return alloc(smt_solver_factory);
}

2
src/smt/smt_statistics.cpp
View file

@ -25,5 +25,5 @@ namespace smt {
memset(this, 0, sizeof(statistics));
}
};
}

3
src/smt/smt_statistics.h
View file

@ -45,13 +45,14 @@ namespace smt {
unsigned m_num_checks;
unsigned m_num_simplifications;
unsigned m_num_del_clauses;
unsigned m_num_assignments;
statistics() {
reset();
}
void reset();
};
};
}

7
src/smt/smt_theory.cpp
View file

@ -152,7 +152,8 @@ namespace smt {
expr_ref e(_e, m);
bool is_not = m.is_not(_e, _e);
if (!ctx.e_internalized(_e)) {
ctx.internalize(_e, is_quantifier(_e));
auto n = ctx.non_ground_internalize(_e);
_e = n->get_expr();
}
literal lit = ctx.get_literal(_e);
ctx.mark_as_relevant(lit);
@ -204,7 +205,7 @@ namespace smt {
log_axiom_instantiation(mk_or(fmls));
}
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, expr * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
ast_manager & m = get_manager();
SASSERT(r->get_ref_count() > 0);
std::ostream& out = m.trace_stream();
@ -261,5 +262,5 @@ namespace smt {
return get_th_var(ctx.get_enode(e));
}
};
}

12
src/smt/smt_theory.h
View file

@ -259,7 +259,7 @@ namespace smt {
\brief This method is invoked when the theory application n
is marked as relevant.
*/
virtual void relevant_eh(app * n) {
virtual void relevant_eh(expr * n) {
}
/**
@ -428,12 +428,14 @@ namespace smt {
smt_params const& get_fparams() const;
virtual void updt_params() {}
enode * get_enode(theory_var v) const {
SASSERT(v < static_cast<int>(m_var2enode.size()));
return m_var2enode[v];
}
app * get_expr(theory_var v) const {
expr * get_expr(theory_var v) const {
return get_enode(v)->get_expr();
}
@ -480,11 +482,11 @@ namespace smt {
protected:
void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
expr * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>());
void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
expr * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes);
}
@ -653,6 +655,6 @@ namespace smt {
virtual bool is_fixed_propagated(theory_var v, expr_ref& val, literal_vector & explain) { return false; }
};
};
}

2
src/smt/smt_types.h
View file

@ -72,6 +72,6 @@ namespace smt {
// if defined, then clauses have an extra mask field used to optimize backward subsumption, and backward/forward subsumption resolution.
#define APPROX_LIT_SET
};
}

2
src/smt/smt_value_sort.h
View file

@ -30,6 +30,6 @@ namespace smt {
bool is_value_sort(ast_manager& m, expr* e);
};
}

12
src/smt/tactic/smt_tactic_core.cpp
View file

@ -429,18 +429,26 @@ static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
parallel_params pp(p);
return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
}
tactic * mk_smt_tactic_core(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(m, p);
if (pp.enable())
return mk_parallel_tactic(mk_smt_solver(m, p, logic), p);
return mk_seq_smt_tactic(m, p);
}
tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config, params_ref const& _p) {
parallel_params pp(_p);
params_ref p = _p;
p.set_bool("auto_config", auto_config);
return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(m, p), p);
tactic *t = nullptr;
if (pp.enable())
t = mk_parallel_smt_tactic(m, p);
else
t = mk_seq_smt_tactic(m, p);
return using_params(t, p);
}

2
src/smt/theory_arith.cpp
View file

@ -27,4 +27,4 @@ namespace smt {
// template class theory_arith<smi_ext>;
template class smt::theory_arith<inf_ext>;
};
}

8
src/smt/theory_arith.h
View file

@ -524,7 +524,7 @@ namespace smt {
bool has_var(expr * v) const { return get_context().e_internalized(v) && get_context().get_enode(v)->get_th_var(get_id()) != null_theory_var; }
theory_var expr2var(expr * v) const { SASSERT(get_context().e_internalized(v)); return get_context().get_enode(v)->get_th_var(get_id()); }
expr * var2expr(theory_var v) const { return get_enode(v)->get_expr(); }
expr * var2expr(theory_var v) const { return get_expr(v); }
bool reflection_enabled() const;
bool reflect(app * n) const;
unsigned lazy_pivoting_lvl() const { return m_params.m_arith_lazy_pivoting_lvl; }
@ -656,7 +656,7 @@ namespace smt {
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
void relevant_eh(app * n) override;
void relevant_eh(expr * n) override;
void restart_eh() override;
void init_search_eh() override;
@ -966,7 +966,7 @@ namespace smt {
\brief A monomial is 'pure' if does not have a numeric coefficient.
*/
bool is_pure_monomial(expr * m) const;
bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_enode(v)->get_expr()); }
bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_expr(v)); }
void mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found);
void mark_dependents(theory_var v, svector<theory_var> & vars, var_set & already_found, row_set & already_visited_rows);
void get_non_linear_cluster(svector<theory_var> & vars);
@ -1277,6 +1277,6 @@ namespace smt {
// typedef theory_arith<smi_ext> theory_smi_arith;
};
}

14
src/smt/theory_arith_aux.h
View file

@ -147,7 +147,7 @@ namespace smt {
result_map[it->m_var] = -1;
}
}
};
}
#ifdef Z3DEBUG
/**
@ -1086,7 +1086,7 @@ namespace smt {
expr_ref theory_arith<Ext>::mk_gt(theory_var v) {
ast_manager& m = get_manager();
inf_numeral const& val = get_value(v);
expr* obj = get_enode(v)->get_expr();
expr* obj = get_expr(v);
expr_ref e(m);
rational r = val.get_rational();
if (m_util.is_int(obj->get_sort())) {
@ -1124,7 +1124,7 @@ namespace smt {
expr_ref theory_arith<Ext>::mk_ge(generic_model_converter& fm, theory_var v, inf_numeral const& val) {
ast_manager& m = get_manager();
std::ostringstream strm;
strm << val << " <= " << mk_pp(get_enode(v)->get_expr(), get_manager());
strm << val << " <= " << mk_pp(get_expr(v), get_manager());
app* b = m.mk_const(symbol(strm.str()), m.mk_bool_sort());
expr_ref result(b, m);
TRACE(opt, tout << result << "\n";);
@ -1799,7 +1799,7 @@ namespace smt {
*/
template<typename Ext>
typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) {
expr* e = get_enode(v)->get_expr();
expr* e = get_expr(v);
(void)e;
SASSERT(!maintain_integrality || valid_assignment());
SASSERT(satisfy_bounds());
@ -2179,8 +2179,8 @@ namespace smt {
TRACE(shared, tout << ctx.get_scope_level() << " " << v << " " << r->get_num_parents() << "\n";);
for (; it != end; ++it) {
enode * parent = *it;
app * o = parent->get_expr();
if (o->get_family_id() == get_id()) {
app* o = parent->get_app();
if (parent->get_family_id() == get_id()) {
switch (o->get_decl_kind()) {
case OP_DIV:
case OP_IDIV:
@ -2295,6 +2295,6 @@ namespace smt {
}
#endif
};
}

25
src/smt/theory_arith_core.h
View file

@ -1381,18 +1381,19 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::relevant_eh(app * n) {
void theory_arith<Ext>::relevant_eh(expr * n) {
TRACE(arith_relevant_eh, tout << "relevant_eh: " << mk_pp(n, m) << "\n";);
if (m_util.is_mod(n))
mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1));
else if (m_util.is_rem(n))
mk_rem_axiom(n->get_arg(0), n->get_arg(1));
else if (m_util.is_div(n))
mk_div_axiom(n->get_arg(0), n->get_arg(1));
expr* x = nullptr, *y = nullptr;
if (m_util.is_mod(n, x, y))
mk_idiv_mod_axioms(x, y);
else if (m_util.is_rem(n, x, y))
mk_rem_axiom(x, y);
else if (m_util.is_div(n, x, y))
mk_div_axiom(x, y);
else if (m_util.is_to_int(n))
mk_to_int_axiom(n);
mk_to_int_axiom(to_app(n));
else if (m_util.is_is_int(n))
mk_is_int_axiom(n);
mk_is_int_axiom(to_app(n));
}
template<typename Ext>
@ -1451,8 +1452,8 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::new_diseq_eh(theory_var v1, theory_var v2) {
TRACE(arith_new_diseq_eh, tout << mk_bounded_pp(get_enode(v1)->get_expr(), m) << "\n" <<
mk_bounded_pp(get_enode(v2)->get_expr(), m) << "\n";);
TRACE(arith_new_diseq_eh, tout << mk_bounded_pp(get_expr(v1), m) << "\n" <<
mk_bounded_pp(get_expr(v2), m) << "\n";);
m_stats.m_assert_diseq++;
m_arith_eq_adapter.new_diseq_eh(v1, v2);
}
@ -3569,5 +3570,5 @@ namespace smt {
}
};
}

2
src/smt/theory_arith_eq.h
View file

@ -346,6 +346,6 @@ namespace smt {
tout << enode_pp(_x, ctx) << " = " << enode_pp(_y, ctx) << "\n";);
ctx.assign_eq(_x, _y, eq_justification(js));
}
};
}

10
src/smt/theory_arith_int.h
View file

@ -215,7 +215,7 @@ namespace smt {
tout << "k = " << k << ", _k = "<< _k << std::endl;
);
expr_ref bound(m);
expr* e = get_enode(v)->get_expr();
expr* e = get_expr(v);
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
context & ctx = get_context();
{
@ -413,7 +413,7 @@ namespace smt {
for (; it != end; ++it) {
if (!it->is_dead() && it->m_var != b && is_free(it->m_var)) {
theory_var v = it->m_var;
expr* e = get_enode(v)->get_expr();
expr* e = get_expr(v);
bool _is_int = m_util.is_int(e);
expr_ref bound(m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)), get_manager());
context & ctx = get_context();
@ -629,9 +629,9 @@ namespace smt {
}
rational _k = k.to_rational();
if (is_lower)
bound = m_util.mk_ge(get_enode(v)->get_expr(), m_util.mk_numeral(_k, is_int(v)));
bound = m_util.mk_ge(get_expr(v), m_util.mk_numeral(_k, is_int(v)));
else
bound = m_util.mk_le(get_enode(v)->get_expr(), m_util.mk_numeral(_k, is_int(v)));
bound = m_util.mk_le(get_expr(v), m_util.mk_numeral(_k, is_int(v)));
}
else {
if (num_ints > 0) {
@ -1110,6 +1110,6 @@ namespace smt {
return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
}
};
}

2
src/smt/theory_arith_inv.h
View file

@ -229,6 +229,6 @@ namespace smt {
#endif
};
}

4
src/smt/theory_arith_nl.h
View file

@ -653,7 +653,7 @@ theory_var theory_arith<Ext>::find_nl_var_for_branching() {
bool computed_epsilon = false;
bool r = check_monomial_assignment(v, computed_epsilon);
if (!r) {
expr * m = get_enode(v)->get_expr();
expr * m = get_expr(v);
SASSERT(is_pure_monomial(m));
for (expr * arg : *to_app(m)) {
theory_var curr = ctx.get_enode(arg)->get_th_var(get_id());
@ -2410,7 +2410,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
}
};
}

4
src/smt/theory_arith_pp.h
View file

@ -484,7 +484,7 @@ namespace smt {
pp.set_benchmark_name("lemma");
int n = get_num_vars();
for (theory_var v = 0; v < n; ++v) {
expr * n = get_enode(v)->get_expr();
expr * n = get_expr(v);
if (is_fixed(v)) {
inf_numeral k_inf = lower_bound(v);
rational k = k_inf.get_rational().to_rational();
@ -528,6 +528,6 @@ namespace smt {
id++;
}
};
}

63
src/smt/theory_array.cpp
View file

@ -42,7 +42,7 @@ namespace smt {
// v1 is the new root
TRACE(array,
tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1);
tout << mk_pp(get_enode(v1)->get_expr(), m) << " <- " << mk_pp(get_enode(v2)->get_expr(), m) << "\n";);
tout << mk_pp(get_expr(v1), m) << " <- " << mk_pp(get_expr(v2), m) << "\n";);
SASSERT(v1 == find(v1));
var_data * d1 = m_var_data[v1];
var_data * d2 = m_var_data[v2];
@ -68,12 +68,12 @@ namespace smt {
m_var_data.push_back(alloc(var_data));
var_data * d = m_var_data[r];
TRACE(array, tout << mk_bounded_pp(n->get_expr(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
", is_store: " << is_store(n) << "\n";);
", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n->get_expr()) << "\n";);
d->m_is_array = is_array_sort(n);
if (d->m_is_array)
register_sort(n->get_expr()->get_sort());
d->m_is_select = is_select(n);
if (is_store(n))
if (is_store(n) || is_lambda(n->get_expr()))
d->m_stores.push_back(n);
ctx.attach_th_var(n, this, r);
if (laziness() <= 1 && is_store(n))
@ -88,14 +88,14 @@ namespace smt {
v = find(v);
var_data * d = m_var_data[v];
d->m_parent_selects.push_back(s);
TRACE(array, tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_enode(v)->get_expr(), m) << "\n";);
TRACE(array, tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_expr(v), m) << "\n";);
m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_selects));
for (enode* n : d->m_stores)
instantiate_axiom2a(s, n);
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode* store : d->m_parent_stores) {
SASSERT(is_store(store));
SASSERT(is_store(store) || is_lambda(store->get_expr()));
if (!m_params.m_array_cg || store->is_cgr()) {
instantiate_axiom2b(s, store);
}
@ -106,7 +106,7 @@ namespace smt {
void theory_array::add_parent_store(theory_var v, enode * s) {
if (m_params.m_array_cg && !s->is_cgr())
return;
SASSERT(is_store(s));
SASSERT(is_store(s) || is_lambda(s->get_expr()));
v = find(v);
var_data * d = m_var_data[v];
d->m_parent_stores.push_back(s);
@ -177,7 +177,7 @@ namespace smt {
void theory_array::add_store(theory_var v, enode * s) {
if (m_params.m_array_cg && !s->is_cgr())
return;
SASSERT(is_store(s));
SASSERT(is_store(s) || is_lambda(s->get_expr()));
v = find(v);
var_data * d = m_var_data[v];
unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d);
@ -204,7 +204,7 @@ namespace smt {
void theory_array::instantiate_axiom2a(enode * select, enode * store) {
TRACE(array, tout << "axiom 2a: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
SASSERT(is_select(select));
SASSERT(is_store(store));
SASSERT(is_store(store) || is_lambda(store->get_expr()));
if (assert_store_axiom2(store, select))
m_stats.m_num_axiom2a++;
}
@ -212,7 +212,7 @@ namespace smt {
bool theory_array::instantiate_axiom2b(enode * select, enode * store) {
TRACE(array_axiom2b, tout << "axiom 2b: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
SASSERT(is_select(select));
SASSERT(is_store(store));
SASSERT(is_store(store) || is_lambda(store->get_expr()));
if (assert_store_axiom2(store, select)) {
m_stats.m_num_axiom2b++;
return true;
@ -261,7 +261,7 @@ namespace smt {
}
bool theory_array::internalize_term(app * n) {
if (!is_store(n) && !is_select(n)) {
if (!is_store(n) && !is_select(n) && !is_lambda(n)) {
if (!is_array_ext(n))
found_unsupported_op(n);
return false;
@ -282,7 +282,7 @@ namespace smt {
if (is_select(n)) {
add_parent_select(v_arg, ctx.get_enode(n));
}
else if (is_store(n)) {
else if (is_store(n) || is_lambda(n)) {
add_parent_store(v_arg, ctx.get_enode(n));
}
}
@ -298,11 +298,6 @@ namespace smt {
void theory_array::new_eq_eh(theory_var v1, theory_var v2) {
m_find.merge(v1, v2);
enode* n1 = get_enode(v1), *n2 = get_enode(v2);
if (n1->get_expr()->get_decl()->is_lambda() ||
n2->get_expr()->get_decl()->is_lambda()) {
assert_congruent(n1, n2);
}
}
void theory_array::new_diseq_eh(theory_var v1, theory_var v2) {
@ -310,8 +305,8 @@ namespace smt {
v2 = find(v2);
var_data * d1 = m_var_data[v1];
TRACE(ext, tout << "extensionality: " << d1->m_is_array << "\n"
<< mk_bounded_pp(get_enode(v1)->get_expr(), m, 5) << "\n"
<< mk_bounded_pp(get_enode(v2)->get_expr(), m, 5) << "\n";);
<< mk_bounded_pp(get_expr(v1), m, 5) << "\n"
<< mk_bounded_pp(get_expr(v2), m, 5) << "\n";);
if (d1->m_is_array) {
SASSERT(m_var_data[v2]->m_is_array);
@ -319,16 +314,18 @@ namespace smt {
}
}
void theory_array::relevant_eh(app * n) {
void theory_array::relevant_eh(expr * n) {
if (laziness() == 0)
return;
if (m.is_ite(n)) {
TRACE(array, tout << "relevant ite " << mk_pp(n, m) << "\n";);
}
if (!is_store(n) && !is_select(n))
if (!is_store(n) && !is_select(n) && !is_lambda(n))
return;
if (!ctx.e_internalized(n)) ctx.internalize(n, false);
enode * arg = ctx.get_enode(n->get_arg(0));
if (is_lambda(n))
return;
enode * arg = ctx.get_enode(to_app(n)->get_arg(0));
theory_var v_arg = arg->get_th_var(get_id());
SASSERT(v_arg != null_theory_var);
@ -374,14 +371,14 @@ namespace smt {
else {
if (mk_interface_eqs_at_final_check() == FC_CONTINUE)
r = FC_CONTINUE;
else
else
r = assert_delayed_axioms();
}
}
else {
if (m_final_check_idx % 2 == 1) {
r = assert_delayed_axioms();
if (r == FC_DONE)
if (r == FC_DONE)
r = mk_interface_eqs_at_final_check();
}
else {
@ -392,22 +389,22 @@ namespace smt {
}
}
bool should_giveup = m_found_unsupported_op || has_propagate_up_trail();
if (r == FC_DONE && should_giveup && !ctx.get_fparams().m_array_fake_support)
if (r == FC_DONE && should_giveup && !ctx.get_fparams().m_array_fake_support)
r = FC_GIVEUP;
CTRACE(array, r != FC_DONE || m_found_unsupported_op, tout << r << "\n";);
return r;
}
final_check_status theory_array::assert_delayed_axioms() {
if (!m_params.m_array_delay_exp_axiom)
return FC_DONE;
final_check_status r = FC_DONE;
unsigned num_vars = get_num_vars();
for (unsigned v = 0; v < num_vars; ++v) {
var_data * d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom2b_for(v))
r = FC_CONTINUE;
}
if (m_params.m_array_delay_exp_axiom) {
unsigned num_vars = get_num_vars();
for (unsigned v = 0; v < num_vars; ++v) {
var_data *d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom2b_for(v))
r = FC_CONTINUE;
}
}
return r;
}
@ -508,4 +505,4 @@ namespace smt {
st.update("array splits", m_stats.m_num_eq_splits);
}
};
}

8
src/smt/theory_array.h
View file

@ -28,7 +28,8 @@ namespace smt {
unsigned m_num_axiom1, m_num_axiom2a, m_num_axiom2b, m_num_extensionality, m_num_eq_splits;
unsigned m_num_map_axiom, m_num_default_map_axiom;
unsigned m_num_select_const_axiom, m_num_default_store_axiom, m_num_default_const_axiom, m_num_default_as_array_axiom;
unsigned m_num_select_as_array_axiom, m_num_default_lambda_axiom;
unsigned m_num_select_as_array_axiom, m_num_default_lambda_axiom, m_num_choice_axiom;
unsigned m_num_select_lambda_axiom;
void reset() { memset(this, 0, sizeof(theory_array_stats)); }
theory_array_stats() { reset(); }
};
@ -59,7 +60,7 @@ namespace smt {
void apply_sort_cnstr(enode * n, sort * s) override;
void new_eq_eh(theory_var v1, theory_var v2) override;
void new_diseq_eh(theory_var v1, theory_var v2) override;
void relevant_eh(app * n) override;
void relevant_eh(expr * n) override;
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
final_check_status final_check_eh(unsigned) override;
@ -113,6 +114,5 @@ namespace smt {
ptr_vector<enode> const& parent_selects(enode* n) { return m_var_data[find(n->get_root()->get_th_var(get_id()))]->m_parent_selects; }
};
};
}

196
src/smt/theory_array_base.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "smt/smt_model_generator.h"
#include "model/func_interp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/pattern/pattern_inference.h"
namespace smt {
@ -67,7 +68,6 @@ namespace smt {
return mk_select(num_args, args);
}
app * theory_array_base::mk_store(unsigned num_args, expr * const * args) {
return m.mk_app(get_family_id(), OP_STORE, 0, nullptr, num_args, args);
}
@ -108,7 +108,7 @@ namespace smt {
}
void theory_array_base::assert_store_axiom1_core(enode * e) {
app * n = e->get_expr();
app * n = e->get_app();
SASSERT(is_store(n));
ptr_buffer<expr> sel_args;
unsigned num_args = n->get_num_args();
@ -217,28 +217,48 @@ namespace smt {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
}
}
void theory_array_base::assert_lambda_axiom_core(enode* n, enode* select) {
SASSERT(is_lambda(n->get_expr()));
SASSERT(is_select(select));
expr *e = n->get_expr();
SASSERT(is_lambda(e));
app *s = select->get_app();
auto q = to_quantifier(e);
SASSERT(q);
SASSERT(q->get_num_decls() == s->get_num_args() - 1);
// do the same thing as in sat/smt/array_axioms:
ptr_vector<expr> args(s->get_num_args(), s->get_args());
args[0] = q;
array_util a(m);
expr_ref alpha(a.mk_select(args), m);
expr_ref beta(alpha);
ctx.get_rewriter()(beta);
TRACE(array, tout << alpha << " == " << beta << "\n";);
auto alpha_n = ensure_enode(alpha);
auto beta_n = ensure_enode(beta);
ctx.assign_eq(alpha_n, beta_n, eq_justification::mk_axiom());
}
bool theory_array_base::assert_store_axiom2(enode * store, enode * select) {
SASSERT(is_store(store) || is_lambda(store->get_expr()));
unsigned num_args = select->get_num_args();
unsigned i = 1;
for (; i < num_args; ++i)
if (store->get_arg(i)->get_root() != select->get_arg(i)->get_root())
if (is_store(store) && store->get_arg(i)->get_root() != select->get_arg(i)->get_root())
break;
if (i == num_args)
return false;
if (ctx.add_fingerprint(store, store->get_owner_id(), select->get_num_args() - 1, select->get_args() + 1)) {
TRACE(array, tout << "adding axiom2 to todo queue\n";);
m_axiom2_todo.push_back(std::make_pair(store, select));
m_axiom2_todo.push_back({store, select});
return true;
}
TRACE(array, tout << "axiom already instantiated: #" << store->get_owner_id() << " #" << select->get_owner_id() << "\n";);
return false;
}
func_decl_ref_vector * theory_array_base::register_sort(sort * s_array) {
unsigned dimension = get_dimension(s_array);
func_decl_ref_vector * ext_skolems = nullptr;
@ -259,7 +279,7 @@ namespace smt {
SASSERT(n1->get_num_args() == n2->get_num_args());
unsigned n = n1->get_num_args();
// skipping first argument of the select.
for(unsigned i = 1; i < n; ++i) {
for (unsigned i = 1; i < n; ++i) {
if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) {
return false;
}
@ -275,9 +295,8 @@ namespace smt {
enode * r1 = v1->get_root();
enode * r2 = v2->get_root();
if (r1->get_class_size() > r2->get_class_size()) {
std::swap(r1, r2);
}
if (r1->get_class_size() > r2->get_class_size())
std::swap(r1, r2);
m_array_value.reset();
// populate m_array_value if the select(a, i) parent terms of r1
@ -315,11 +334,13 @@ namespace smt {
return false; // axiom was already instantiated
if (already_diseq(n1, n2))
return false;
m_extensionality_todo.push_back(std::make_pair(n1, n2));
m_extensionality_todo.push_back({n1, n2});
return true;
}
void theory_array_base::assert_congruent(enode * a1, enode * a2) {
if (ctx.get_fparams().m_array_fake_support)
return;
TRACE(array, tout << "congruent: #" << a1->get_owner_id() << " #" << a2->get_owner_id() << "\n";);
SASSERT(is_array_sort(a1));
SASSERT(is_array_sort(a2));
@ -328,13 +349,13 @@ namespace smt {
enode * nodes[2] = { a1, a2 };
if (!ctx.add_fingerprint(this, 1, 2, nodes))
return; // axiom was already instantiated
m_congruent_todo.push_back(std::make_pair(a1, a2));
m_congruent_todo.push_back({a1, a2});
}
void theory_array_base::assert_extensionality_core(enode * n1, enode * n2) {
app * e1 = n1->get_expr();
app * e2 = n2->get_expr();
expr * e1 = n1->get_expr();
expr * e2 = n2->get_expr();
func_decl_ref_vector * funcs = nullptr;
sort * s = e1->get_sort();
@ -371,15 +392,15 @@ namespace smt {
\brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars)
*/
void theory_array_base::assert_congruent_core(enode * n1, enode * n2) {
app * e1 = n1->get_expr();
app * e2 = n2->get_expr();
expr * e1 = n1->get_expr();
expr * e2 = n2->get_expr();
sort* s = e1->get_sort();
unsigned dimension = get_array_arity(s);
literal n1_eq_n2 = mk_eq(e1, e2, true);
ctx.mark_as_relevant(n1_eq_n2);
expr_ref_vector args1(m), args2(m);
args1.push_back(instantiate_lambda(e1));
args2.push_back(instantiate_lambda(e2));
args1.push_back(e1);
args2.push_back(e2);
svector<symbol> names;
sort_ref_vector sorts(m);
for (unsigned i = 0; i < dimension; ++i) {
@ -395,6 +416,16 @@ namespace smt {
expr * eq = m.mk_eq(sel1, sel2);
expr_ref q(m.mk_forall(dimension, sorts.data(), names.data(), eq), m);
ctx.get_rewriter()(q);
// The select terms are beta-reduced away by the rewriter, so the
// resulting quantifier carries no patterns. Infer patterns so that the
// e-matching engine can instantiate it (dynamically generated
// quantifiers bypass the pre-processing pattern inference pass).
if (is_forall(q) && to_quantifier(q)->get_num_patterns() == 0) {
pattern_inference_rw infer(m, ctx.get_fparams());
expr_ref q2(m);
infer(q, q2);
q = q2;
}
if (!ctx.b_internalized(q)) {
ctx.internalize(q, true);
}
@ -403,17 +434,6 @@ namespace smt {
assert_axiom(~n1_eq_n2, fa_eq);
}
expr_ref theory_array_base::instantiate_lambda(app* e) {
quantifier * q = m.is_lambda_def(e->get_decl());
expr_ref f(e, m);
if (q) {
// the variables in q are maybe not consecutive.
var_subst sub(m, false);
f = sub(q, e->get_num_args(), e->get_args());
}
return f;
}
bool theory_array_base::can_propagate() {
return
!m_axiom1_todo.empty() ||
@ -424,13 +444,16 @@ namespace smt {
}
void theory_array_base::propagate() {
while (can_propagate()) {
while (theory_array_base::can_propagate()) {
for (unsigned i = 0; i < m_axiom1_todo.size(); ++i)
assert_store_axiom1_core(m_axiom1_todo[i]);
m_axiom1_todo.reset();
for (unsigned i = 0; i < m_axiom2_todo.size(); ++i) {
auto [store, select] = m_axiom2_todo[i];
assert_store_axiom2_core(store, select);
if (is_store(store))
assert_store_axiom2_core(store, select);
else
assert_lambda_axiom_core(store, select);
}
m_axiom2_todo.reset();
for (unsigned i = 0; i < m_extensionality_todo.size(); ++i) {
@ -524,6 +547,7 @@ namespace smt {
unsigned num_vars = get_num_vars();
for (unsigned i = 0; i < num_vars; ++i) {
enode * n = get_enode(i);
TRACE(array, tout << enode_pp(n, ctx) << " is_relevant: " << ctx.is_relevant(n) << " is_array: " << is_array_sort(n) << "\n";);
if (!ctx.is_relevant(n) || !is_array_sort(n)) {
continue;
}
@ -561,19 +585,20 @@ namespace smt {
TRACE(array_bug, tout << "mk_interface_eqs: processing: v" << *it1 << "\n";);
theory_var v1 = *it1;
enode * n1 = get_enode(v1);
sort * s1 = n1->get_expr()->get_sort();
sort * s1 = n1->get_sort();
sbuffer<theory_var>::iterator it2 = it1;
++it2;
for (; it2 != end1; ++it2) {
theory_var v2 = *it2;
enode * n2 = get_enode(v2);
sort * s2 = n2->get_expr()->get_sort();
sort * s2 = n2->get_sort();
if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
app * eq = mk_eq_atom(n1->get_expr(), n2->get_expr());
if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
app_ref eq = app_ref(mk_eq_atom(n1->get_expr(), n2->get_expr()), m);
TRACE(array_bug, tout << "mk_interface_eqs: adding: " << eq << "\n";);
if (!ctx.b_internalized(eq.get()) || !ctx.is_relevant(eq.get())) {
result++;
ctx.internalize(eq, true);
ctx.mark_as_relevant(eq);
ctx.mark_as_relevant(eq.get());
}
}
}
@ -687,6 +712,8 @@ namespace smt {
collect_defaults();
collect_selects();
propagate_selects();
// check_selects();
TRACE(array, display_selects(tout); display(tout););
}
/**
@ -784,12 +811,89 @@ namespace smt {
return set;
}
void theory_array_base::collect_selects() {
int num_vars = get_num_vars();
void theory_array_base::reset_selects() {
for (auto r : m_selects_range)
dealloc(r);
m_selects_range.reset();
m_selects.reset();
m_selects_domain.reset();
m_selects_range.reset();
}
std::ostream& theory_array_base::display_selects(std::ostream& out) {
for (auto [r, s] : m_selects) {
out << enode_pp(r, ctx) << ":\n";
for (auto sel : *s)
out << " " << enode_pp(sel, ctx) << " "
<< enode_pp(sel->get_root(), ctx) << "\n";
out << "\n";
}
return out;
}
bool theory_array_base::check_selects() {
auto same_args = [&](unsigned num_args, enode *n1, enode *n2) {
for (unsigned i = 1; i < num_args; ++i) {
if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root())
return false;
}
return true;
};
auto check_selects = [&](enode* n, select_set &s1, select_set &s2) {
for (auto sel1 : s1) {
if (same_args(sel1->get_num_args(), sel1, n))
continue;
bool found = false;
for (auto sel2 : s2) {
verbose_stream() << "check_selects: " << enode_pp(sel1, ctx) << " " << enode_pp(sel2, ctx) << "\n";
if (!same_args(sel2->get_num_args(), sel1, sel2))
continue;
found = true;
if (sel1->get_root() != sel2->get_root()) {
verbose_stream() << "selects: " << pp(sel1, m) << " " << pp(sel2, m) << "\n";
return false;
}
break;
}
if (!found) {
verbose_stream() << "selects: " << pp(sel1, m) << " " << pp(n, m) << "\n";
return false;
}
}
return true;
};
for (auto [r, s1] : m_selects) {
for (auto n : *r) {
if (false && !ctx.is_relevant(n))
continue;
if (is_store(n)) {
auto st = n->get_arg(0)->get_root();
auto &s2 = m_selects[st];
if (!check_selects(n, *s1, *s2))
return false;
if (!check_selects(n, *s2, *s1))
return false;
}
if (is_const(n)) {
auto v = n->get_arg(0)->get_root();
for (auto sel : *s1) {
if (v != sel->get_root()) {
verbose_stream() << pp(n, m) << " != " << pp(sel, m) << "\n";
return false;
}
}
}
}
}
return true;
}
void theory_array_base::collect_selects() {
int num_vars = get_num_vars();
reset_selects();
for (theory_var v = 0; v < num_vars; ++v) {
enode * r = get_enode(v)->get_root();
@ -838,7 +942,7 @@ namespace smt {
if (i < num_args) {
SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
parent_sel_set->insert(sel);
todo.push_back(std::make_pair(parent_root, sel));
todo.push_back({parent_root, sel});
}
}
}
@ -864,7 +968,7 @@ namespace smt {
}
void theory_array_base::finalize_model(model_generator & m) {
std::for_each(m_selects_range.begin(), m_selects_range.end(), delete_proc<select_set>());
reset_selects();
}
class array_value_proc : public model_value_proc {
@ -974,7 +1078,7 @@ namespace smt {
model_value_proc * theory_array_base::mk_value(enode * n, model_generator & mg) {
theory_var v = n->get_th_var(get_id());
SASSERT(v != null_theory_var);
sort * s = n->get_expr()->get_sort();
sort * s = n->get_sort();
enode * else_val_n = get_default(v);
array_value_proc * result = nullptr;
@ -1041,4 +1145,4 @@ namespace smt {
return result;
}
};
}

36
src/smt/theory_array_base.h
View file

@ -34,25 +34,31 @@ namespace smt {
virtual void set_prop_upward(theory_var v) {}
void found_unsupported_op(expr * n);
void found_unsupported_op(enode* n) { found_unsupported_op(n->get_expr()); }
void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_expr()); }
void found_unsupported_op(theory_var v) { found_unsupported_op(get_expr(v)); }
bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); }
bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); }
bool is_select(app const* n) const { return n->is_app_of(get_id(), OP_SELECT); }
bool is_default(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_DEFAULT); }
bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); }
bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
bool is_store(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_STORE); }
bool is_map(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_MAP); }
bool is_select(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_SELECT); }
bool is_default(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_DEFAULT); }
bool is_const(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CONST_ARRAY); }
bool is_array_ext(expr const * n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_ARRAY_EXT); }
bool is_as_array(expr const * n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_AS_ARRAY); }
bool is_choice(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CHOICE); }
bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); }
bool is_array_sort(expr const* n) const { return is_array_sort(n->get_sort()); }
bool is_store(enode const * n) const { return is_store(n->get_expr()); }
bool is_map(enode const* n) const { return is_map(n->get_expr()); }
bool is_select(enode const* n) const { return is_select(n->get_expr()); }
bool is_const(enode const* n) const { return is_const(n->get_expr()); }
bool is_as_array(enode const * n) const { return is_as_array(n->get_expr()); }
bool is_choice(enode const* n) const { return is_choice(n->get_expr()); }
bool is_default(enode const* n) const { return is_default(n->get_expr()); }
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_expr()); }
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_sort()); }
bool is_select_arg(enode* r);
app * mk_select(unsigned num_args, expr * const * args);
@ -74,13 +80,14 @@ namespace smt {
void assert_axiom(literal l);
void assert_store_axiom1_core(enode * n);
void assert_store_axiom2_core(enode * store, enode * select);
void assert_lambda_axiom_core(enode *lambda, enode *select);
void assert_store_axiom1(enode * n) { m_axiom1_todo.push_back(n); }
bool assert_store_axiom2(enode * store, enode * select);
void assert_extensionality_core(enode * a1, enode * a2);
bool assert_extensionality(enode * a1, enode * a2);
expr_ref instantiate_lambda(app* e);
expr_ref instantiate_lambda(expr* e);
void assert_congruent_core(enode * a1, enode * a2);
void assert_congruent(enode * a1, enode * a2);
@ -184,6 +191,10 @@ namespace smt {
ptr_vector<select_set> m_selects_range;
bool m_use_unspecified_default; // temporary field for model construction
void reset_selects();
std::ostream &display_selects(std::ostream &out);
bool check_selects();
theory_var mg_find(theory_var v);
void mg_merge(theory_var n, theory_var m);
@ -206,6 +217,5 @@ namespace smt {
~theory_array_base() override { restore_sorts(0); }
};
};
}

159
src/smt/theory_array_full.cpp
View file

@ -248,7 +248,7 @@ namespace smt {
instantiate_default_as_array_axiom(n);
d->m_as_arrays.push_back(n);
}
else if (m.is_lambda_def(n->get_decl())) {
else if (is_lambda(n->get_expr())) {
instantiate_default_lambda_def_axiom(n);
d->m_lambdas.push_back(n);
m_lambdas.push_back(n);
@ -271,7 +271,7 @@ namespace smt {
return theory_array::internalize_term(n);
}
if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n)) {
if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_choice(n)) {
if (!is_array_ext(n))
found_unsupported_op(n);
return false;
@ -354,6 +354,14 @@ namespace smt {
add_as_array(v1, n);
for (enode* n : d2->m_lambdas)
add_lambda(v1, n);
// When a lambda is equated to another array term, assert the congruence
// axiom n1 = n2 => forall k . select(n1, k) = select(n2, k).
// This lets positive equalities between lambdas (which have no select
// parents of their own) produce usable consequences.
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
if (is_lambda(n1->get_expr()) || is_lambda(n2->get_expr()))
assert_congruent(n1, n2);
TRACE(array,
tout << pp(get_enode(v1), m) << "\n";
tout << pp(get_enode(v2), m) << "\n";
@ -368,8 +376,8 @@ namespace smt {
TRACE(array, tout << "v" << v << " " << pp(get_enode(v), m) << " "
<< d->m_prop_upward << " " << m_params.m_array_delay_exp_axiom << "\n";);
for (enode * store : d->m_stores) {
SASSERT(is_store(store));
instantiate_default_store_axiom(store);
if (is_store(store))
instantiate_default_store_axiom(store);
}
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
@ -393,6 +401,10 @@ namespace smt {
SASSERT(is_map(map));
instantiate_select_map_axiom(s, map);
}
for (enode *lam : d_full->m_lambdas) {
SASSERT(is_lambda(lam->get_expr()));
instantiate_select_lambda_axiom(s, lam);
}
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode * map : d_full->m_parent_maps) {
SASSERT(is_map(map));
@ -403,22 +415,23 @@ namespace smt {
}
}
void theory_array_full::relevant_eh(app* n) {
void theory_array_full::relevant_eh(expr* n) {
TRACE(array, tout << mk_pp(n, m) << "\n";);
theory_array::relevant_eh(n);
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){
if (!is_default(n) && !is_select(n) && !is_map(n) &&
!is_const(n) && !is_as_array(n) && !is_choice(n)) {
return;
}
ctx.ensure_internalized(n);
enode* node = ctx.get_enode(n);
if (is_select(n)) {
enode * arg = ctx.get_enode(n->get_arg(0));
enode * arg = ctx.get_enode(to_app(n)->get_arg(0));
theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var);
add_parent_select(find(v), node);
}
else if (is_default(n)) {
enode * arg = ctx.get_enode(n->get_arg(0));
enode * arg = ctx.get_enode(to_app(n)->get_arg(0));
theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var);
set_prop_upward(v);
@ -431,7 +444,7 @@ namespace smt {
add_parent_default(find(v));
}
else if (is_map(n)) {
for (expr * e : *n) {
for (expr * e : *to_app(n)) {
enode* arg = ctx.get_enode(e);
theory_var v_arg = find(arg->get_th_var(get_id()));
add_parent_map(v_arg, node);
@ -442,6 +455,10 @@ namespace smt {
else if (is_as_array(n)) {
instantiate_default_as_array_axiom(node);
}
else if (is_choice(n)) {
m_choice_terms.push_back(node);
ctx.push_trail(push_back_vector(m_choice_terms));
}
}
bool theory_array_full::should_research(expr_ref_vector & unsat_core) {
@ -456,14 +473,13 @@ namespace smt {
// select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i))
//
bool theory_array_full::instantiate_select_map_axiom(enode* sl, enode* mp) {
app* map = mp->get_expr();
app* select = sl->get_expr();
app* map = mp->get_app();
app* select = sl->get_app();
SASSERT(is_map(map));
SASSERT(is_select(select));
SASSERT(map->get_num_args() > 0);
func_decl* f = to_func_decl(map->get_decl()->get_parameter(0).get_ast());
TRACE(array_map_bug, tout << "invoked instantiate_select_map_axiom\n";
tout << sl->get_owner_id() << " " << mp->get_owner_id() << "\n";
tout << mk_ismt2_pp(sl->get_expr(), m) << "\n" << mk_ismt2_pp(mp->get_expr(), m) << "\n";);
@ -513,6 +529,34 @@ namespace smt {
return try_assign_eq(sel1, sel2);
}
bool theory_array_full::instantiate_select_lambda_axiom(enode* sl, enode* lambda) {
app* select = sl->get_app();
SASSERT(is_select(select));
SASSERT(is_lambda(lambda->get_expr()));
SASSERT(lambda->get_sort() == sl->get_arg(0)->get_sort());
if (!ctx.add_fingerprint(lambda, lambda->get_owner_id(), sl->get_num_args() - 1, sl->get_args() + 1)) {
return false;
}
m_stats.m_num_select_lambda_axiom++;
unsigned num_args = select->get_num_args();
ptr_buffer<expr> args;
args.push_back(lambda->get_expr());
for (unsigned i = 1; i < num_args; ++i)
args.push_back(select->get_arg(i));
expr_ref sel1(m), sel2(m);
sel1 = mk_select(args.size(), args.data());
sel2 = sel1;
ctx.get_rewriter()(sel2);
ctx.internalize(sel1, false);
ctx.internalize(sel2, false);
TRACE(array, tout << mk_bounded_pp(sel1, m) << "\n==\n" << mk_bounded_pp(sel2, m) << "\n";);
return try_assign_eq(sel1, sel2);
}
//
//
@ -523,7 +567,7 @@ namespace smt {
bool theory_array_full::instantiate_default_map_axiom(enode* mp) {
SASSERT(is_map(mp));
app* map = mp->get_expr();
app* map = mp->get_app();
if (!ctx.add_fingerprint(this, m_default_map_fingerprint, 1, &mp)) {
return false;
}
@ -573,27 +617,44 @@ namespace smt {
if (!ctx.add_fingerprint(this, m_default_lambda_fingerprint, 1, &arr))
return false;
m_stats.m_num_default_lambda_axiom++;
expr* e = arr->get_expr();
expr_ref def(mk_default(e), m);
quantifier* lam = m.is_lambda_def(arr->get_decl());
TRACE(array, tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
quantifier *lam = to_quantifier(arr->get_expr());
expr_ref def(mk_default(arr->get_expr()), m);
TRACE(array, tout << mk_pp(lam, m) << "\n");
expr_ref_vector args(m);
var_subst subst(m, false);
args.push_back(subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args()));
args.push_back(lam);
for (unsigned i = 0; i < lam->get_num_decls(); ++i)
args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
expr_ref val(mk_select(args), m);
ctx.get_rewriter()(val);
if (has_quantifiers(val)) {
expr_ref fn(m.mk_fresh_const("lambda-body", val->get_sort()), m);
expr_ref eq(m.mk_eq(fn, val), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
val = fn;
}
ctx.internalize(def, false);
ctx.internalize(val.get(), false);
return try_assign_eq(val.get(), def);
auto val_e = ctx.non_ground_internalize(val);
return try_assign_eq(val_e->get_expr(), def);
}
bool theory_array_full::instantiate_choice_axiom(enode* ch) {
if (!ctx.add_fingerprint(this, m_choice_fingerprint, 1, &ch))
return false;
++m_stats.m_num_choice_axiom;
SASSERT(is_choice(ch));
app* choice_term = ch->get_app();
expr* pred = choice_term->get_arg(0);
sort* pred_sort = pred->get_sort();
SASSERT(is_array_sort(pred_sort));
SASSERT(get_array_arity(pred_sort) == 1);
SASSERT(m.is_bool(get_array_range(pred_sort)));
sort* x_sort = get_array_domain(pred_sort, 0);
expr_ref x(m.mk_var(0, x_sort), m);
expr* args1[2] = { pred, x };
expr_ref px(mk_select(2, args1), m);
expr* args2[2] = { pred, choice_term };
expr_ref pc(mk_select(2, args2), m);
expr_ref body(m.mk_implies(px, pc), m);
symbol x_name("x");
expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
ctx.get_rewriter()(q);
TRACE(array, tout << "choice " << q << "\n");
ctx.assert_expr(q);
ctx.internalize_assertions();
return true;
}
//
@ -613,10 +674,10 @@ namespace smt {
ptr_buffer<expr> sel_args;
sel_args.push_back(cnst->get_expr());
for (unsigned short i = 1; i < num_args; ++i) {
sel_args.push_back(select->get_expr()->get_arg(i));
sel_args.push_back(select->get_app()->get_arg(i));
}
expr * sel = mk_select(sel_args.size(), sel_args.data());
expr * val = cnst->get_expr()->get_arg(0);
expr * val = cnst->get_app()->get_arg(0);
TRACE(array, tout << "new select-const axiom...\n";
tout << "const: " << mk_bounded_pp(cnst->get_expr(), m) << "\n";
tout << "select: " << mk_bounded_pp(select->get_expr(), m) << "\n";
@ -647,7 +708,7 @@ namespace smt {
ptr_buffer<expr> sel_args;
sel_args.push_back(arr->get_expr());
for (unsigned short i = 1; i < num_args; ++i) {
sel_args.push_back(select->get_expr()->get_arg(i));
sel_args.push_back(select->get_app()->get_arg(i));
}
expr * sel = mk_select(sel_args.size(), sel_args.data());
func_decl * f = array_util(m).get_as_array_func_decl(arr->get_expr());
@ -669,7 +730,7 @@ namespace smt {
bool theory_array_full::instantiate_default_store_axiom(enode* store) {
SASSERT(is_store(store));
SASSERT(store->get_num_args() >= 3);
app* store_app = store->get_expr();
app* store_app = store->get_app();
if (!ctx.add_fingerprint(this, m_default_store_fingerprint, store->get_num_args(), store->get_args())) {
return false;
}
@ -747,6 +808,17 @@ namespace smt {
return {eps, diag};
}
void theory_array_full::propagate() {
theory_array::propagate();
if (m_choice_qhead == m_choice_terms.size())
return;
ctx.push_trail(value_trail(m_choice_qhead));
for (; m_choice_qhead < m_choice_terms.size(); ++m_choice_qhead) {
enode *choice = m_choice_terms[m_choice_qhead];
instantiate_choice_axiom(choice);
}
}
final_check_status theory_array_full::assert_delayed_axioms() {
final_check_status r = FC_DONE;
if (!m_params.m_array_delay_exp_axiom) {
@ -772,6 +844,8 @@ namespace smt {
}
bool theory_array_full::has_non_beta_as_array() {
if (ctx.get_fparams().m_array_fake_support)
return false;
for (enode* n : m_as_array) {
for (enode* p : n->get_parents())
if (ctx.is_relevant(p) && !ctx.is_beta_redex(p, n)) {
@ -781,13 +855,28 @@ namespace smt {
}
for (enode* n : m_lambdas)
for (enode* p : n->get_parents())
if (ctx.is_relevant(p) && !is_default(p) && !ctx.is_beta_redex(p, n)) {
if (ctx.is_relevant(p) && !is_default(p) && !is_select(p) && !ctx.is_beta_redex(p, n) && !is_congruent_eq(p)) {
TRACE(array, tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n");
return true;
}
return false;
}
/**
\brief A relevant equality between two array terms whose roots coincide is
handled by the congruence axiom asserted on merge (see merge_eh /
assert_congruent). Such an equality parent does not make a lambda an
unsupported (non beta-redex) occurrence, so it should not trigger a
final-check give-up.
*/
bool theory_array_full::is_congruent_eq(enode* p) {
expr* a = nullptr, * b = nullptr;
if (!m.is_eq(p->get_expr(), a, b))
return false;
return is_array_sort(p->get_arg(0)) &&
p->get_arg(0)->get_root() == p->get_arg(1)->get_root();
}
bool theory_array_full::instantiate_parent_stores_default(theory_var v) {
SASSERT(v != null_theory_var);
@ -839,5 +928,7 @@ namespace smt {
st.update("array def as-array", m_stats.m_num_default_as_array_axiom);
st.update("array sel as-array", m_stats.m_num_select_as_array_axiom);
st.update("array def lambda", m_stats.m_num_default_lambda_axiom);
st.update("array sel lambda", m_stats.m_num_select_lambda_axiom);
st.update("array choice ax", m_stats.m_num_choice_axiom);
}
}

14
src/smt/theory_array_full.h
View file

@ -37,12 +37,15 @@ namespace smt {
ast2ast_trailmap<sort, app> m_sort2epsilon;
ast2ast_trailmap<sort, func_decl> m_sort2diag;
obj_pair_map<expr, expr, bool> m_eqs;
enode_vector m_choice_terms;
unsigned m_choice_qhead = 0;
static unsigned const m_default_map_fingerprint = UINT_MAX - 112;
static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
static unsigned const m_default_const_fingerprint = UINT_MAX - 115;
static unsigned const m_default_as_array_fingerprint = UINT_MAX - 116;
static unsigned const m_default_lambda_fingerprint = UINT_MAX - 117;
static unsigned const m_choice_fingerprint = UINT_MAX - 118;
protected:
@ -59,7 +62,7 @@ namespace smt {
bool internalize_atom(app * atom, bool gate_ctx) override;
void pop_scope_eh(unsigned num_scopes) override;
theory_var mk_var(enode * n) override;
void relevant_eh(app * n) override;
void relevant_eh(expr * n) override;
bool should_research(expr_ref_vector & unsat_core) override;
void add_theory_assumptions(expr_ref_vector & assumptions) override;
@ -80,6 +83,8 @@ namespace smt {
bool instantiate_default_map_axiom(enode* map);
bool instantiate_default_as_array_axiom(enode* arr);
bool instantiate_default_lambda_def_axiom(enode* arr);
bool instantiate_choice_axiom(enode* ch);
bool instantiate_parent_stores_default(theory_var v);
@ -87,10 +92,12 @@ namespace smt {
enode_vector m_as_array;
enode_vector m_lambdas;
bool has_non_beta_as_array();
bool is_congruent_eq(enode* p);
bool instantiate_select_const_axiom(enode* select, enode* cnst);
bool instantiate_select_as_array_axiom(enode* select, enode* arr);
bool instantiate_select_map_axiom(enode* select, enode* map);
bool instantiate_select_lambda_axiom(enode *select, enode *lambda);
bool instantiate_axiom_map_for(theory_var v);
@ -108,8 +115,9 @@ namespace smt {
void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) override;
void display_var(std::ostream & out, theory_var v) const override;
void collect_statistics(::statistics & st) const override;
bool can_propagate() override { return theory_array::can_propagate() || m_choice_qhead < m_choice_terms.size(); }
void propagate() override;
};
};
}

90
src/smt/theory_bv.cpp
View file

@ -38,7 +38,7 @@ namespace smt {
return r;
}
app * theory_bv::mk_bit2bool(app * bv, unsigned idx) {
app * theory_bv::mk_bit2bool(expr * bv, unsigned idx) {
parameter p(idx);
expr * args[1] = {bv};
return get_manager().mk_app(get_id(), OP_BIT2BOOL, 1, &p, 1, args);
@ -46,7 +46,7 @@ namespace smt {
void theory_bv::mk_bits(theory_var v) {
enode * n = get_enode(v);
app * owner = n->get_expr();
expr * owner = n->get_expr();
unsigned bv_size = get_bv_size(n);
bool is_relevant = ctx.is_relevant(n);
literal_vector & bits = m_bits[v];
@ -179,11 +179,15 @@ namespace smt {
if (params().m_bv_reflect) {
return n->get_arg(idx);
}
else {
app * arg = to_app(n->get_expr()->get_arg(idx));
else if (n->is_app()) {
app * arg = to_app(n->get_app()->get_arg(idx));
SASSERT(ctx.e_internalized(arg));
return ctx.get_enode(arg);
}
else {
UNREACHABLE();
return nullptr;
}
}
inline theory_var theory_bv::get_arg_var(enode * n, unsigned idx) {
@ -236,8 +240,8 @@ namespace smt {
TRACE(bv_diseq_axiom, tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2););
// found new disequality
m_stats.m_num_diseq_static++;
app * e1 = get_expr(v1);
app * e2 = get_expr(v2);
expr * e1 = get_expr(v1);
expr * e2 = get_expr(v2);
expr_ref eq(m.mk_eq(e1, e2), m);
literal l = ~mk_literal(eq);
std::function<expr*(void)> logfn = [&]() {
@ -438,8 +442,8 @@ namespace smt {
return;
}
++m_stats.m_num_eq_dynamic;
app* o1 = get_enode(v1)->get_expr();
app* o2 = get_enode(v2)->get_expr();
expr* o1 = get_expr(v1);
expr* o2 = get_expr(v2);
literal oeq = mk_eq(o1, o2, true);
ctx.mark_as_relevant(oeq);
@ -475,7 +479,7 @@ namespace smt {
VERIFY(get_fixed_value(v, val));
enode* n = get_enode(v);
if (ctx.watches_fixed(n)) {
expr_ref num(m_util.mk_numeral(val, n->get_expr()->get_sort()), m);
expr_ref num(m_util.mk_numeral(val, n->get_sort()), m);
literal_vector& lits = m_tmp_literals;
lits.reset();
for (literal b : m_bits[v]) {
@ -904,15 +908,15 @@ namespace smt {
case OP_BADD: internalize_add(term); return true;
case OP_BSUB: internalize_sub(term); return true;
case OP_BMUL: internalize_mul(term); return true;
case OP_BSDIV_I: internalize_sdiv(term); return true;
case OP_BSDIV_I: internalize_sdiv(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
#if ENABLE_QUOT_REM_ENCODING
case OP_BUDIV_I: internalize_udiv_quot_rem(term); return true;
case OP_BUDIV_I: internalize_udiv_quot_rem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
#else
case OP_BUDIV_I: internalize_udiv(term); return true;
case OP_BUDIV_I: internalize_udiv(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
#endif
case OP_BSREM_I: internalize_srem(term); return true;
case OP_BUREM_I: internalize_urem(term); return true;
case OP_BSMOD_I: internalize_smod(term); return true;
case OP_BSREM_I: internalize_srem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
case OP_BUREM_I: internalize_urem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
case OP_BSMOD_I: internalize_smod(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
case OP_BAND: internalize_and(term); return true;
case OP_BOR: internalize_or(term); return true;
case OP_BNOT: internalize_not(term); return true;
@ -1124,15 +1128,18 @@ namespace smt {
// Determine whether bit-vector expression should be approximated
// based on the number of bits used by the arguments.
//
bool theory_bv::approximate_term(app* n) {
bool theory_bv::approximate_term(expr *e) {
if (params().m_bv_blast_max_size == INT_MAX) {
return false;
}
if (!is_app(e))
return false;
app *n = to_app(e);
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i <= num_args; ++i) {
expr* arg = (i == num_args)?n:n->get_arg(i);
sort* s = arg->get_sort();
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) {
expr *arg = (i == num_args) ? n : n->get_arg(i);
sort *s = arg->get_sort();
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) {
if (!m_approximates_large_bvs) {
TRACE(bv, tout << "found large size bit-vector:\n" << mk_pp(n, m) << "\n";);
ctx.push_trail(value_trail<bool>(m_approximates_large_bvs));
@ -1154,7 +1161,7 @@ namespace smt {
}
void theory_bv::new_eq_eh(theory_var v1, theory_var v2) {
TRACE(bv_eq, tout << "new_eq: " << mk_pp(get_enode(v1)->get_expr(), m) << " = " << mk_pp(get_enode(v2)->get_expr(), m) << "\n";);
TRACE(bv_eq, tout << "new_eq: " << mk_pp(get_expr(v1), m) << " = " << mk_pp(get_expr(v2), m) << "\n";);
TRACE(bv, tout << "new_eq_eh v" << v1 << " = v" << v2 << " @ " << ctx.get_scope_level() <<
" relevant1: " << ctx.is_relevant(get_enode(v1)) <<
" relevant2: " << ctx.is_relevant(get_enode(v2)) << "\n";);
@ -1218,7 +1225,7 @@ namespace smt {
literal_vector & lits = m_tmp_literals;
lits.reset();
literal eq = mk_eq(get_enode(v1)->get_expr(), get_enode(v2)->get_expr(), true);
literal eq = mk_eq(get_expr(v1), get_expr(v2), true);
lits.push_back(eq);
it1 = bits1.begin();
it2 = bits2.begin();
@ -1232,7 +1239,7 @@ namespace smt {
lits.push_back(arg);
}
TRACE(bv,
tout << mk_pp(get_enode(v1)->get_expr(), m) << " = " << mk_pp(get_enode(v2)->get_expr(), m) << " "
tout << mk_pp(get_expr(v1), m) << " = " << mk_pp(get_expr(v2), m) << " "
<< ctx.get_scope_level()
<< "\n";
ctx.display_literals_smt2(tout, lits););
@ -1385,10 +1392,17 @@ namespace smt {
}
}
void theory_bv::relevant_eh(app * n) {
void theory_bv::relevant_eh(expr * n) {
TRACE(arith, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";);
TRACE(bv, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
if (ctx.relevancy() && m_util.is_bv_divrem(n)) {
ctx.mark_as_relevant(to_app(n)->get_arg(0));
ctx.mark_as_relevant(to_app(n)->get_arg(1));
assert_bv_divrem_bound_axiom(to_app(n));
}
if (m.is_bool(n)) {
if (!ctx.b_internalized(n))
return;
bool_var v = ctx.get_bool_var(n);
atom * a = get_bv2a(v);
if (a && !a->is_bit()) {
@ -1401,18 +1415,18 @@ namespace smt {
}
}
else if (params().m_bv_enable_int2bv2int && m_util.is_ubv2int(n)) {
ctx.mark_as_relevant(n->get_arg(0));
assert_bv2int_axiom(n);
ctx.mark_as_relevant(to_app(n)->get_arg(0));
assert_bv2int_axiom(to_app(n));
}
else if (params().m_bv_enable_int2bv2int && m_util.is_int2bv(n)) {
ctx.mark_as_relevant(n->get_arg(0));
assert_int2bv_axiom(n);
ctx.mark_as_relevant(to_app(n)->get_arg(0));
assert_int2bv_axiom(to_app(n));
}
#if ENABLE_QUOT_REM_ENCODING
else if (m_util.is_bv_udivi(n)) {
ctx.mark_as_relevant(n->get_arg(0));
ctx.mark_as_relevant(n->get_arg(1));
assert_udiv_quot_rem_axiom(n);
ctx.mark_as_relevant(to_app(n)->get_arg(0));
ctx.mark_as_relevant(to_app(n)->get_arg(1));
assert_udiv_quot_rem_axiom(to_app(n));
}
#endif
else if (ctx.e_internalized(n)) {
@ -2061,5 +2075,19 @@ namespace smt {
}
#endif
// Add, on the fly, the magnitude bound axioms for division/remainder operators.
// Uses the shared bv_util::mk_bv_divrem_bound clause builder so the axiom matches the
// one produced by the bv-divrem-bounds simplifier. Only fires for a symbolic divisor.
void theory_bv::assert_bv_divrem_bound_axiom(app * n) {
expr_ref_vector clause(m);
m_util.mk_bv_divrem_bound(n, clause);
if (clause.empty())
return;
literal_vector lits;
for (expr* e : clause)
lits.push_back(mk_literal(e));
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
}
};
}

13
src/smt/theory_bv.h
View file

@ -144,13 +144,13 @@ namespace smt {
unsigned get_bv_size(app const * n) const { return m_util.get_bv_size(n); }
unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_expr()); }
unsigned get_bv_size(theory_var v) const { return get_bv_size(get_enode(v)); }
bool is_bv(app const* n) const { return m_util.is_bv_sort(n->get_sort()); }
bool is_bv(expr const* n) const { return m_util.is_bv_sort(n->get_sort()); }
bool is_bv(enode const* n) const { return is_bv(n->get_expr()); }
bool is_bv(theory_var v) const { return is_bv(get_enode(v)); }
region & get_region() { return m_trail_stack.get_region(); }
bool is_numeral(theory_var v) const { return m_util.is_numeral(get_enode(v)->get_expr()); }
app * mk_bit2bool(app * bv, unsigned idx);
bool is_numeral(theory_var v) const { return m_util.is_numeral(get_expr(v)); }
app * mk_bit2bool(expr * bv, unsigned idx);
void mk_bits(theory_var v);
friend class mk_atom_trail;
void mk_bit2bool(app * n);
@ -217,7 +217,7 @@ namespace smt {
void internalize_smul_no_overflow(app *n);
void internalize_smul_no_underflow(app *n);
bool approximate_term(app* n);
bool approximate_term(expr* e);
template<bool Signed>
void internalize_le(app * atom);
@ -229,6 +229,7 @@ namespace smt {
void assert_int2bv_axiom(app* n);
void assert_bv2int_axiom(app* n);
void assert_udiv_quot_rem_axiom(app * n);
void assert_bv_divrem_bound_axiom(app * n);
protected:
@ -240,7 +241,7 @@ namespace smt {
void new_diseq_eh(theory_var v1, theory_var v2) override;
virtual void expand_diseq(theory_var v1, theory_var v2);
void assign_eh(bool_var v, bool is_true) override;
void relevant_eh(app * n) override;
void relevant_eh(expr * n) override;
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
final_check_status final_check_eh(unsigned) override;
@ -296,4 +297,4 @@ namespace smt {
bool check_invariant();
bool check_zero_one_bits(theory_var v);
};
};
}

89
src/smt/theory_datatype.cpp
View file

@ -138,7 +138,7 @@ namespace smt {
where acc_i are the accessors of constructor c.
*/
void theory_datatype::assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent) {
app* e = n->get_expr();
app* e = n->get_app();
TRACE(datatype_bug, tout << "creating axiom (= n (c (acc_1 n) ... (acc_m n))) for\n"
<< mk_pp(c, m) << " " << mk_pp(e, m) << "\n";);
m_stats.m_assert_cnstr++;
@ -171,7 +171,7 @@ namespace smt {
func_decl * d = n->get_decl();
ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(d);
SASSERT(n->get_num_args() == accessors.size());
app_ref_vector bindings(m);
expr_ref_vector bindings(m);
vector<std::tuple<enode *, enode *>> used_enodes;
used_enodes.push_back(std::make_tuple(nullptr, n));
for (unsigned i = 0; i < n->get_num_args(); ++i) {
@ -223,7 +223,7 @@ namespace smt {
void theory_datatype::assert_update_field_axioms(enode * n) {
m_stats.m_assert_update_field++;
SASSERT(is_update_field(n));
app* own = n->get_expr();
app* own = n->get_app();
expr* arg1 = own->get_arg(0);
func_decl * upd = n->get_decl();
func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast());
@ -354,6 +354,7 @@ namespace smt {
for (unsigned i = 0; i < num_args; ++i) {
enode * arg = e->get_arg(i);
sort * s = arg->get_sort();
sort *e_sort = nullptr;
if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
app_ref def(m_autil.mk_default(arg->get_expr()), m);
if (!ctx.e_internalized(def)) {
@ -361,6 +362,13 @@ namespace smt {
}
arg = ctx.get_enode(def);
}
if (m_fsutil.is_finite_set(s, e_sort) && m_util.is_datatype(e_sort)) {
app_ref def(m_fsutil.mk_empty(s), m);
if (!ctx.e_internalized(def)) {
ctx.internalize(def, false);
}
arg = ctx.get_enode(def);
}
if (!m_util.is_datatype(s) && !m_sutil.is_seq(s))
continue;
if (is_attached_to_var(arg))
@ -698,7 +706,7 @@ namespace smt {
return result;
}
void theory_datatype::relevant_eh(app * n) {
void theory_datatype::relevant_eh(expr * n) {
force_push();
TRACE(datatype, tout << "relevant_eh: " << mk_pp(n, m) << "\n";);
SASSERT(ctx.relevancy());
@ -799,8 +807,9 @@ namespace smt {
found = true;
}
sort * s = arg->get_sort();
if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
for (enode* aarg : get_array_args(arg)) {
sort *se = nullptr;
auto add_args = [&](ptr_vector<enode> const &args) {
for (enode *aarg : args) {
if (aarg->get_root() == child->get_root()) {
if (aarg != child) {
m_used_eqs.push_back(enode_pair(aarg, child));
@ -808,17 +817,16 @@ namespace smt {
found = true;
}
}
};
if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
add_args(get_array_args(arg));
}
if (m_fsutil.is_finite_set(s, se) && m_util.is_datatype(se)) {
add_args(get_finite_set_args(arg));
}
sort* se = nullptr;
if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
enode* sibling;
for (enode* aarg : get_seq_args(arg, sibling)) {
if (aarg->get_root() == child->get_root()) {
if (aarg != child)
m_used_eqs.push_back(enode_pair(aarg, child));
found = true;
}
}
enode *sibling = nullptr;
add_args(get_seq_args(arg, sibling));
if (sibling && sibling != arg)
m_used_eqs.push_back(enode_pair(arg, sibling));
@ -907,6 +915,11 @@ namespace smt {
return true;
}
}
else if (m_fsutil.is_finite_set(s, se) && m_util.is_datatype(se)) {
for (enode *aarg : get_finite_set_args(arg))
if (process_arg(aarg))
return true;
}
else if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
for (enode* aarg : get_array_args(arg))
if (process_arg(aarg))
@ -916,6 +929,33 @@ namespace smt {
return false;
}
ptr_vector<enode> const &theory_datatype::get_finite_set_args(enode *n) {
m_args.reset();
m_todo.reset();
auto add_todo = [&](enode *n) {
if (!n->is_marked()) {
n->set_mark();
m_todo.push_back(n);
}
};
add_todo(n);
for (unsigned i = 0; i < m_todo.size(); ++i) {
enode *n = m_todo[i];
expr *e = n->get_expr();
if (m_fsutil.is_singleton(e))
m_args.push_back(n->get_arg(0));
else if (m_fsutil.is_union(e))
for (auto k : enode::args(n))
add_todo(k);
}
for (enode *n : m_todo)
n->unset_mark();
return m_args;
}
ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n, enode*& sibling) {
m_args.reset();
m_todo.reset();
@ -1028,6 +1068,7 @@ namespace smt {
m_util(m),
m_autil(m),
m_sutil(m),
m_fsutil(m),
m_find(*this) {
}
@ -1096,11 +1137,23 @@ namespace smt {
};
model_value_proc * theory_datatype::mk_value(enode * n, model_generator & mg) {
auto mk_fallback = [&]() -> model_value_proc * {
app* val = to_app(m_factory->get_some_value(n->get_sort()));
TRACE(datatype,
tout << "fallback datatype value for " << pp(n, m)
<< " = " << mk_pp(val, m) << "\n";);
return alloc(expr_wrapper_proc, val);
};
theory_var v = n->get_th_var(get_id());
// Guard before using union-find: null_theory_var is not a valid index for m_find.
if (v == null_theory_var)
return mk_fallback();
v = m_find.find(v);
SASSERT(v != null_theory_var);
if (v == null_theory_var || static_cast<unsigned>(v) >= m_var_data.size() || m_var_data[v] == nullptr)
return mk_fallback();
var_data * d = m_var_data[v];
SASSERT(d->m_constructor);
if (d->m_constructor == nullptr)
return mk_fallback();
func_decl * c_decl = d->m_constructor->get_decl();
datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
for (enode* arg : enode::args(d->m_constructor))
@ -1361,4 +1414,4 @@ namespace smt {
}
};
}

19
src/smt/theory_datatype.h
View file

@ -21,6 +21,7 @@ Revision History:
#include "util/union_find.h"
#include "ast/array_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/finite_set_decl_plugin.h"
#include "ast/datatype_decl_plugin.h"
#include "model/datatype_factory.h"
#include "smt/smt_theory.h"
@ -60,23 +61,24 @@ namespace smt {
datatype_util m_util;
array_util m_autil;
seq_util m_sutil;
finite_set_util m_fsutil;
ptr_vector<var_data> m_var_data;
th_union_find m_find;
trail_stack m_trail_stack;
datatype_factory * m_factory;
stats m_stats;
bool is_constructor(app * f) const { return m_util.is_constructor(f); }
bool is_recognizer(app * f) const { return m_util.is_recognizer(f); }
bool is_subterm_predicate(app * f) const { return m_util.is_subterm_predicate(f); }
bool is_accessor(app * f) const { return m_util.is_accessor(f); }
bool is_update_field(app * f) const { return m_util.is_update_field(f); }
bool is_constructor(expr * f) const { return m_util.is_constructor(f); }
bool is_recognizer(expr * f) const { return m_util.is_recognizer(f); }
bool is_subterm_predicate(expr * f) const { return m_util.is_subterm_predicate(f); }
bool is_accessor(expr * f) const { return m_util.is_accessor(f); }
bool is_update_field(expr * f) const { return m_util.is_update_field(f); }
bool is_constructor(enode * n) const { return is_constructor(n->get_expr()); }
bool is_recognizer(enode * n) const { return is_recognizer(n->get_expr()); }
bool is_subterm_predicate(enode * n) const { return is_subterm_predicate(n->get_expr()); }
bool is_accessor(enode * n) const { return is_accessor(n->get_expr()); }
bool is_update_field(enode * n) const { return m_util.is_update_field(n->get_expr()); }
bool is_update_field(enode * n) const { return is_update_field(n->get_expr()); }
void assert_eq_axiom(enode * lhs, expr * rhs, literal antecedent);
void assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent);
@ -116,6 +118,7 @@ namespace smt {
ptr_vector<enode> m_args, m_todo;
ptr_vector<enode> const& get_array_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n, enode*& sibling);
ptr_vector<enode> const& get_finite_set_args(enode *n);
// class for managing state of final_check
class final_check_st {
@ -145,7 +148,7 @@ namespace smt {
bool use_diseqs() const override;
void new_diseq_eh(theory_var v1, theory_var v2) override;
void assign_eh(bool_var v, bool is_true) override;
void relevant_eh(app * n) override;
void relevant_eh(expr * n) override;
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
final_check_status final_check_eh(unsigned) override;
@ -212,6 +215,6 @@ namespace smt {
bool include_func_interp(func_decl* f) override;
};
};
}

2
src/smt/theory_dense_diff_logic.cpp
View file

@ -23,4 +23,4 @@ namespace smt {
template class theory_dense_diff_logic<i_ext>;
template class theory_dense_diff_logic<smi_ext>;
template class theory_dense_diff_logic<si_ext>;
};
}

2
src/smt/theory_dense_diff_logic.h
View file

@ -292,6 +292,6 @@ namespace smt {
typedef theory_dense_diff_logic<i_ext> theory_dense_i;
typedef theory_dense_diff_logic<smi_ext> theory_dense_smi;
typedef theory_dense_diff_logic<si_ext> theory_dense_si;
};
}

Some files were not shown because too many files have changed in this diff Show more