From cfa7c733db9778c4bb73ef25257960526233ba8a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Sep 2020 04:35:11 -0700 Subject: [PATCH] fixing #4670 (#4682) * fixing #4670 Signed-off-by: Nikolaj Bjorner * init Signed-off-by: Nikolaj Bjorner * arrays Signed-off-by: Nikolaj Bjorner * arrays Signed-off-by: Nikolaj Bjorner * arrays Signed-off-by: Nikolaj Bjorner * na Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.h | 6 + src/ast/datatype_decl_plugin.h | 2 +- src/ast/euf/euf_egraph.cpp | 34 +- src/ast/euf/euf_egraph.h | 2 +- src/ast/euf/euf_enode.h | 20 +- src/ast/euf/euf_etable.cpp | 16 +- src/ast/rewriter/rewriter.h | 6 +- src/muz/ddnf/ddnf.cpp | 14 +- src/muz/rel/tbv.cpp | 2 + src/muz/rel/tbv.h | 6 + src/opt/opt_context.cpp | 1 + src/opt/opt_solver.cpp | 52 ++- src/opt/opt_solver.h | 3 +- src/sat/sat_binspr.h | 2 +- src/sat/sat_cut_simplifier.cpp | 44 +-- src/sat/sat_cut_simplifier.h | 28 +- src/sat/sat_extension.h | 32 +- src/sat/sat_local_search.h | 31 +- src/sat/smt/CMakeLists.txt | 4 + src/sat/smt/array_axioms.cpp | 528 +++++++++++++++++++++++++++ src/sat/smt/array_internalize.cpp | 153 ++++++++ src/sat/smt/array_model.cpp | 77 ++++ src/sat/smt/array_solver.cpp | 220 +++++++++++ src/sat/smt/array_solver.h | 203 ++++++++++ src/sat/smt/bv_internalize.cpp | 22 +- src/sat/smt/bv_solver.cpp | 14 +- src/sat/smt/bv_solver.h | 2 +- src/sat/smt/euf_internalize.cpp | 83 ++++- src/sat/smt/euf_invariant.cpp | 4 +- src/sat/smt/euf_model.cpp | 12 +- src/sat/smt/euf_solver.cpp | 12 +- src/sat/smt/euf_solver.h | 13 +- src/sat/smt/sat_th.cpp | 19 + src/sat/smt/sat_th.h | 15 +- src/smt/mam.cpp | 6 +- src/smt/params/smt_params.cpp | 4 +- src/smt/params/theory_arith_params.h | 6 +- src/smt/smt_context.cpp | 10 +- src/smt/smt_context_inv.cpp | 16 +- src/smt/theory_arith_core.h | 4 +- src/smt/theory_array_base.cpp | 2 +- src/smt/theory_seq.cpp | 4 +- src/test/tbv.cpp | 62 ++++ src/util/dlist.h | 138 +------ src/util/hashtable.h | 4 +- src/util/obj_hashtable.h | 4 +- src/util/small_object_allocator.h | 4 +- src/util/top_sort.h | 4 +- 48 files changed, 1591 insertions(+), 359 deletions(-) create mode 100644 src/sat/smt/array_axioms.cpp create mode 100644 src/sat/smt/array_internalize.cpp create mode 100644 src/sat/smt/array_model.cpp create mode 100644 src/sat/smt/array_solver.cpp create mode 100644 src/sat/smt/array_solver.h diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index be68b87a3d3..76a88660c2c 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -161,6 +161,8 @@ class array_recognizers { bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); } bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); } bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); } + bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); } + bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); } bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); } func_decl * get_as_array_func_decl(expr * n) const; func_decl * get_as_array_func_decl(func_decl* f) const; @@ -199,6 +201,10 @@ class array_util : public array_recognizers { return mk_select(args.size(), args.c_ptr()); } + app * mk_select(ptr_buffer const& args) { + return mk_select(args.size(), args.c_ptr()); + } + app * mk_select(expr_ref_vector const& args) { return mk_select(args.size(), args.c_ptr()); } diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index ae1d38e1498..4e6983cedf5 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -53,7 +53,7 @@ namespace datatype { symbol m_name; sort_ref m_range; unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed. - constructor* m_constructor; + constructor* m_constructor{ nullptr }; public: accessor(ast_manager& m, symbol const& n, sort* range): m_name(n), diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 74c0c0b0f4c..39e97d7c2e1 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -71,7 +71,7 @@ namespace euf { } bool egraph::is_equality(enode* p) const { - return m.is_eq(p->get_owner()); + return m.is_eq(p->get_expr()); } void egraph::force_push() { @@ -112,7 +112,7 @@ namespace euf { update_children(n); } else { - SASSERT(r->get_owner() != n->get_owner()); + SASSERT(r->get_expr() != n->get_expr()); merge_justification(n, r, justification::congruence(p.second)); std::swap(n->m_next, r->m_next); n->m_root = r; @@ -191,7 +191,7 @@ namespace euf { auto undo_node = [&](enode* n) { if (n->num_args() > 1) m_table.erase(n); - m_expr2enode[n->get_owner_id()] = nullptr; + m_expr2enode[n->get_expr_id()] = nullptr; n->~enode(); m_nodes.pop_back(); m_exprs.pop_back(); @@ -243,8 +243,8 @@ namespace euf { } void egraph::merge(enode* n1, enode* n2, justification j) { - SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner())); - TRACE("euf", tout << n1->get_owner_id() << " == " << n2->get_owner_id() << "\n";); + SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr())); + TRACE("euf", tout << n1->get_expr_id() << " == " << n2->get_expr_id() << "\n";); force_push(); enode* r1 = n1->get_root(); enode* r2 = n2->get_root(); @@ -259,7 +259,7 @@ namespace euf { std::swap(r1, r2); std::swap(n1, n2); } - if ((m.is_true(r2->get_owner()) || m.is_false(r2->get_owner())) && j.is_congruence()) { + if ((m.is_true(r2->get_expr()) || m.is_false(r2->get_expr())) && j.is_congruence()) { add_literal(n1, false); } for (enode* p : enode_parents(n1)) @@ -357,10 +357,10 @@ namespace euf { explanations up to the least common ancestors. */ void egraph::push_congruence(enode* n1, enode* n2, bool comm) { - SASSERT(is_app(n1->get_owner())); + SASSERT(is_app(n1->get_expr())); SASSERT(n1->get_decl() == n2->get_decl()); if (m_used_cc) - m_used_cc(to_app(n1->get_owner()), to_app(n2->get_owner())); + m_used_cc(to_app(n1->get_expr()), to_app(n2->get_expr())); if (comm && n1->get_arg(0)->get_root() == n2->get_arg(1)->get_root() && n1->get_arg(1)->get_root() == n2->get_arg(0)->get_root()) { @@ -428,7 +428,7 @@ namespace euf { push_to_lca(a, lca); push_to_lca(b, lca); if (m_used_eq) - m_used_eq(a->get_owner(), b->get_owner(), lca->get_owner()); + m_used_eq(a->get_expr(), b->get_expr(), lca->get_expr()); explain_todo(justifications); } @@ -449,10 +449,10 @@ namespace euf { } std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const { - out << n->get_owner_id() << " := "; + out << n->get_expr_id() << " := "; if (!n->is_root()) - out << "[" << n->get_root()->get_owner_id() << "] "; - expr* f = n->get_owner(); + out << "[" << n->get_root()->get_expr_id() << "] "; + expr* f = n->get_expr(); if (is_app(f)) out << mk_bounded_pp(f, m, 1); else if (is_quantifier(f)) @@ -463,7 +463,7 @@ namespace euf { if (!n->m_parents.empty()) { out << " "; for (enode* p : enode_parents(n)) - out << p->get_owner_id() << " "; + out << p->get_expr_id() << " "; out << "\n"; } if (n->has_th_vars()) { @@ -505,7 +505,7 @@ namespace euf { SASSERT(!n1->has_th_vars()); args.reset(); for (unsigned j = 0; j < n1->num_args(); ++j) - args.push_back(old_expr2new_enode[n1->get_arg(j)->get_owner_id()]); + args.push_back(old_expr2new_enode[n1->get_arg(j)->get_expr_id()]); expr* e2 = tr(e1); enode* n2 = mk(e2, args.size(), args.c_ptr()); old_expr2new_enode.setx(e1->get_id(), n2, nullptr); @@ -514,10 +514,10 @@ namespace euf { enode* n1 = src.m_nodes[i]; enode* n1t = n1->m_target; enode* n2 = m_nodes[i]; - enode* n2t = n1t ? old_expr2new_enode[n1->get_owner_id()] : nullptr; + enode* n2t = n1t ? old_expr2new_enode[n1->get_expr_id()] : nullptr; SASSERT(!n1t || n2t); - SASSERT(!n1t || src.m.get_sort(n1->get_owner()) == src.m.get_sort(n1t->get_owner())); - SASSERT(!n1t || m.get_sort(n2->get_owner()) == m.get_sort(n2t->get_owner())); + SASSERT(!n1t || src.m.get_sort(n1->get_expr()) == src.m.get_sort(n1t->get_expr())); + SASSERT(!n1t || m.get_sort(n2->get_expr()) == m.get_sort(n2t->get_expr())); if (n1t && n2->get_root() != n2t->get_root()) merge(n2, n2t, n1->m_justification.copy(copy_justification)); } diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 63265605de5..581ddba9464 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -68,7 +68,7 @@ namespace euf { struct new_th_eq_qhead {}; struct new_lits_qhead {}; struct inconsistent {}; - enum tag_t { is_set_parent, is_add_node, is_toggle_merge, + enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq, is_new_th_eq_qhead, is_new_lits_qhead, is_inconsistent }; tag_t tag; diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index 41bab679e7d..68a2048dca4 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -36,7 +36,7 @@ namespace euf { const theory_id null_theory_id = -1; class enode { - expr* m_owner{ nullptr }; + expr* m_expr{ nullptr }; bool m_mark1 { false }; bool m_mark2 { false }; bool m_commutative { false }; @@ -69,14 +69,14 @@ namespace euf { SASSERT(num_args <= (is_app(f) ? to_app(f)->get_num_args() : 0)); void* mem = r.allocate(get_enode_size(num_args)); enode* n = new (mem) enode(); - n->m_owner = f; + n->m_expr = f; n->m_next = n; n->m_root = n; n->m_commutative = num_args == 2 && is_app(f) && to_app(f)->get_decl()->is_commutative(); n->m_num_args = num_args; n->m_merge_enabled = true; for (unsigned i = 0; i < num_args; ++i) { - SASSERT(to_app(f)->get_arg(i) == args[i]->get_owner()); + SASSERT(to_app(f)->get_arg(i) == args[i]->get_expr()); n->m_args[i] = args[i]; } return n; @@ -112,8 +112,7 @@ namespace euf { bool merge_enabled() { return m_merge_enabled; } enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; } - unsigned hash() const { return m_owner->hash(); } - func_decl* get_decl() const { return is_app(m_owner) ? to_app(m_owner)->get_decl() : nullptr; } + unsigned hash() const { return m_expr->hash(); } unsigned get_table_id() const { return m_table_id; } void set_table_id(unsigned t) { m_table_id = t; } @@ -143,9 +142,11 @@ namespace euf { unsigned class_size() const { return m_class_size; } bool is_root() const { return m_root == this; } enode* get_root() const { return m_root; } - expr* get_owner() const { return m_owner; } - unsigned get_owner_id() const { return m_owner->get_id(); } - unsigned get_root_id() const { return m_root->m_owner->get_id(); } + expr* get_expr() const { return m_expr; } + app* get_app() const { return to_app(m_expr); } + func_decl* get_decl() const { return is_app(m_expr) ? to_app(m_expr)->get_decl() : nullptr; } + unsigned get_expr_id() const { return m_expr->get_id(); } + unsigned get_root_id() const { return m_root->m_expr->get_id(); } theory_var get_th_var(theory_id id) const { return m_th_vars.find(id); } bool is_attached_to(theory_id id) const { return get_th_var(id) != null_theory_var; } bool has_th_vars() const { return !m_th_vars.empty(); } @@ -201,6 +202,7 @@ namespace euf { iterator end() const { return iterator(&n, &n); } }; + class enode_th_vars { enode& n; public: @@ -208,7 +210,7 @@ namespace euf { th_var_list* m_th_vars; public: iterator(th_var_list* n) : m_th_vars(n) {} - th_var_list operator*() { return *m_th_vars; } + th_var_list const& operator*() { return *m_th_vars; } iterator& operator++() { m_th_vars = m_th_vars->get_next(); return *this; } iterator operator++(int) { iterator tmp = *this; ++* this; return tmp; } bool operator==(iterator const& other) const { return m_th_vars == other.m_th_vars; } diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index 22c4abaf016..704c0c398f9 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -169,7 +169,7 @@ namespace euf { binary_table* tb = UNTAG(binary_table*, t); out << "b "; for (enode* n : *tb) { - out << n->get_owner_id() << " "; + out << n->get_expr_id() << " "; } out << "\n"; } @@ -178,7 +178,7 @@ namespace euf { comm_table* tb = UNTAG(comm_table*, t); out << "bc "; for (enode* n : *tb) { - out << n->get_owner_id() << " "; + out << n->get_expr_id() << " "; } out << "\n"; } @@ -187,7 +187,7 @@ namespace euf { unary_table* tb = UNTAG(unary_table*, t); out << "un "; for (enode* n : *tb) { - out << n->get_owner_id() << " "; + out << n->get_expr_id() << " "; } out << "\n"; } @@ -196,7 +196,7 @@ namespace euf { table* tb = UNTAG(table*, t); out << "nary "; for (enode* n : *tb) { - out << n->get_owner_id() << " "; + out << n->get_expr_id() << " "; } out << "\n"; } @@ -205,8 +205,8 @@ namespace euf { enode_bool_pair etable::insert(enode * n) { // it doesn't make sense to insert a constant. SASSERT(n->num_args() > 0); - SASSERT(!m_manager.is_and(n->get_owner())); - SASSERT(!m_manager.is_or(n->get_owner())); + SASSERT(!m_manager.is_and(n->get_expr())); + SASSERT(!m_manager.is_or(n->get_expr())); enode * n_prime; void * t = get_table(n); switch (static_cast(GET_TAG(t))) { @@ -215,7 +215,7 @@ namespace euf { return enode_bool_pair(n_prime, false); case BINARY: n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); - TRACE("euf", tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n"; + TRACE("euf", tout << "insert: " << n->get_expr_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_expr_id() << "\n"; display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); return enode_bool_pair(n_prime, false); case BINARY_COMM: @@ -236,7 +236,7 @@ namespace euf { UNTAG(unary_table*, t)->erase(n); break; case BINARY: - TRACE("euf", tout << "erase: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";); + TRACE("euf", tout << "erase: " << n->get_expr_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";); UNTAG(binary_table*, t)->erase(n); break; case BINARY_COMM: diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index 22ae69e8501..b9b3a7f8594 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -150,9 +150,9 @@ class var_shifter_core : public rewriter_core { - (VAR i + s2) if i < b */ class var_shifter : public var_shifter_core { - unsigned m_bound; - unsigned m_shift1; - unsigned m_shift2; + unsigned m_bound { 0 }; + unsigned m_shift1 { 0 }; + unsigned m_shift2 { 0 }; void process_var(var * v) override; public: var_shifter(ast_manager & m):var_shifter_core(m) {} diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index 26020eacfb9..2a83a65e6b1 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -453,10 +453,8 @@ namespace datalog { } void display(std::ostream& out) const { - u_map::iterator it = m_mgrs.begin(), end = m_mgrs.end(); - for (; it != end; ++it) { - it->m_value->display(out); - } + for (auto const& kv : m_mgrs) + kv.m_value->display(out); } private: @@ -558,13 +556,9 @@ namespace datalog { m_todo.reset(); m_cache.reset(); m_expr2tbv.reset(); - datalog::rule_set::iterator it = rules.begin(); - datalog::rule_set::iterator end = rules.end(); - for (; it != end; ++it) { - if (!pre_process_rule(**it)) { + for (auto* r : rules) + if (!pre_process_rule(*r)) return false; - } - } return true; } diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index a649279ee68..be85edead44 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -176,6 +176,7 @@ tbv* tbv_manager::allocate(rational const& r) { return v; } void tbv_manager::deallocate(tbv* bv) { +#if 0 DEBUG_CODE( if (!allocated_tbvs.contains(bv)) { std::cout << "double deallocate: " << bv << "\n"; @@ -185,6 +186,7 @@ void tbv_manager::deallocate(tbv* bv) { TRACE("doc", tout << "deallocate: " << bv << "\n";); } allocated_tbvs.erase(bv);); +#endif m.deallocate(bv); } void tbv_manager::copy(tbv& dst, tbv const& src) const { diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h index 5369969f4c6..a8aaea23460 100644 --- a/src/muz/rel/tbv.h +++ b/src/muz/rel/tbv.h @@ -102,6 +102,9 @@ class tbv: private fixed_bit_vector { bool operator()(tbv const& d1, tbv const& d2) const { return m.equals(d1, d2); } + bool operator()(tbv const* d1, tbv const* d2) const { + return m.equals(*d1, *d2); + } }; struct hash { @@ -110,6 +113,9 @@ class tbv: private fixed_bit_vector { unsigned operator()(tbv const& d) const { return m.hash(d); } + unsigned operator()(tbv const* d) const { + return m.hash(*d); + } }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 940dba8d501..0e6a4cf555b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -387,6 +387,7 @@ namespace opt { void context::get_model_core(model_ref& mdl) { mdl = m_model; + CTRACE("opt", mdl, tout << *mdl;); fix_model(mdl); if (mdl) mdl->set_model_completion(true); CTRACE("opt", mdl, tout << *mdl;); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index d70b5b25462..3f2e8ecfa70 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -54,7 +54,6 @@ namespace opt { } m_params.m_arith_auto_config_simplex = false; m_params.m_threads = 1; // need to interact with the solver that created model so can't have threads - m_was_sat = false; // m_params.m_auto_config = false; } @@ -85,11 +84,11 @@ namespace opt { } void opt_solver::assert_expr_core(expr * t) { + m_last_model = nullptr; if (has_quantifiers(t)) { m_params.m_relevancy_lvl = 2; } m_context.assert_expr(t); - m_was_sat = false; } void opt_solver::push_core() { @@ -182,6 +181,7 @@ namespace opt { verbose_stream().flush();); } lbool r; + m_last_model = nullptr; if (m_first && num_assumptions == 0 && m_context.get_scope_level() == 0) { r = m_context.setup_and_check(); } @@ -189,9 +189,8 @@ namespace opt { r = m_context.check(num_assumptions, assumptions); } r = adjust_result(r); - m_was_sat = r == l_true; if (r == l_true) { - m_context.get_model(m_model); + m_context.get_model(m_last_model); } m_first = false; if (dump_benchmarks()) { @@ -240,35 +239,40 @@ namespace opt { void opt_solver::maximize_objective(unsigned i, expr_ref& blocker) { smt::theory_var v = m_objective_vars[i]; bool has_shared = false; + m_last_model = nullptr; inf_eps val = get_optimizer().maximize(v, blocker, has_shared); - get_model(m_model); + m_context.get_model(m_last_model); inf_eps val2; m_valid_objectives[i] = true; has_shared = true; TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";); - if (!m_models[i]) { - set_model(i); - } + if (!m_models[i]) + m_models.set(i, m_last_model.get()); + if (!val.is_finite()) { // skip model updates } else if (m_context.get_context().update_model(has_shared)) { + m_last_model = nullptr; + m_context.get_model(m_last_model); if (has_shared && val != current_objective_value(i)) { decrement_value(i, val); + m_last_model = nullptr; if (l_true != m_context.check(0, nullptr)) throw default_exception("maximization suspended"); - m_was_sat = true; + m_context.get_model(m_last_model); } else { - set_model(i); + m_models.set(i, m_last_model.get()); } } else { + m_last_model = nullptr; SASSERT(has_shared); decrement_value(i, val); if (l_true != m_context.check(0, nullptr)) throw default_exception("maximization suspended"); - m_was_sat = true; + m_context.get_model(m_last_model); } m_objective_values[i] = val; TRACE("opt", { @@ -278,12 +282,6 @@ namespace opt { if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); }); } - void opt_solver::set_model(unsigned i) { - model_ref mdl; - get_model(mdl); - m_models.set(i, mdl.get()); - } - lbool opt_solver::decrement_value(unsigned i, inf_eps& val) { push_core(); expr_ref ge = mk_ge(i, val); @@ -291,9 +289,9 @@ namespace opt { assert_expr(ge); lbool is_sat = m_context.check(0, nullptr); is_sat = adjust_result(is_sat); - m_was_sat = is_sat == l_true; if (is_sat == l_true) { - set_model(i); + m_context.get_model(m_last_model); + m_models.set(i, m_last_model.get()); } pop_core(1); TRACE("opt", tout << is_sat << "\n";); @@ -327,14 +325,14 @@ namespace opt { } } - void opt_solver::get_model_core(model_ref & m) { - if (m_was_sat) { - m_context.get_model(m); - if (!m) m = m_model; else m_model = m; - } - else { - m = nullptr; - } + void opt_solver::get_model_core(model_ref & m) { + for (auto* mdl : m_models) { + if (mdl) { + m = mdl; + return; + } + } + m = m_last_model.get(); } proof * opt_solver::get_proof() { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index b6b35dd3cc0..a7951a50bd0 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -72,8 +72,7 @@ namespace opt { generic_model_converter& m_fm; progress_callback * m_callback; symbol m_logic; - model_ref m_model; - bool m_was_sat; + model_ref m_last_model; svector m_objective_vars; vector m_objective_values; sref_vector m_models; diff --git a/src/sat/sat_binspr.h b/src/sat/sat_binspr.h index 5b4f9a0d091..874d8687fbb 100644 --- a/src/sat/sat_binspr.h +++ b/src/sat/sat_binspr.h @@ -71,7 +71,7 @@ namespace sat { void collect_candidates(literal lit, literal const* begin, literal const* end); void strengthen_clause(literal lit, literal const* begin, literal const* end); - bool_var m_p, m_q, m_u, m_v; + bool_var m_p{ 0 }, m_q{ 0 }, m_u{ 0 }, m_v{ 0 }; lbool m_vals[4]; void algorithm2(); diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp index bc6d9871fc5..74e11a04065 100644 --- a/src/sat/sat_cut_simplifier.cpp +++ b/src/sat/sat_cut_simplifier.cpp @@ -460,7 +460,7 @@ namespace sat { return; } bin_rel q, p(~u, v); - if (m_bins.find(p, q) && q.op != none) + if (m_bins.find(p, q) && q.op != op_code::none) return; if (big.connected(u, v)) return; @@ -614,20 +614,16 @@ namespace sat { */ void cut_simplifier::cuts2bins(vector const& cuts) { svector dcs; - for (auto const& p : m_bins) { - if (p.op != none) - dcs.push_back(p); - } + for (auto const& p : m_bins) + if (p.op != op_code::none) + dcs.push_back(p); m_bins.reset(); - for (auto const& cs : cuts) { - for (auto const& c : cs) { - for (unsigned i = c.size(); i-- > 0; ) { - for (unsigned j = i; j-- > 0; ) { + for (auto const& cs : cuts) + for (auto const& c : cs) + for (unsigned i = c.size(); i-- > 0; ) + for (unsigned j = i; j-- > 0; ) m_bins.insert(bin_rel(c[j],c[i])); - } - } - } - } + // don't lose previous don't cares for (auto const& p : dcs) { if (m_bins.contains(p)) { @@ -646,27 +642,27 @@ namespace sat { big b(s.rand()); b.init(s, true); for (auto& p : m_bins) { - if (p.op != none) continue; + if (p.op != op_code::none) continue; literal u(p.u, false), v(p.v, false); // u -> v, then u & ~v is impossible if (b.connected(u, v)) { - p.op = pn; + p.op = op_code::pn; } else if (b.connected(u, ~v)) { - p.op = pp; + p.op = op_code::pp; } else if (b.connected(~u, v)) { - p.op = nn; + p.op = op_code::nn; } else if (b.connected(~u, ~v)) { - p.op = np; + p.op = op_code::np; } - if (p.op != none) { + if (p.op != op_code::none) { track_binary(p); } } IF_VERBOSE(2, { - unsigned n = 0; for (auto const& p : m_bins) if (p.op != none) ++n; + unsigned n = 0; for (auto const& p : m_bins) if (p.op != op_code::none) ++n; verbose_stream() << n << " / " << m_bins.size() << " don't cares\n"; }); } @@ -698,10 +694,10 @@ namespace sat { */ uint64_t cut_simplifier::op2dont_care(unsigned i, unsigned j, bin_rel const& p) { SASSERT(i < j && j < 6); - if (p.op == none) return 0ull; + if (p.op == op_code::none) return 0ull; // first position of mask is offset into output bits contributed by i and j - bool i_is_0 = (p.op == np || p.op == nn); - bool j_is_0 = (p.op == pn || p.op == nn); + bool i_is_0 = (p.op == op_code::np || p.op == op_code::nn); + bool j_is_0 = (p.op == op_code::pn || p.op == op_code::nn); uint64_t first = (i_is_0 ? 0 : (1 << i)) + (j_is_0 ? 0 : (1 << j)); uint64_t inc = 1ull << (j + 1); uint64_t r = 1ull << first; @@ -719,7 +715,7 @@ namespace sat { for (unsigned i = 0; i < c.size(); ++i) { for (unsigned j = i + 1; j < c.size(); ++j) { bin_rel p(c[i], c[j]); - if (m_bins.find(p, p) && p.op != none) { + if (m_bins.find(p, p) && p.op != op_code::none) { dc |= op2dont_care(i, j, p); } } diff --git a/src/sat/sat_cut_simplifier.h b/src/sat/sat_cut_simplifier.h index 144051ffdc5..aae5d4cfe46 100644 --- a/src/sat/sat_cut_simplifier.h +++ b/src/sat/sat_cut_simplifier.h @@ -68,27 +68,27 @@ namespace sat { * */ - enum op_code { pp, pn, np, nn, none }; + enum class op_code { pp, pn, np, nn, none }; struct bin_rel { unsigned u, v; op_code op; - bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(none) { + bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(op_code::none) { if (u > v) std::swap(u, v); } // convert binary clause into a bin-rel - bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(none) { - if (_u.sign() && _v.sign()) op = pp; - else if (_u.sign()) op = pn; - else if (_v.sign()) op = np; - else op = nn; + bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(op_code::none) { + if (_u.sign() && _v.sign()) op = op_code::pp; + else if (_u.sign()) op = op_code::pn; + else if (_v.sign()) op = op_code::np; + else op = op_code::nn; if (u > v) { std::swap(u, v); - if (op == np) op = pn; - else if (op == pn) op = np; + if (op == op_code::np) op = op_code::pn; + else if (op == op_code::pn) op = op_code::np; } } - bin_rel(): u(UINT_MAX), v(UINT_MAX), op(none) {} + bin_rel(): u(UINT_MAX), v(UINT_MAX), op(op_code::none) {} struct hash { unsigned operator()(bin_rel const& p) const { @@ -102,10 +102,10 @@ namespace sat { }; void to_binary(literal& lu, literal& lv) const { switch (op) { - case pp: lu = literal(u, true); lv = literal(v, true); break; - case pn: lu = literal(u, true); lv = literal(v, false); break; - case np: lu = literal(u, false); lv = literal(v, true); break; - case nn: lu = literal(u, false); lv = literal(v, false); break; + case op_code::pp: lu = literal(u, true); lv = literal(v, true); break; + case op_code::pn: lu = literal(u, true); lv = literal(v, false); break; + case op_code::np: lu = literal(u, false); lv = literal(v, true); break; + case op_code::nn: lu = literal(u, false); lv = literal(v, false); break; default: UNREACHABLE(); break; } } diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index e248ddbef2d..6db3816f0b8 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -58,40 +58,40 @@ namespace sat { virtual ~extension() {} virtual unsigned get_id() const { return 0; } virtual void set_solver(solver* s) = 0; - virtual void set_lookahead(lookahead* s) = 0; + virtual void set_lookahead(lookahead* s) {}; virtual void init_search() {} virtual bool propagate(literal l, ext_constraint_idx idx) = 0; virtual bool unit_propagate() = 0; virtual bool is_external(bool_var v) = 0; - virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0; + virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const { return 0; } virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) = 0; - virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0; + virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) { return false; } virtual void asserted(literal l) = 0; virtual check_result check() = 0; virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma virtual void push() = 0; void push_scopes(unsigned n) { for (unsigned i = 0; i < n; ++i) push(); } virtual void pop(unsigned n) = 0; - virtual void pre_simplify() = 0; - virtual void simplify() = 0; + virtual void pre_simplify() {} + virtual void simplify() {} // have a way to replace l by r in all constraints virtual bool set_root(literal l, literal r) { return false; } virtual void flush_roots() {} - virtual void clauses_modifed() = 0; - virtual lbool get_phase(bool_var v) = 0; + virtual void clauses_modifed() {} + virtual lbool get_phase(bool_var v) { return l_undef; } virtual std::ostream& display(std::ostream& out) const = 0; virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0; virtual std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const = 0; virtual void collect_statistics(statistics& st) const = 0; - virtual extension* copy(solver* s) = 0; - virtual void find_mutexes(literal_vector& lits, vector & mutexes) = 0; - virtual void gc() = 0; - virtual void pop_reinit() = 0; - virtual bool validate() = 0; - virtual void init_use_list(ext_use_list& ul) = 0; - virtual bool is_blocked(literal l, ext_constraint_idx) = 0; - virtual bool check_model(model const& m) const = 0; - virtual unsigned max_var(unsigned w) const = 0; + virtual extension* copy(solver* s) { UNREACHABLE(); return nullptr; } + virtual void find_mutexes(literal_vector& lits, vector & mutexes) {} + virtual void gc() {} + virtual void pop_reinit() {} + virtual bool validate() { return true; } + virtual void init_use_list(ext_use_list& ul) {} + virtual bool is_blocked(literal l, ext_constraint_idx) { return false; } + virtual bool check_model(model const& m) const { return true; } + virtual unsigned max_var(unsigned w) const { return w; } virtual bool extract_pb(std::function& card, std::function& pb) { diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index a8fb7829a7a..e48d889248f 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -88,33 +88,24 @@ namespace sat { }; struct var_info { - bool m_value; // current solution - unsigned m_bias; // bias for current solution in percentage. + bool m_value{ true }; // current solution + unsigned m_bias{ 50 }; // bias for current solution in percentage. // if bias is 0, then value is always false, if 100, then always true - bool m_unit; // is this a unit literal + bool m_unit{ false }; // is this a unit literal literal m_explain; // explanation for unit assignment - bool m_conf_change; // whether its configure changes since its last flip - bool m_in_goodvar_stack; - int m_score; - int m_slack_score; - int m_time_stamp; // the flip time stamp + bool m_conf_change{ true }; // whether its configure changes since its last flip + bool m_in_goodvar_stack{ false }; + int m_score{ 0 }; + int m_slack_score{ 0 }; + int m_time_stamp{ 0 }; // the flip time stamp bool_var_vector m_neighbors; // neighborhood variables coeff_vector m_watch[2]; literal_vector m_bin[2]; - unsigned m_flips; + unsigned m_flips{ 0 }; ema m_slow_break; - double m_break_prob; + double m_break_prob{ 0 }; var_info(): - m_value(true), - m_bias(50), - m_unit(false), - m_conf_change(true), - m_in_goodvar_stack(false), - m_score(0), - m_slack_score(0), - m_flips(0), - m_slow_break(1e-5), - m_break_prob(0) + m_slow_break(1e-5) {} }; diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 6555749d963..775a3518631 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -1,5 +1,9 @@ z3_add_component(sat_smt SOURCES + array_axioms.cpp + array_internalize.cpp + array_model.cpp + array_solver.cpp atom2bool_var.cpp ba_internalize.cpp ba_solver.cpp diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp new file mode 100644 index 00000000000..21326764e9b --- /dev/null +++ b/src/sat/smt/array_axioms.cpp @@ -0,0 +1,528 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + array_axioms.cpp + +Abstract: + + Routines for instantiating array axioms + +Author: + + Nikolaj Bjorner (nbjorner) 2020-09-08 + +--*/ + +#include "ast/ast_trail.h" +#include "ast/ast_ll_pp.h" +#include "sat/smt/array_solver.h" +#include "sat/smt/euf_solver.h" + +namespace array { + + void solver::push_axiom(axiom_record const& r) { + unsigned idx = m_axiom_trail.size(); + m_axiom_trail.push_back(r); + if (m_axioms.contains(idx)) + m_axiom_trail.pop_back(); + } + + bool solver::assert_axiom(unsigned idx) { + axiom_record const& r = m_axiom_trail[idx]; + if (m_axioms.contains(idx)) + return false; + m_axioms.insert(idx); + ctx.push(insert_map(m_axioms, idx)); + expr* child = r.n->get_expr(); + app* select; + switch (r.m_kind) { + case axiom_record::kind_t::is_store: + return assert_store_axiom(to_app(child)); + case axiom_record::kind_t::is_select: + select = r.select->get_app(); + SASSERT(a.is_select(select)); + if (a.is_const(child)) + return assert_select_const_axiom(select, to_app(child)); + else if (a.is_as_array(child)) + return assert_select_as_array_axiom(select, to_app(child)); + else if (a.is_store(child)) + return assert_select_store_axiom(select, to_app(child)); + else if (a.is_map(child)) + return assert_select_map_axiom(select, to_app(child)); + else if (is_lambda(child)) + return assert_select_lambda_axiom(select, child); + else + UNREACHABLE(); + break; + case axiom_record::kind_t::is_default: + if (a.is_const(child)) + return assert_default_const_axiom(to_app(child)); + else if (a.is_store(child)) + return assert_default_store_axiom(to_app(child)); + else if (a.is_map(child)) + return assert_default_map_axiom(to_app(child)); + else if (a.is_as_array(child)) + return assert_default_as_array_axiom(to_app(child)); + else + UNREACHABLE(); + break; + case axiom_record::kind_t::is_extensionality: + return assert_extensionality(r.n->get_arg(0)->get_expr(), r.n->get_arg(1)->get_expr()); + case axiom_record::kind_t::is_congruence: + return assert_congruent_axiom(child, r.select->get_expr()); + default: + UNREACHABLE(); + break; + } + return false; + } + + /** + * Assert + * select(n, i) = v + * Where + * n := store(a, i, v) + */ + bool solver::assert_store_axiom(app* e) { + m_stats.m_num_store_axiom++; + SASSERT(a.is_store(e)); + unsigned num_args = e->get_num_args(); + ptr_vector sel_args(num_args - 1, e->get_args()); + sel_args[0] = e; + expr_ref sel(a.mk_select(sel_args), m); + euf::enode* n1 = e_internalize(sel); + euf::enode* n2 = expr2enode(e->get_arg(num_args - 1)); + return ctx.propagate(n1, n2, array_axiom()); + } + + + /** + * Assert + * i_k = j_k or select(store(a, i, v), j) = select(a, j) + * where i = (i_1, ..., i_n), j = (j_1, .., j_n), k in 1..n + */ + bool solver::assert_select_store_axiom(app* select, app* store) { + m_stats.m_num_select_store_axiom++; + SASSERT(a.is_store(store)); + SASSERT(a.is_select(select)); + SASSERT(store->get_num_args() == 1 + select->get_num_args()); + ptr_buffer sel1_args, sel2_args; + unsigned num_args = select->get_num_args(); + sel1_args.push_back(store); + sel2_args.push_back(store->get_arg(0)); + + for (unsigned i = 1; i < num_args; i++) { + sel1_args.push_back(select->get_arg(i)); + sel2_args.push_back(select->get_arg(i)); + } + + expr_ref sel1(a.mk_select(sel1_args), m); + expr_ref sel2(a.mk_select(sel2_args), m); + expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m); + euf::enode* s1 = e_internalize(sel1); + euf::enode* s2 = e_internalize(sel2); + if (s1->get_root() == s2->get_root()) + return false; + sat::literal sel_eq = b_internalize(sel_eq_e); + + for (unsigned i = 1; i < num_args; i++) { + expr* idx1 = store->get_arg(i); + expr* idx2 = select->get_arg(i); + euf::enode* r1 = expr2enode(idx1)->get_root(); + euf::enode* r2 = expr2enode(idx2)->get_root(); + if (r1 == r2) + continue; + if (m.are_distinct(r1->get_expr(), r2->get_expr())) { + add_clause(sel_eq); + break; + } + sat::literal idx_eq = b_internalize(m.mk_eq(idx1, idx2)); + add_clause(idx_eq, sel_eq); + } + return true; + } + + /** + * Assert + * select(const(v), i) = v + */ + bool solver::assert_select_const_axiom(app* select, app* cnst) { + m_stats.m_num_select_const_axiom++; + expr* val = nullptr; + VERIFY(a.is_const(cnst, val)); + SASSERT(a.is_select(select)); + unsigned num_args = select->get_num_args(); + ptr_vector sel_args(num_args, select->get_args()); + sel_args[0] = cnst; + expr_ref sel(a.mk_select(sel_args), m); + euf::enode* n1 = e_internalize(sel); + euf::enode* n2 = expr2enode(val); + return ctx.propagate(n1, n2, array_axiom()); + } + + + /** + * e1 = e2 or select(e1, diff(e1,e2)) != select(e2, diff(e1, e2)) + */ + bool solver::assert_extensionality(expr* e1, expr* e2) { + m_stats.m_num_extensionality_axiom++; + func_decl_ref_vector* funcs = nullptr; + VERIFY(m_sort2diff.find(m.get_sort(e1), funcs)); + expr_ref_vector args1(m), args2(m); + args1.push_back(e1); + args2.push_back(e2); + for (func_decl* f : *funcs) { + expr* k = m.mk_app(f, e1, e2); + args1.push_back(k); + args2.push_back(k); + } + expr_ref sel1(a.mk_select(args1), m); + expr_ref sel2(a.mk_select(args2), m); + expr_ref n1_eq_n2(m.mk_eq(e1, e2), m); + expr_ref sel1_eq_sel2(m.mk_eq(sel1, sel2), m); + literal lit1 = b_internalize(n1_eq_n2); + literal lit2 = b_internalize(sel1_eq_sel2); + if (s().value(lit1) == l_true || s().value(lit2) == l_false) + return false; + add_clause(lit1, ~lit2); + return true; + } + + /** + * Assert axiom: + * select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i)) + */ + bool solver::assert_select_map_axiom(app* select, app* map) { + m_stats.m_num_select_map_axiom++; + SASSERT(a.is_map(map)); + SASSERT(a.is_select(select)); + SASSERT(map->get_num_args() > 0); + func_decl* f = a.get_map_func_decl(map); + + TRACE("array", + tout << mk_bounded_pp(map, m) << "\n"; + tout << mk_bounded_pp(select, m) << "\n";); + unsigned num_args = select->get_num_args(); + unsigned num_arrays = map->get_num_args(); + ptr_buffer args1, args2; + vector > args2l; + args1.push_back(map); + for (expr* ar : *map) { + ptr_vector arg; + arg.push_back(ar); + args2l.push_back(arg); + } + for (unsigned i = 1; i < num_args; ++i) { + expr* arg = select->get_arg(i); + for (auto& args : args2l) + args.push_back(arg); + args1.push_back(arg); + } + for (auto const& args : args2l) + args2.push_back(a.mk_select(args)); + + expr_ref sel1(m), sel2(m); + sel1 = a.mk_select(args1); + sel2 = m.mk_app(f, args2); + rewrite(sel2); + euf::enode* n1 = e_internalize(sel1); + euf::enode* n2 = e_internalize(sel2); + return ctx.propagate(n1, n2, array_axiom()); + } + + + /** + * Assert axiom: + * select(as-array f, i_1, ..., i_n) = (f i_1 ... i_n) + */ + bool solver::assert_select_as_array_axiom(app* select, app* arr) { + m_stats.m_num_select_as_array_axiom++; + SASSERT(a.is_as_array(arr)); + SASSERT(a.is_select(select)); + unsigned num_args = select->get_num_args(); + func_decl* f = a.get_as_array_func_decl(arr); + ptr_vector sel_args(num_args, select->get_args()); + sel_args[0] = arr; + expr_ref sel(a.mk_select(sel_args), m); + expr_ref val(m.mk_app(f, sel_args.size() - 1, sel_args.c_ptr() + 1), m); + euf::enode* n1 = e_internalize(sel); + euf::enode* n2 = e_internalize(val); + return ctx.propagate(n1, n2, array_axiom()); + } + + /** + * Assert: + * default(map[f](a,..,d)) = f(default(a),..,default(d)) + */ + bool solver::assert_default_map_axiom(app* map) { + m_stats.m_num_default_map_axiom++; + SASSERT(a.is_map(map)); + func_decl* f = a.get_map_func_decl(map); + SASSERT(map->get_num_args() == f->get_arity()); + ptr_buffer args2; + for (expr* arg : *map) + args2.push_back(a.mk_default(arg)); + + expr_ref def1(a.mk_default(map), m); + expr_ref def2(m.mk_app(f, args2), m); + rewrite(def2); + return ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()); + } + + + /** + * Assert: + * default(const(e)) = e + */ + bool solver::assert_default_const_axiom(app* cnst) { + m_stats.m_num_default_const_axiom++; + expr* val = nullptr; + VERIFY(a.is_const(cnst, val)); + TRACE("array", tout << mk_bounded_pp(cnst, m) << "\n";); + expr_ref def(a.mk_default(cnst), m); + return ctx.propagate(expr2enode(val), e_internalize(def), array_axiom()); + } + + bool solver::assert_default_as_array_axiom(app* as_array) { + // no-op + return false; + } + + + /** + * let n := store(a, i, v) + * Assert: + * - when sort(n) has exactly one element: + * default(n) = v + * - for small domains: + * default(n) = ite(epsilon1 = i, v, default(a)) + n[diag(i)] = a[diag(i)] + * - for large domains: + * default(n) = default(a) + */ + bool solver::assert_default_store_axiom(app* store) { + m_stats.m_num_default_store_axiom++; + SASSERT(a.is_store(store)); + SASSERT(store->get_num_args() >= 3); + expr_ref def1(m), def2(m); + bool prop = false; + + unsigned num_args = store->get_num_args(); + + def1 = a.mk_default(store); + def2 = a.mk_default(store->get_arg(0)); + + bool is_new = false; + + if (has_unitary_domain(store)) { + def2 = store->get_arg(num_args - 1); + } + else if (!has_large_domain(store)) { + // + // let A = store(B, i, v) + // + // Add: + // default(A) = ite(epsilon1 = i, v, default(B)) + // A[diag(i)] = B[diag(i)] + // + expr_ref_vector eqs(m); + expr_ref_vector args1(m), args2(m); + args1.push_back(store->get_arg(0)); + args2.push_back(store); + + for (unsigned i = 1; i + 1 < num_args; ++i) { + expr* arg = store->get_arg(i); + sort* srt = m.get_sort(arg); + auto ep = mk_epsilon(srt); + eqs.push_back(m.mk_eq(ep.first, arg)); + args1.push_back(m.mk_app(ep.second, arg)); + args2.push_back(m.mk_app(ep.second, arg)); + } + expr_ref eq(m.mk_and(eqs), m); + def2 = m.mk_ite(eq, store->get_arg(num_args - 1), def2); + app_ref sel1(m), sel2(m); + sel1 = a.mk_select(args1); + sel2 = a.mk_select(args2); + if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom())) + prop = true; + } + if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom())) + prop = true; + return prop; + } + + /** + * Assert select(lambda xs . M, N1,.., Nk) -> M[N1/x1, ..., Nk/xk] + */ + bool solver::assert_select_lambda_axiom(app* select, expr* lambda) { + SASSERT(is_lambda(lambda)); + SASSERT(a.is_select(select)); + SASSERT(m.get_sort(lambda) == m.get_sort(select->get_arg(0))); + ptr_vector args(select->get_num_args(), select->get_args()); + args[0] = lambda; + expr_ref alpha(a.mk_select(args), m); + expr_ref beta(alpha); + rewrite(beta); + return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom()); + } + + /** + \brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars) + */ + bool solver::assert_congruent_axiom(expr* e1, expr* e2) { + ++m_stats.m_num_congruence_axiom; + sort* s = m.get_sort(e1); + unsigned dimension = get_array_arity(s); + expr_ref n1_eq_n2(m.mk_eq(e1, e2), m); + expr_ref_vector args1(m), args2(m); + args1.push_back(e1); + args2.push_back(e2); + svector names; + sort_ref_vector sorts(m); + for (unsigned i = 0; i < dimension; i++) { + sort * srt = get_array_domain(s, i); + sorts.push_back(srt); + names.push_back(symbol(i)); + expr * k = m.mk_var(dimension - i - 1, srt); + args1.push_back(k); + args2.push_back(k); + } + expr * sel1 = a.mk_select(dimension+1, args1.c_ptr()); + expr * sel2 = a.mk_select(dimension+1, args2.c_ptr()); + expr * eq = m.mk_eq(sel1, sel2); + expr_ref q(m.mk_forall(dimension, sorts.c_ptr(), names.c_ptr(), eq), m); + rewrite(q); + sat::literal fa_eq = b_internalize(q); + add_clause(~b_internalize(n1_eq_n2), fa_eq); + return true; + } + + bool solver::has_unitary_domain(app* array_term) { + SASSERT(a.is_array(array_term)); + sort* s = m.get_sort(array_term); + unsigned dim = get_array_arity(s); + for (unsigned i = 0; i < dim; ++i) { + sort* d = get_array_domain(s, i); + if (d->is_infinite() || d->is_very_big() || 1 != d->get_num_elements().size()) + return false; + } + return true; + } + + bool solver::has_large_domain(app* array_term) { + SASSERT(a.is_array(array_term)); + sort* s = m.get_sort(array_term); + unsigned dim = get_array_arity(s); + rational sz(1); + for (unsigned i = 0; i < dim; ++i) { + sort* d = get_array_domain(s, i); + if (d->is_infinite() || d->is_very_big()) { + return true; + } + sz *= rational(d->get_num_elements().size(), rational::ui64()); + if (sz >= rational(1 << 14)) { + return true; + } + } + return false; + } + + + std::pair solver::mk_epsilon(sort* s) { + app* eps = nullptr; + func_decl* diag = nullptr; + if (!m_sort2epsilon.find(s, eps)) { + eps = m.mk_fresh_const("epsilon", s); + ctx.push(ast2ast_trail(m_sort2epsilon, s, eps)); + } + if (!m_sort2diag.find(s, diag)) { + diag = m.mk_fresh_func_decl("diag", 1, &s, s); + ctx.push(ast2ast_trail(m_sort2diag, s, diag)); + } + return std::make_pair(eps, diag); + } + + void solver::push_parent_select_store_axioms(theory_var v) { + expr* e = var2expr(v); + if (!a.is_array(e)) + return; + auto& d = get_var_data(v); + for (euf::enode* store : d.m_parents) + if (a.is_store(store->get_expr())) + for (euf::enode* sel : d.m_parents) + if (a.is_select(sel->get_expr())) + push_axiom(select_axiom(sel, store)); + } + + bool solver::add_delayed_axioms() { + if (!get_config().m_array_delay_exp_axiom) + return false; + unsigned num_vars = get_num_vars(); + for (unsigned v = 0; v < num_vars; v++) + push_parent_select_store_axioms(v); + return unit_propagate(); + } + + bool solver::add_interface_equalities() { + sbuffer roots; + collect_shared_vars(roots); + bool prop = false; + for (unsigned i = roots.size(); i-- > 0; ) { + theory_var v1 = roots[i]; + euf::enode* n1 = var2enode(v1); + for (unsigned j = i; j-- > 0; ) { + theory_var v2 = roots[j]; + euf::enode* n2 = var2enode(v2); + if (m.get_sort(n1->get_expr()) != m.get_sort(n2->get_expr())) + continue; + expr_ref eq(m.mk_eq(n1->get_expr(), n2->get_expr()), m); + sat::literal lit = b_internalize(eq); + if (s().value(lit) == l_undef) + prop = true; + } + } + return prop; + } + + void solver::collect_shared_vars(sbuffer& roots) { + ptr_buffer to_unmark; + unsigned num_vars = get_num_vars(); + for (unsigned i = 0; i < num_vars; i++) { + euf::enode * n = var2enode(i); + if (!a.is_array(n->get_expr())) { + continue; + } + euf::enode * r = n->get_root(); + if (r->is_marked1()) { + continue; + } + // arrays used as indices in other arrays have to be treated as shared. + // issue #3532, #3529 + // + if (ctx.is_shared(r) || is_select_arg(r)) { + TRACE("array", tout << "new shared var: #" << r->get_expr_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != euf::null_theory_var); + roots.push_back(r_th_var); + } + r->mark1(); + to_unmark.push_back(r); + } + TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(roots.size(), (unsigned*)roots.c_ptr()) << "\n";); + for (auto* n : to_unmark) + n->unmark1(); + } + + bool solver::is_select_arg(euf::enode* r) { + for (euf::enode* n : euf::enode_parents(r)) + if (a.is_select(n->get_expr())) + for (unsigned i = 1; i < n->num_args(); ++i) + if (r == n->get_arg(i)->get_root()) + return true; + return false; + } + +} + diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp new file mode 100644 index 00000000000..5006537af2c --- /dev/null +++ b/src/sat/smt/array_internalize.cpp @@ -0,0 +1,153 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + array_internalize.cpp + +Abstract: + + Internalize routines for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2020-09-08 + +--*/ + +#include "sat/smt/array_solver.h" +#include "sat/smt/euf_solver.h" + +namespace array { + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + // TODO + return sat::null_literal; + } + + void solver::internalize(expr* e, bool redundant) { + // TODO + } + + euf::theory_var solver::mk_var(euf::enode* n) { + theory_var r = euf::th_euf_solver::mk_var(n); + m_find.mk_var(); + ctx.attach_th_var(n, this, r); + m_var_data.push_back(alloc(var_data)); + return r; + } + + void solver::ensure_var(euf::enode* n) { + theory_var v = n->get_th_var(get_id()); + if (v == euf::null_theory_var) + mk_var(n); + } + + void solver::apply_sort_cnstr(euf::enode * n, sort * s) { + ensure_var(n); + } + + void solver::internalize_store(euf::enode* n) { + if (get_config().m_array_laziness == 0) + add_parent(n->get_arg(0), n); + push_axiom(store_axiom(n)); + } + + void solver::internalize_select(euf::enode* n) { + if (get_config().m_array_laziness == 0) + add_parent(n->get_arg(0), n); + } + + void solver::internalize_const(euf::enode* n) { + push_axiom(default_axiom(n)); + set_prop_upward(n); + } + + void solver::internalize_ext(euf::enode* n) { + push_axiom(extensionality_axiom(n)); + } + + void solver::internalize_default(euf::enode* n) { + add_parent(n->get_arg(0), n); + set_prop_upward(n); + } + + void solver::internalize_map(euf::enode* n) { + for (auto* arg : euf::enode_args(n)) { + add_parent(arg, n); + set_prop_upward(arg); + } + push_axiom(default_axiom(n)); + } + + void solver::internalize_as_array(euf::enode* n) { + // TBD: delay verdict whether model is undetermined + ctx.unhandled_function(n->get_decl()); + push_axiom(default_axiom(n)); + } + + bool solver::visited(expr* e) { + euf::enode* n = expr2enode(e); + return n && n->is_attached_to(get_id()); + } + + bool solver::visit(expr* e) { + if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { + ctx.internalize(e, m_is_redundant); + ensure_var(expr2enode(e)); + return true; + } + m_stack.push_back(sat::eframe(e)); + return false; + } + + bool solver::post_visit(expr* e, bool sign, bool root) { + euf::enode* n = expr2enode(e); + app* a = to_app(e); + SASSERT(!n || !n->is_attached_to(get_id())); + if (!n) + n = mk_enode(e, false); + SASSERT(!n->is_attached_to(get_id())); + theory_var v = mk_var(n); + for (auto* arg : euf::enode_args(n)) + ensure_var(arg); + switch (a->get_decl_kind()) { + case OP_STORE: + internalize_store(n); + break; + case OP_SELECT: + internalize_select(n); + break; + case OP_CONST_ARRAY: + internalize_const(n); + break; + case OP_ARRAY_EXT: + internalize_ext(n); + break; + case OP_ARRAY_DEFAULT: + internalize_default(n); + break; + case OP_ARRAY_MAP: + internalize_map(n); + break; + case OP_AS_ARRAY: + internalize_as_array(n); + break; + case OP_SET_UNION: + case OP_SET_INTERSECT: + case OP_SET_DIFFERENCE: + case OP_SET_COMPLEMENT: + case OP_SET_SUBSET: + case OP_SET_HAS_SIZE: + case OP_SET_CARD: + ctx.unhandled_function(a->get_decl()); + break; + default: + UNREACHABLE(); + break; + } + return true; + } + +} + diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp new file mode 100644 index 00000000000..7e18dfa7ff6 --- /dev/null +++ b/src/sat/smt/array_model.cpp @@ -0,0 +1,77 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + array_model.cpp + +Abstract: + + Theory plugin for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2020-09-08 + +--*/ + +#include "ast/ast_ll_pp.h" +#include "model/array_factory.h" +#include "sat/smt/array_solver.h" +#include "sat/smt/euf_solver.h" + +namespace array { + + + void solver::add_dep(euf::enode* n, top_sort& dep) { + if (!a.is_array(n->get_expr())) { + dep.insert(n, nullptr); + return; + } + for (euf::enode* p : euf::enode_parents(n)) { + if (!a.is_select(p->get_expr())) + continue; + dep.add(n, p); + for (unsigned i = 1; i < p->num_args(); ++i) + dep.add(n, p->get_arg(i)); + } + for (euf::enode* k : euf::enode_class(n)) + if (a.is_const(k->get_expr())) + dep.add(n, k); + else if (a.is_default(k->get_expr())) + dep.add(n, k); + } + + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + SASSERT(a.is_array(n->get_expr())); + ptr_vector args; + sort* srt = m.get_sort(n->get_expr()); + unsigned arity = get_array_arity(srt); + func_decl * f = mk_aux_decl_for_array_sort(m, srt); + func_interp * fi = alloc(func_interp, m, arity); + mdl.register_decl(f, fi); + + for (euf::enode* p : euf::enode_parents(n)) { + if (!a.is_select(p->get_expr())) + continue; + args.reset(); + for (unsigned i = 1; i < p->num_args(); ++i) + args.push_back(values.get(p->get_arg(i)->get_root_id())); + expr* value = values.get(p->get_root_id()); + fi->insert_entry(args.c_ptr(), value); + } + if (!fi->get_else()) + for (euf::enode* k : euf::enode_class(n)) + if (a.is_const(k->get_expr())) + fi->set_else(k->get_arg(0)->get_root()->get_expr()); + if (!fi->get_else()) + for (euf::enode* k : euf::enode_parents(n)) + if (a.is_default(k->get_expr())) + fi->set_else(k->get_root()->get_expr()); + + parameter p(f); + values.set(n->get_root_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p)); + } + +} diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp new file mode 100644 index 00000000000..23a7c95d59b --- /dev/null +++ b/src/sat/smt/array_solver.cpp @@ -0,0 +1,220 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + array_solver.h + +Abstract: + + Theory plugin for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2020-09-08 + +--*/ + +#include "ast/ast_ll_pp.h" +#include "sat/smt/array_solver.h" +#include "sat/smt/euf_solver.h" + +namespace array { + + solver::solver(euf::solver& ctx, theory_id id): + th_euf_solver(ctx, id), + a(m), + m_sort2epsilon(m), + m_sort2diag(m), + m_find(*this), + m_hash(*this), + m_eq(*this), + m_axioms(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq) + { + m_constraint = alloc(sat::constraint_base); + m_constraint->initialize(m_constraint.get(), this); + } + + sat::check_result solver::check() { + flet _is_redundant(m_is_redundant, true); + bool turn[2] = { false, false }; + turn[s().rand()(2)] = true; + for (unsigned idx = 0; idx < 2; ++idx) { + if (turn[idx]) { + if (add_delayed_axioms()) + return sat::CR_CONTINUE; + } + else { + if (add_interface_equalities()) + return sat::CR_CONTINUE; + } + } + return sat::CR_DONE; + } + + void solver::push() { + th_euf_solver::lazy_push(); + } + + void solver::pop(unsigned n) { + n = lazy_pop(n); + if (n == 0) + return; + m_var_data.resize(get_num_vars()); + } + + std::ostream& solver::display(std::ostream& out) const { + for (unsigned i = 0; i < get_num_vars(); ++i) { + out << var2enode(i)->get_expr_id() << " " << mk_bounded_pp(var2expr(i), m, 2) << "\n"; + } + return out; + } + + std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out; } + std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { return out; } + + void solver::collect_statistics(statistics& st) const { + st.update("array store", m_stats.m_num_store_axiom); + st.update("array sel/store", m_stats.m_num_select_store_axiom); + st.update("array sel/const", m_stats.m_num_select_const_axiom); + st.update("array sel/map", m_stats.m_num_select_map_axiom); + st.update("array sel/as array", m_stats.m_num_select_as_array_axiom); + st.update("array def/map", m_stats.m_num_default_map_axiom); + st.update("array def/const", m_stats.m_num_default_const_axiom); + st.update("array def/store", m_stats.m_num_default_store_axiom); + st.update("array ext ax", m_stats.m_num_extensionality_axiom); + st.update("array cong ax", m_stats.m_num_congruence_axiom); + st.update("array exp ax2", m_stats.m_num_select_store_axiom_delayed); + st.update("array splits", m_stats.m_num_eq_splits); + } + + euf::th_solver* solver::fresh(sat::solver* s, euf::solver& ctx) { + auto* result = alloc(solver, ctx, get_id()); + ast_translation tr(m, ctx.get_manager()); + for (unsigned i = 0; i < get_num_vars(); ++i) { + expr* e1 = var2expr(i); + expr* e2 = tr(e1); + euf::enode* n = ctx.get_enode(e2); + result->mk_var(n); + } + return result; + } + + void solver::new_eq_eh(euf::th_eq const& eq) { + m_find.merge(eq.m_v1, eq.m_v2); + } + + bool solver::unit_propagate() { + if (m_qhead == m_axiom_trail.size()) + return false; + bool prop = false; + ctx.push(value_trail(m_qhead)); + for (; m_qhead < m_axiom_trail.size() && !s().inconsistent(); ++m_qhead) + if (assert_axiom(m_qhead)) + prop = true; + return prop; + } + + void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) { + euf::enode* n1 = var2enode(v1); + euf::enode* n2 = var2enode(v2); + SASSERT(n1->get_root() == n2->get_root()); + SASSERT(n1->is_root() || n2->is_root()); + SASSERT(v1 == find(v1)); + + expr* e1 = n1->get_expr(); + expr* e2 = n2->get_expr(); + auto& d1 = get_var_data(v1); + auto& d2 = get_var_data(v2); + if (d2.m_prop_upward && !d1.m_prop_upward) + set_prop_upward(v1); + if (a.is_array(e1)) + for (euf::enode* parent : d2.m_parents) { + add_parent(v1, parent); + if (a.is_store(parent->get_expr())) + add_store(v1, parent); + } + if (is_lambda(e1) || is_lambda(e2)) + push_axiom(congruence_axiom(n1, n2)); + } + + void solver::unmerge_eh(theory_var v1, theory_var v2) { + auto& p1 = get_var_data(v1).m_parents; + auto& p2 = get_var_data(v2).m_parents; + p1.shrink(p1.size() - p2.size()); + } + + void solver::add_store(theory_var v, euf::enode* store) { + SASSERT(a.is_store(store->get_expr())); + auto& d = get_var_data(v); + unsigned lambda_equiv_class_size = get_lambda_equiv_size(d); + if (get_config().m_array_always_prop_upward || lambda_equiv_class_size >= 1) + set_prop_upward(d); + for (euf::enode* n : d.m_parents) + if (a.is_select(n->get_expr())) + push_axiom(select_axiom(n, store)); + if (get_config().m_array_always_prop_upward || lambda_equiv_class_size >= 1) + set_prop_upward(store); + } + + void solver::add_parent(theory_var v_child, euf::enode* parent) { + SASSERT(parent->is_root()); + get_var_data(v_child).m_parents.push_back(parent); + euf::enode* child = var2enode(v_child); + euf::enode* r = child->get_root(); + expr* p = parent->get_expr(); + expr* c = child->get_expr(); + if (a.is_select(p) && parent->get_arg(0)->get_root() == r) { + if (a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c)) + push_axiom(select_axiom(parent, child)); +#if 0 + if (!get_config().m_array_delay_exp_axiom && d.m_prop_upward) { + auto& d = get_var_data(v_child); + for (euf::enode* p2 : d.m_parents) + if (a.is_store(p2->get_expr())) + push_axiom(select_axiom(parent, p2)); + } +#endif + } + else if (a.mk_default(p)) { + if (a.is_const(c) || a.is_store(c) || a.is_map(c) || a.is_as_array(c)) + push_axiom(default_axiom(child)); + } + } + + void solver::set_prop_upward(theory_var v) { + auto& d = get_var_data(find(v)); + if (!d.m_prop_upward) { + ctx.push(reset_flag_trail(d.m_prop_upward)); + d.m_prop_upward = true; + if (!get_config().m_array_delay_exp_axiom) + push_parent_select_store_axioms(v); + set_prop_upward(d); + } + } + + void solver::set_prop_upward(euf::enode* n) { + if (a.is_store(n->get_expr())) + set_prop_upward(n->get_arg(0)->get_th_var(get_id())); + } + + void solver::set_prop_upward(var_data& d) { + for (auto* p : d.m_parents) + set_prop_upward(p); + } + + /** + \brief Return the size of the equivalence class for array terms + that can be expressed as \lambda i : Index . [.. (select a i) ..] + */ + unsigned solver::get_lambda_equiv_size(var_data const& d) { + unsigned sz = 0; + for (auto* p : d.m_parents) + if (a.is_store(p->get_expr())) + ++sz; + return sz; + } + + + +} diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h new file mode 100644 index 00000000000..aa923edd37c --- /dev/null +++ b/src/sat/smt/array_solver.h @@ -0,0 +1,203 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + array_solver.h + +Abstract: + + Theory plugin for arrays + +Author: + + Nikolaj Bjorner (nbjorner) 2020-09-08 + +--*/ +#pragma once + +#include "ast/ast_trail.h" +#include "sat/smt/sat_th.h" +#include "ast/array_decl_plugin.h" + +namespace euf { + class solver; +} + +namespace array { + + class solver : public euf::th_euf_solver { + typedef euf::theory_var theory_var; + typedef euf::theory_id theory_id; + typedef sat::literal literal; + typedef sat::bool_var bool_var; + typedef sat::literal_vector literal_vector; + typedef union_find array_union_find; + + + struct stats { + unsigned m_num_store_axiom, m_num_extensionality_axiom; + unsigned m_num_eq_splits, m_num_congruence_axiom; + unsigned m_num_select_store_axiom, m_num_select_as_array_axiom, m_num_select_map_axiom; + unsigned m_num_select_const_axiom, m_num_select_store_axiom_delayed; + unsigned m_num_default_store_axiom, m_num_default_map_axiom; + unsigned m_num_default_const_axiom, m_num_default_as_array_axiom; + void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } + }; + + // void log_drat(array_justification const& c); + + struct var_data { + bool m_prop_upward{ false }; + bool m_is_array{ false }; + bool m_is_select{ false }; + ptr_vector m_parents; + var_data() {} + }; + + + array_util a; + stats m_stats; + sat::solver* m_solver{ nullptr }; + scoped_ptr_vector m_var_data; + ast2ast_trailmap m_sort2epsilon; + ast2ast_trailmap m_sort2diag; + obj_map m_sort2diff; + array_union_find m_find; + + sat::solver& s() { return *m_solver; } + theory_var find(theory_var v) { return m_find.find(v); } + + // internalize + bool visit(expr* e) override; + bool visited(expr* e) override; + bool post_visit(expr* e, bool sign, bool root) override; + void ensure_var(euf::enode* n); + void internalize_store(euf::enode* n); + void internalize_select(euf::enode* n); + void internalize_const(euf::enode* n); + void internalize_ext(euf::enode* n); + void internalize_default(euf::enode* n); + void internalize_map(euf::enode* n); + void internalize_as_array(euf::enode* n); + + // axioms + struct axiom_record { + enum class kind_t { + is_store, + is_select, + is_extensionality, + is_default, + is_congruence + }; + kind_t m_kind; + euf::enode* n; + euf::enode* select; + axiom_record(kind_t k, euf::enode* n, euf::enode* select = nullptr) : m_kind(k), n(n), select(select) {} + + struct hash { + solver& s; + hash(solver& s) :s(s) {} + unsigned operator()(unsigned idx) const { + auto const& r = s.m_axiom_trail[idx]; + return mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select ? r.select->get_expr_id() : 1); + } + }; + + struct eq { + solver& s; + eq(solver& s) :s(s) {} + unsigned operator()(unsigned a, unsigned b) const { + auto const& p = s.m_axiom_trail[a]; + auto const& r = s.m_axiom_trail[b]; + return p.n == r.n && p.select == r.select && p.m_kind == r.m_kind; + } + }; + }; + typedef hashtable axiom_table_t; + axiom_record::hash m_hash; + axiom_record::eq m_eq; + axiom_table_t m_axioms; + svector m_axiom_trail; + unsigned m_qhead { 0 }; + void push_axiom(axiom_record const& r); + bool assert_axiom(unsigned idx); + + axiom_record select_axiom(euf::enode* s, euf::enode* n) { return axiom_record(axiom_record::kind_t::is_select, n, s); } + axiom_record default_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_default, n); } + axiom_record store_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_store, n); } + axiom_record extensionality_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_extensionality, n); } + axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); } + + scoped_ptr m_constraint; + + sat::ext_justification_idx array_axiom() { return m_constraint->to_index(); } + + bool assert_store_axiom(app* _e); + bool assert_select_store_axiom(app* select, app* store); + bool assert_select_const_axiom(app* select, app* cnst); + bool assert_select_as_array_axiom(app* select, app* arr); + bool assert_select_map_axiom(app* select, app* map); + bool assert_select_lambda_axiom(app* select, expr* lambda); + bool assert_extensionality(expr* e1, expr* e2); + bool assert_default_map_axiom(app* map); + bool assert_default_const_axiom(app* cnst); + bool assert_default_store_axiom(app* store); + bool assert_default_as_array_axiom(app* as_array); + bool assert_congruent_axiom(expr* e1, expr* e2); + bool add_delayed_axioms(); + + bool has_unitary_domain(app* array_term); + bool has_large_domain(app* array_term); + std::pair mk_epsilon(sort* s); + void collect_shared_vars(sbuffer& roots); + bool add_interface_equalities(); + bool is_select_arg(euf::enode* r); + + // solving + void add_parent(theory_var v_child, euf::enode* parent); + void add_parent(euf::enode* child, euf::enode* parent) { add_parent(child->get_th_var(get_id()), parent); } + void add_store(theory_var v, euf::enode* store); + void set_prop_upward(theory_var v); + void set_prop_upward(var_data& d); + void set_prop_upward(euf::enode* n); + void push_parent_select_store_axioms(theory_var v); + unsigned get_lambda_equiv_size(var_data const& d); + + var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); } + var_data& get_var_data(theory_var v) { return *m_var_data[v]; } + + + // invariants + + public: + solver(euf::solver& ctx, theory_id id); + ~solver() override {} + void set_solver(sat::solver* s) override { m_solver = s; } + bool is_external(bool_var v) override { return false; } + bool propagate(literal l, sat::ext_constraint_idx idx) override { UNREACHABLE(); return false; } + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {} + void asserted(literal l) override {} + sat::check_result check() override; + void push() override; + void pop(unsigned n) override; + std::ostream& display(std::ostream& out) const override; + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + void collect_statistics(statistics& st) const override; + euf::th_solver* fresh(sat::solver* s, euf::solver& ctx) override; + void new_eq_eh(euf::th_eq const& eq) override; + bool unit_propagate() override; + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; + void add_dep(euf::enode* n, top_sort& dep) override; + sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; + void internalize(expr* e, bool redundant) override; + euf::theory_var mk_var(euf::enode* n) override; + void apply_sort_cnstr(euf::enode* n, sort* s) override; + + void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2); + void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} + void unmerge_eh(theory_var v1, theory_var v2); + }; +} diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 9029c30823c..4f6bbea450b 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -62,7 +62,7 @@ namespace bv { m_zero_one_bits.push_back(zero_one_bits()); ctx.attach_th_var(n, this, r); - TRACE("bv", tout << "mk-var: " << r << " " << n->get_owner_id() << " " << mk_pp(n->get_owner(), m) << "\n";); + TRACE("bv", tout << "mk-var: " << r << " " << n->get_expr_id() << " " << mk_pp(n->get_expr(), m) << "\n";); return r; } @@ -100,17 +100,9 @@ namespace bv { app* a = to_app(e); SASSERT(!n || !n->is_attached_to(get_id())); - if (!n) { - m_args.reset(); - if (get_config().m_bv_reflect || m.is_considered_uninterpreted(a->get_decl())) { - for (expr* arg : *a) - m_args.push_back(expr2enode(arg)); - } - DEBUG_CODE(for (auto* n : m_args) VERIFY(n);); - n = ctx.mk_enode(e, m_args.size(), m_args.c_ptr()); - SASSERT(!n->is_attached_to(get_id())); - ctx.attach_node(n); - } + bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl()); + if (!n) + n = mk_enode(e, suppress_args); SASSERT(!n->is_attached_to(get_id())); theory_var v = mk_var(n); @@ -196,14 +188,14 @@ namespace bv { theory_var v = n->get_th_var(get_id()); if (v == euf::null_theory_var) { v = mk_var(n); - if (bv.is_bv(n->get_owner())) + if (bv.is_bv(n->get_expr())) mk_bits(v); } return v; } euf::enode* solver::get_arg(euf::enode* n, unsigned idx) { - app* o = to_app(n->get_owner()); + app* o = to_app(n->get_expr()); return ctx.get_enode(o->get_arg(idx)); } @@ -280,7 +272,7 @@ namespace bv { } unsigned solver::get_bv_size(euf::enode* n) { - return bv.get_bv_size(n->get_owner()); + return bv.get_bv_size(n->get_expr()); } unsigned solver::get_bv_size(theory_var v) { diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 564d1db98cf..b2cfb283ec8 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -153,7 +153,7 @@ namespace bv { out.width(4); out << e->get_id() << " -> "; out.width(4); - out << var2enode(find(v))->get_owner_id(); + out << var2enode(find(v))->get_expr_id(); out << std::right; out.flush(); atom* a = nullptr; @@ -168,7 +168,7 @@ namespace bv { else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) { if (a->is_bit()) { for (var_pos vp : a->to_bit()) - out << " " << var2enode(vp.first)->get_owner_id() << "[" << vp.second << "]"; + out << " " << var2enode(vp.first)->get_expr_id() << "[" << vp.second << "]"; } else out << "def-atom"; @@ -277,7 +277,7 @@ namespace bv { literal bit1 = m_bits[v1][idx]; lbool val = s().value(bit1); - TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_owner_id() << "[" << idx << "] = " << val << "\n";); + TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";); if (val == l_undef) return; @@ -287,7 +287,7 @@ namespace bv { for (theory_var v2 = m_find.next(v1); v2 != v1 && !s().inconsistent(); v2 = m_find.next(v2)) { literal bit2 = m_bits[v2][idx]; SASSERT(m_bits[v1][idx] != ~m_bits[v2][idx]); - TRACE("bv", tout << "propagating #" << var2enode(v2)->get_owner_id() << "[" << idx << "] = " << s().value(bit2) << "\n";); + TRACE("bv", tout << "propagating #" << var2enode(v2)->get_expr_id() << "[" << idx << "] = " << s().value(bit2) << "\n";); if (val == l_false) bit2.neg(); @@ -454,8 +454,8 @@ namespace bv { bool solver::check_model(sat::model const& m) const { return true; } unsigned solver::max_var(unsigned w) const { return w; } - void solver::add_value(euf::enode* n, expr_ref_vector& values) { - SASSERT(bv.is_bv(n->get_owner())); + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + SASSERT(bv.is_bv(n->get_expr())); theory_var v = n->get_th_var(get_id()); rational val; unsigned i = 0; @@ -477,7 +477,7 @@ namespace bv { } void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { - TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_owner_id() << " v" << v2 << " #" << var2enode(v2)->get_owner_id() << "\n";); + TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";); if (!merge_zero_one_bits(r1, r2)) { TRACE("bv", tout << "conflict detected\n";); return; // conflict was detected diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 179d96ba402..45f90d10993 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -268,7 +268,7 @@ namespace bv { void new_eq_eh(euf::th_eq const& eq) override; bool unit_propagate() override; - void add_value(euf::enode* n, expr_ref_vector& values) override; + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; bool extract_pb(std::function& card, std::function& pb) override { return false; } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 0898f8847d6..2b773b06074 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -23,7 +23,7 @@ namespace euf { void solver::internalize(expr* e, bool redundant) { if (si.is_bool_op(e)) - attach_lit(si.internalize(e, redundant), e); + attach_lit(si.internalize(e, redundant), e); else if (auto* ext = get_solver(e)) ext->internalize(e, redundant); else @@ -32,8 +32,8 @@ namespace euf { } sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { - if (si.is_bool_op(e)) - return attach_lit(si.internalize(e, redundant), e); + if (si.is_bool_op(e)) + return attach_lit(si.internalize(e, redundant), e); if (auto* ext = get_solver(e)) return ext->internalize(e, sign, root, redundant); if (!visit_rec(m, e, sign, root, redundant)) @@ -82,11 +82,11 @@ namespace euf { } void solver::attach_node(euf::enode* n) { - expr* e = n->get_owner(); + expr* e = n->get_expr(); if (!m.is_bool(e)) log_node(e); - else - attach_lit(literal(si.add_bool_var(e), false), e); + else + attach_lit(literal(si.add_bool_var(e), false), e); if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) { auto* e_ext = get_solver(e); @@ -143,7 +143,7 @@ namespace euf { sat::literal_vector lits; for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m); + expr_ref eq(m.mk_eq(args[i]->get_expr(), args[j]->get_expr()), m); sat::literal lit = internalize(eq, false, false, m_is_redundant); lits.push_back(lit); } @@ -184,11 +184,11 @@ namespace euf { if (sz <= 1) { s().mk_clause(0, nullptr, st); return; - } + } if (sz <= distinct_max_args) { for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m); + expr_ref eq(m.mk_eq(args[i]->get_expr(), args[j]->get_expr()), m); sat::literal lit = internalize(eq, true, false, m_is_redundant); s().add_clause(1, &lit, st); } @@ -213,9 +213,9 @@ namespace euf { } void solver::axiomatize_basic(enode* n) { - expr* e = n->get_owner(); + expr* e = n->get_expr(); sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); - if (m.is_ite(e)) { + if (m.is_ite(e)) { app* a = to_app(e); expr* c = a->get_arg(0); expr* th = a->get_arg(1); @@ -237,7 +237,7 @@ namespace euf { unsigned sz = n->num_args(); for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - expr_ref eq(m.mk_eq(n->get_arg(i)->get_owner(), n->get_arg(j)->get_owner()), m); + expr_ref eq(m.mk_eq(n->get_arg(i)->get_expr(), n->get_arg(j)->get_expr()), m); eqs.push_back(eq); } } @@ -247,8 +247,65 @@ namespace euf { sat::literal lits1[2] = { ~dist, ~some_eq }; sat::literal lits2[2] = { dist, some_eq }; s().add_clause(2, lits1, st); - s().add_clause(2, lits2, st); + s().add_clause(2, lits2, st); } } + + bool solver::is_shared(enode* n) const { + n = n->get_root(); + + if (m.is_ite(n->get_expr())) + return true; + + theory_id th_id = null_theory_id; + for (auto p : euf::enode_th_vars(n)) { + if (th_id == null_theory_id) + th_id = p.get_id(); + else + return true; + } + if (th_id == null_theory_id) + return false; + + // the variable is shared if the equivalence class of n + // contains a parent application. + + for (euf::enode* parent : euf::enode_parents(n)) { + app* p = to_app(parent->get_expr()); + family_id fid = p->get_family_id(); + if (fid != th_id && fid != m.get_basic_family_id()) + return true; + } + + // Some theories implement families of theories. Examples: + // Arrays and Tuples. For example, array theory is a + // parametric theory, that is, it implements several theories: + // (array int int), (array int (array int int)), ... + // + // Example: + // + // a : (array int int) + // b : (array int int) + // x : int + // y : int + // v : int + // w : int + // A : (array (array int int) int) + // + // assert (= b (store a x v)) + // assert (= b (store a y w)) + // assert (not (= x y)) + // assert (not (select A a)) + // assert (not (select A b)) + // check + // + // In the example above, 'a' and 'b' are shared variables between + // the theories of (array int int) and (array (array int int) int). + // Remark: The inconsistency is not going to be detected if they are + // not marked as shared. + return true; + // TODO + // return get_theory(th_id)->is_shared(l->get_var()); + } } diff --git a/src/sat/smt/euf_invariant.cpp b/src/sat/smt/euf_invariant.cpp index bb5e0c68837..97f7acb5147 100644 --- a/src/sat/smt/euf_invariant.cpp +++ b/src/sat/smt/euf_invariant.cpp @@ -26,14 +26,14 @@ namespace euf { void solver::check_eqc_bool_assignment() const { for (enode* n : m_egraph.nodes()) { - VERIFY(!m.is_bool(n->get_owner()) || + VERIFY(!m.is_bool(n->get_expr()) || s().value(get_literal(n)) == s().value(get_literal(n->get_root()))); } } void solver::check_missing_bool_enode_propagation() const { for (enode* n : m_egraph.nodes()) - if (m.is_bool(n->get_owner()) && l_undef == s().value(get_literal(n))) { + if (m.is_bool(n->get_expr()) && l_undef == s().value(get_literal(n))) { if (!n->is_root()) { VERIFY(l_undef == s().value(get_literal(n->get_root()))); } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 26f6106d958..c6a3fd4ed30 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -48,7 +48,7 @@ namespace euf { deps.insert(n, nullptr); continue; } - auto* mb = get_solver(n->get_owner()); + auto* mb = get_solver(n->get_expr()); if (mb) mb->add_dep(n, deps); else @@ -56,13 +56,13 @@ namespace euf { } } - void solver::dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl) { + void solver::dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref& mdl) { user_sort_factory user_sort(m); for (enode* n : deps.top_sorted()) { unsigned id = n->get_root_id(); if (values.get(id, nullptr)) continue; - expr* e = n->get_owner(); + expr* e = n->get_expr(); values.reserve(id + 1); if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(to_app(e)->get_decl())) { values.set(id, mdl->get_const_interp(to_app(e)->get_decl())); @@ -96,13 +96,13 @@ namespace euf { } auto* mb = get_solver(e); if (mb) - mb->add_value(n, values); + mb->add_value(n, *mdl, values); else if (m.is_uninterp(m.get_sort(e))) { expr* v = user_sort.get_fresh_value(m.get_sort(e)); values.set(id, v); } else if ((mb = get_solver(m.get_sort(e)))) - mb->add_value(n, values); + mb->add_value(n, *mdl, values); else { IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n"); } @@ -112,7 +112,7 @@ namespace euf { void solver::values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl) { ptr_vector args; for (enode* n : deps.top_sorted()) { - expr* e = n->get_owner(); + expr* e = n->get_expr(); if (!is_app(e)) continue; app* a = to_app(e); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 71572c90507..e336fff93ba 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -138,8 +138,11 @@ namespace euf { m_egraph.explain_eq(m_explain, a, b); } - void solver::propagate(enode* a, enode* b, ext_justification_idx idx) { + bool solver::propagate(enode* a, enode* b, ext_justification_idx idx) { + if (a->get_root() == b->get_root()) + return false; m_egraph.merge(a, b, to_ptr(idx)); + return true; } @@ -235,7 +238,7 @@ namespace euf { euf::enode_bool_pair p = m_egraph.get_literal(); euf::enode* n = p.first; bool is_eq = p.second; - expr* e = n->get_owner(); + expr* e = n->get_expr(); expr* a = nullptr, *b = nullptr; bool_var v = si.to_bool_var(e); SASSERT(m.is_bool(e)); @@ -247,7 +250,7 @@ namespace euf { lit = literal(v, false); } else { - a = e, b = n->get_root()->get_owner(); + a = e, b = n->get_root()->get_expr(); SASSERT(m.is_true(b) || m.is_false(b)); cnstr = lit_constraint().to_index(); lit = literal(v, m.is_false(b)); @@ -548,7 +551,7 @@ namespace euf { } for (euf::enode* n : m_egraph.nodes()) { if (!n->is_root()) - fmls.push_back(m.mk_eq(n->get_owner(), n->get_root()->get_owner())); + fmls.push_back(m.mk_eq(n->get_expr(), n->get_root()->get_expr())); } return true; } @@ -560,4 +563,5 @@ namespace euf { return false; return true; } + } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 32eee7da2e5..42395f04d2a 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -20,6 +20,7 @@ Module Name: #include "util/trail.h" #include "ast/ast_translation.h" #include "ast/euf/euf_egraph.h" +#include "ast/rewriter/th_rewriter.h" #include "tactic/model_converter.h" #include "sat/sat_extension.h" #include "sat/smt/atom2bool_var.h" @@ -83,6 +84,7 @@ namespace euf { euf::egraph m_egraph; euf_trail_stack m_trail; stats m_stats; + th_rewriter m_rewriter; func_decl_ref_vector m_unhandled_functions; @@ -129,13 +131,12 @@ namespace euf { th_solver* get_solver(expr* e); th_solver* get_solver(sat::bool_var v); void add_solver(family_id fid, th_solver* th); - void unhandled_function(func_decl* f); void init_ackerman(); // model building bool include_func_interp(func_decl* f); void register_macros(model& mdl); - void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl); + void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref& mdl); void collect_dependencies(deps_t& deps); void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl); @@ -166,6 +167,7 @@ namespace euf { si(si), m_egraph(m), m_trail(*this), + m_rewriter(m), m_unhandled_functions(m), m_solver(nullptr), m_lookahead(nullptr), @@ -201,7 +203,7 @@ namespace euf { ast_manager& get_manager() { return m; } enode* get_enode(expr* e) { return m_egraph.find(e); } sat::literal get_literal(expr* e) const { return literal(si.to_bool_var(e), false); } - sat::literal get_literal(enode* e) const { return get_literal(e->get_owner()); } + sat::literal get_literal(enode* e) const { return get_literal(e->get_expr()); } smt_params const& get_config() { return m_config; } region& get_region() { return m_trail.get_region(); } template @@ -217,7 +219,7 @@ namespace euf { bool is_external(bool_var v) override; bool propagate(literal l, ext_constraint_idx idx) override; bool unit_propagate() override; - void propagate(enode* a, enode* b, ext_justification_idx); + bool propagate(enode* a, enode* b, ext_justification_idx); bool set_root(literal l, literal r) override; void flush_roots() override; @@ -262,6 +264,9 @@ namespace euf { void attach_node(euf::enode* n); euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); } expr* bool_var2expr(sat::bool_var v) { return m_var2expr.get(v, nullptr); } + void unhandled_function(func_decl* f); + th_rewriter& get_rewriter() { return m_rewriter; } + bool is_shared(euf::enode* n) const; void update_model(model_ref& mdl); diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 21b2a475171..0fc9c78756f 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -139,4 +139,23 @@ namespace euf { ctx.s().add_clause(4, lits, sat::status::th(m_is_redundant, get_id())); } + euf::enode* th_euf_solver::mk_enode(expr* e, bool suppress_args) { + m_args.reset(); + if (!suppress_args) + for (expr* arg : *to_app(e)) + m_args.push_back(expr2enode(arg)); + euf::enode* n = ctx.mk_enode(e, m_args.size(), m_args.c_ptr()); + ctx.attach_node(n); + if (m.is_bool(e)) { + sat::bool_var v = ctx.get_si().add_bool_var(e); + NOT_IMPLEMENTED_YET(); + // TODO: ctx.attach_lit(literal(v, false), e); + } + return n; + } + + + void th_euf_solver::rewrite(expr_ref& a) { + ctx.get_rewriter()(a); + } } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 55c0793d970..33d49467aac 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -19,6 +19,7 @@ Module Name: #include "util/top_sort.h" #include "sat/smt/sat_smt.h" #include "ast/euf/euf_egraph.h" +#include "model/model.h" #include "smt/params/smt_params.h" namespace euf { @@ -44,6 +45,8 @@ namespace euf { virtual void internalize(expr* e, bool redundant) = 0; + sat::literal b_internalize(expr* e) { return internalize(e, false, false, m_is_redundant); } + /** \brief Apply (interpreted) sort constraints on the given enode. */ @@ -55,7 +58,7 @@ namespace euf { public: virtual ~th_decompile() {} - virtual bool to_formulas(std::function& lit2expr, expr_ref_vector& fmls) = 0; + virtual bool to_formulas(std::function& lit2expr, expr_ref_vector& fmls) { return false; } }; class th_model_builder { @@ -67,7 +70,7 @@ namespace euf { \brief compute the value for enode \c n and store the value in \c values for the root of the class of \c n. */ - virtual void add_value(euf::enode* n, expr_ref_vector& values) {} + virtual void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {} /** \brief compute dependencies for node n @@ -113,10 +116,16 @@ namespace euf { void add_unit(sat::literal lit); + void add_clause(sat::literal lit) { add_unit(lit); } void add_clause(sat::literal a, sat::literal b); void add_clause(sat::literal a, sat::literal b, sat::literal c); void add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d); + euf::enode* e_internalize(expr* e) { internalize(e, m_is_redundant); return expr2enode(e); } + euf::enode* mk_enode(expr* e, bool suppress_args); + + void rewrite(expr_ref& a); + public: th_euf_solver(euf::solver& ctx, euf::theory_id id); virtual ~th_euf_solver() {} @@ -124,7 +133,7 @@ namespace euf { unsigned get_num_vars() const { return m_var2enode.size();} enode* expr2enode(expr* e) const; enode* var2enode(theory_var v) const { return m_var2enode[v]; } - expr* var2expr(theory_var v) const { return var2enode(v)->get_owner(); } + expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); } expr* bool_var2expr(sat::bool_var v) const; expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); } theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index bd4f69486bd..3090bd7e250 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -451,7 +451,7 @@ namespace { if (p->is_ground()) { enode * e = get_enode(*m_context, p); SASSERT(e->has_lbl_hash()); - out << "#" << e->get_owner_id() << ":" << e->get_lbl_hash() << " "; + out << "#" << e->get_expr_id() << ":" << e->get_lbl_hash() << " "; } else { out << p->get_decl()->get_name() << ":" << m_lbl_hasher(p->get_decl()) << " "; @@ -2240,7 +2240,7 @@ namespace { out << "nil\n"; } else { - out << "#" << n->get_owner_id() << ", root: " << n->get_root()->get_owner_id(); + out << "#" << n->get_expr_id() << ", root: " << n->get_root()->get_expr_id(); if (m_use_filters) out << ", lbls: " << n->get_root()->get_lbls() << " "; out << "\n"; @@ -3940,7 +3940,7 @@ namespace { TRACE("missing_instance", tout << "qa:\n" << mk_ll_pp(qa, m) << "\npat:\n" << mk_ll_pp(pat, m); for (unsigned i = 0; i < num_bindings; i++) - tout << "#" << bindings[i]->get_owner_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m) << "\n"; + tout << "#" << bindings[i]->get_expr_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m) << "\n"; ); UNREACHABLE(); } diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 44df3fa5519..6b4acf60483 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -51,9 +51,9 @@ void smt_params::updt_local_params(params_ref const & _p) { m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); if (_p.get_bool("arith.greatest_error_pivot", false)) - m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR; + m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_GREATEST_ERROR; else if (_p.get_bool("arith.least_error_pivot", false)) - m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR; + m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_LEAST_ERROR; theory_array_params::updt_params(_p); m_dump_benchmarks = false; m_dump_min_time = 0.5; diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 327d6e255ed..c5f7c5e3abe 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -42,12 +42,14 @@ enum arith_prop_strategy { ARITH_PROP_PROPORTIONAL }; -enum arith_pivot_strategy { +enum class arith_pivot_strategy { ARITH_PIVOT_SMALLEST, ARITH_PIVOT_GREATEST_ERROR, ARITH_PIVOT_LEAST_ERROR }; +inline std::ostream& operator<<(std::ostream& out, arith_pivot_strategy st) { return out << (int)st; } + struct theory_arith_params { bool m_arith_eq2ineq; bool m_arith_process_all_eqs; @@ -141,7 +143,7 @@ struct theory_arith_params { m_arith_adaptive_gcd(false), m_arith_propagation_threshold(UINT_MAX), m_arith_bounded_expansion(false), - m_arith_pivot_strategy(ARITH_PIVOT_SMALLEST), + m_arith_pivot_strategy(arith_pivot_strategy::ARITH_PIVOT_SMALLEST), m_arith_add_binary_bounds(false), m_arith_propagation_strategy(ARITH_PROP_PROPORTIONAL), m_arith_eq_bounds(false), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ae5524095bb..6ce7c69c870 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1279,9 +1279,9 @@ namespace smt { SASSERT(e_internalized(arg)); enode * _arg = get_enode(arg); CTRACE("eq_to_bug", args[i]->get_root() != _arg->get_root(), - tout << "#" << args[i]->get_owner_id() << " #" << args[i]->get_root()->get_owner_id() - << " #" << _arg->get_owner_id() << " #" << _arg->get_root()->get_owner_id() << "\n"; - tout << "#" << r->get_owner_id() << "\n"; + tout << "#" << args[i]->get_expr_id() << " #" << args[i]->get_root()->get_expr_id() + << " #" << _arg->get_expr_id() << " #" << _arg->get_root()->get_expr_id() << "\n"; + tout << "#" << r->get_expr_id() << "\n"; display(tout);); SASSERT(args[i]->get_root() == _arg->get_root()); } @@ -2749,8 +2749,8 @@ namespace smt { char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin ", ":lemmas ", ":simplify ", ":deletions", ":memory" }; std::stringstream l1, l2; - l1 << "(sat.stats "; - l2 << "(sat.stats "; + l1 << "(smt.stats "; + l2 << "(smt.stats "; size_t p1 = 11, p2 = 11; SASSERT(offsets.size() == 9); for (unsigned i = 0; i < offsets.size(); ++i) { diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index b3c460925ac..4c3d16bee9b 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -93,7 +93,7 @@ namespace smt { (!is_true_eq && (!n->is_cgc_enabled() || n->is_cgr() == (m_cg_table.contains_ptr(n)))) || (is_true_eq && !m_cg_table.contains_ptr(n)); CTRACE("check_enode", !cg_inv, - tout << "n: #" << n->get_owner_id() << ", m_cg: #" << n->m_cg->get_owner_id() << ", contains: " << m_cg_table.contains(n) << "\n"; display(tout);); + tout << "n: #" << n->get_expr_id() << ", m_cg: #" << n->m_cg->get_expr_id() << ", contains: " << m_cg_table.contains(n) << "\n"; display(tout);); SASSERT(cg_inv); return true; } @@ -235,8 +235,8 @@ namespace smt { if (m.is_bool(e->get_owner())) { enode * r = e->get_root(); CTRACE("eqc_bool", get_assignment(e) != get_assignment(r), - tout << "#" << e->get_owner_id() << "\n" << mk_pp(e->get_owner(), m) << "\n"; - tout << "#" << r->get_owner_id() << "\n" << mk_pp(r->get_owner(), m) << "\n"; + tout << "#" << e->get_expr_id() << "\n" << mk_pp(e->get_owner(), m) << "\n"; + tout << "#" << r->get_expr_id() << "\n" << mk_pp(r->get_owner(), m) << "\n"; tout << "assignments: " << get_assignment(e) << " " << get_assignment(r) << "\n"; display(tout);); SASSERT(get_assignment(e) == get_assignment(r)); @@ -271,7 +271,7 @@ namespace smt { if (has_enode(v)) { enode * n = bool_var2enode(v); if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m.is_iff(n->get_owner())) { - TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m) << "\n";); + TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_expr_id() << " " << mk_bounded_pp(n->get_owner(), m) << "\n";); enode * lhs = n->get_arg(0)->get_root(); enode * rhs = n->get_arg(1)->get_root(); if (rhs->is_interpreted() && lhs->is_interpreted()) @@ -305,9 +305,9 @@ namespace smt { CTRACE("check_th_diseq_propagation", !found, tout << "checking theory: " << m.get_family_name(th_id) << "\n" - << "root: #" << n->get_root()->get_owner_id() << " node: #" << n->get_owner_id() << "\n" + << "root: #" << n->get_root()->get_expr_id() << " node: #" << n->get_expr_id() << "\n" << mk_pp(n->get_owner(), m) << "\n" - << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() << "\n" + << "lhs: #" << lhs->get_expr_id() << ", rhs: #" << rhs->get_expr_id() << "\n" << mk_bounded_pp(lhs->get_owner(), m) << " " << mk_bounded_pp(rhs->get_owner(), m) << "\n";); VERIFY(found); } @@ -325,8 +325,8 @@ namespace smt { enode * n2 = p.second; if (n1->get_root() == n2->get_root()) { TRACE("diseq_bug", - tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << - ", r: #" << n1->get_root()->get_owner_id() << "\n"; + tout << "n1: #" << n1->get_expr_id() << ", n2: #" << n2->get_expr_id() << + ", r: #" << n1->get_root()->get_expr_id() << "\n"; tout << "n1 parents:\n"; display_parent_eqs(tout, n1); tout << "n2 parents:\n"; display_parent_eqs(tout, n2); tout << "r parents:\n"; display_parent_eqs(tout, n1->get_root()); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 88696629a28..9a12a6d2c74 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -2278,9 +2278,9 @@ namespace smt { if (m_blands_rule) return select_smallest_var(); switch (m_params.m_arith_pivot_strategy) { - case ARITH_PIVOT_GREATEST_ERROR: + case arith_pivot_strategy::ARITH_PIVOT_GREATEST_ERROR: return select_greatest_error_var(); - case ARITH_PIVOT_LEAST_ERROR: + case arith_pivot_strategy::ARITH_PIVOT_LEAST_ERROR: return select_least_error_var(); default: return select_smallest_var(); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 1c5fc4bb4f6..f871bb464da 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -495,7 +495,7 @@ namespace smt { if (ctx.is_relevant(n) && ctx.is_shared(n)) { enode * r = n->get_root(); if (!r->is_marked() && is_array_sort(r)) { - TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + TRACE("array_shared", tout << "new shared var: #" << r->get_expr_id() << "\n";); r->set_mark(); to_unmark.push_back(r); theory_var r_th_var = r->get_var(get_id()); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 077e8328472..2528f24ed2f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2083,8 +2083,8 @@ void theory_seq::validate_model(model& mdl) { enode* rn = ensure_enode(r); IF_VERBOSE(0, verbose_stream() << "bad representation: " << l << " ->\n" << r << "\nbut\n" << mdl(l) << "\n->\n" << mdl(r) << "\n" - << "nodes: #" << ln->get_owner_id() << " #" << rn->get_owner_id() << "\n" - << "roots: #" << ln->get_root()->get_owner_id() << " #" << rn->get_root()->get_owner_id() << "\n"; + << "nodes: #" << ln->get_expr_id() << " #" << rn->get_expr_id() << "\n" + << "roots: #" << ln->get_root()->get_expr_id() << " #" << rn->get_root()->get_expr_id() << "\n"; ); } } diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index 2bfd1404786..3b5c5e78272 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -74,7 +74,69 @@ static void tst2(unsigned num_bits) { } } +// prints all don't care pareto fronts for 8-bit multiplier. +static void test_dc() { + unsigned a = 0; + unsigned b = 0; + unsigned num_bits = 8; + unsigned num_vals = 1 << num_bits; + tbv_manager m(num_bits*2); + tbv::eq eq(m); + tbv::hash hash(m); + ptr_vector tbvs, todo; + map eval(hash, eq); + + for (unsigned a = 0; a < num_vals; ++a) { + for (unsigned b = 0; b < num_vals; ++b) { + unsigned c = a*b; + unsigned bits = a + (b << num_bits); + bool value = (c & (1 << (num_bits-1))) != 0; + tbv* t = m.allocate(bits); + tbvs.push_back(t); + eval.insert(t, value ? BIT_1 : BIT_0); + todo.push_back(t); + } + } + std::cout << todo.size() << "\n"; + for (unsigned i = 0; i < todo.size(); ++i) { + tbv* t = todo[i]; + todo.pop_back(); + bool found = false; + tbit tvalue = eval[t]; + SASSERT(tvalue != BIT_z); + for (unsigned j = 0; j < 2*num_bits; ++j) { + tbit tb = (*t)[j]; + if (tb == BIT_x) + continue; + tbv* nt = m.allocate(*t); + tbvs.push_back(nt); + m.set(*nt, j, neg(tb)); + if (!eval.contains(nt)) + continue; + tbit nvalue = eval[nt]; + m.set(*nt, j, BIT_x); + if (eval.contains(nt)) + continue; + if (tvalue == nvalue) { + todo.push_back(nt); + eval.insert(nt, tvalue); + found = true; + } + else + eval.insert(nt, BIT_z); + } + if (!found) + m.display(std::cout, *t) << " := " << (eval[t] == BIT_0 ? 0 : 1) << "\n"; + } + + + for (auto* t : tbvs) + m.deallocate(t); + +} + void tst_tbv() { + // test_dc(); tst0(); tst1(31); diff --git a/src/util/dlist.h b/src/util/dlist.h index d5a2c404600..6248f34df61 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Templates for manipulating doubly linked lists. + Templates for manipulating circular doubly linked lists. Author: @@ -18,123 +18,6 @@ Revision History: --*/ #pragma once -#if 0 --- unused - -/** - Add element \c elem to the list headed by \c head. - NextProc and PrevProc must have the methods: - T * & operator()(T *); - T * & operator()(T *); - They should return the next and prev fields of the given object. -*/ -template -void dlist_add(T * & head, T * elem, NextProc const & next = NextProc(), PrevProc const & prev = PrevProc()) { - SASSERT(prev(elem) == 0); - SASSERT(next(elem) == 0); - if (head == 0) { - head = elem; - } - else { - next(elem) = head; - prev(head) = elem; - head = elem; - } -} - -template -void dlist_del(T * & head, T * elem, NextProc const & next = NextProc(), PrevProc const & prev = PrevProc()) { - T * & prev_elem = prev(elem); - T * & next_elem = next(elem); - if (head == elem) { - SASSERT(prev_elem == 0); - if (next_elem != 0) - prev(next_elem) = 0; - head = next_elem; - } - else { - SASSERT(prev_elem != 0); - next(prev_elem) = next_elem; - if (next_elem != 0) - prev(next_elem) = prev_elem; - } - prev_elem = 0; - next_elem = 0; -} - -/** - \brief Remove the head of the list. Return the old head. -*/ -template -T * dlist_pop(T * & head, NextProc const & next = NextProc(), PrevProc const & prev = PrevProc()) { - if (head == 0) { - return 0; - } - else { - SASSERT(prev(head) == 0); - T * r = head; - head = next(head); - if (head) - prev(head) = 0; - next(r) = 0; - return r; - } -} - -/** - \brief Insert new element after elem. -*/ -template -void dlist_insert_after(T * elem, T * new_elem, NextProc const & next = NextProc(), PrevProc const & prev = PrevProc()) { - SASSERT(elem); - SASSERT(new_elem); - T * & old_next_elem = next(elem); - prev(new_elem) = elem; - next(new_elem) = old_next_elem; - if (old_next_elem) - prev(old_next_elem) = new_elem; - // next(elem) = new_elem; - old_next_elem = new_elem; -} - -template -bool dlist_contains(T * head, T const * elem, NextProc const & next = NextProc()) { - T * curr = head; - while (curr != 0) { - if (curr == elem) - return true; - curr = next(curr); - } - return false; -} - -template -unsigned dlist_length(T * head, NextProc const & next = NextProc()) { - unsigned r = 0; - T * curr = head; - while (curr != 0) { - r++; - curr = next(curr); - } - return r; -} - -template -bool dlist_check_invariant(T * head, NextProc const & next = NextProc(), PrevProc const & prev = PrevProc()) { - if (head == 0) - return true; - SASSERT(prev(head) == 0); - T * old = head; - T * curr = next(head); - while (curr != 0) { - SASSERT(prev(curr) == old); - old = curr; - curr = next(curr); - } - return true; -} - -#endif template class dll_base { @@ -149,6 +32,14 @@ class dll_base { m_next = t; m_prev = t; } + + static T* pop(T*& list) { + if (!list) + return list; + T* head = list; + remove_from(list, head); + return head; + } static void remove_from(T*& list, T* elem) { if (list->m_next == list) { @@ -182,6 +73,17 @@ class dll_base { list = elem; } } + + bool invariant() const { + auto* e = this; + do { + if (e->m_next->m_prev != e) + return false; + e = e->m_next; + } + while (e != this); + return true; + } }; diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 78abd3c8796..73be1535924 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -43,12 +43,12 @@ typedef enum { HT_FREE, template class default_hash_entry { - unsigned m_hash; //!< cached hash code + unsigned m_hash{ 0 }; //!< cached hash code hash_entry_state m_state; T m_data; public: typedef T data; - default_hash_entry():m_state(HT_FREE) {} + default_hash_entry():m_state(HT_FREE), m_data() {} unsigned get_hash() const { return m_hash; } bool is_free() const { return m_state == HT_FREE; } bool is_deleted() const { return m_state == HT_DELETED; } diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 6ef7ec76e7c..e45bcc57b24 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -59,10 +59,10 @@ class obj_map { struct key_data { Key * m_key; Value m_value; - key_data():m_key(nullptr) { + key_data():m_key(nullptr), m_value() { } key_data(Key * k): - m_key(k) { + m_key(k), m_value() { } key_data(Key * k, Value const & v): m_key(k), diff --git a/src/util/small_object_allocator.h b/src/util/small_object_allocator.h index 4b58f19969a..028c79645e7 100644 --- a/src/util/small_object_allocator.h +++ b/src/util/small_object_allocator.h @@ -27,8 +27,8 @@ class small_object_allocator { static const unsigned SMALL_OBJ_SIZE = 256; static const unsigned NUM_SLOTS = (SMALL_OBJ_SIZE >> PTR_ALIGNMENT); struct chunk { - chunk * m_next; - char * m_curr; + chunk* m_next{ nullptr }; + char* m_curr{ nullptr }; char m_data[CHUNK_SIZE]; chunk():m_curr(m_data) {} }; diff --git a/src/util/top_sort.h b/src/util/top_sort.h index 0e4f97af118..dd4b7360091 100644 --- a/src/util/top_sort.h +++ b/src/util/top_sort.h @@ -99,9 +99,9 @@ class top_sort { T_set* tb = nullptr; if (!m_deps.find(t, tb)) { tb = alloc(T_set); - insert(s, tb); + insert(t, tb); } - t->insert(s); + tb->insert(s); } ptr_vector const& top_sorted() const { return m_top_sorted; }