diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 5fb87bf64..50735a57c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -717,7 +717,7 @@ struct else mk_exists ctx sorts names body weight patterns nopatterns quantifier_id skolem_id - let mk_quantifier (ctx:context) (universal:bool) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = + let mk_quantifier_const (ctx:context) (universal:bool) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = if universal then mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id else diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 4b6d8bc25..69dbfa23d 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -743,10 +743,10 @@ sig val mk_lambda : context -> (Symbol.symbol * Sort.sort) list -> Expr.expr -> quantifier (** Create a Quantifier. *) - val mk_quantifier : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier + val mk_quantifier : context -> bool -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier (** Create a Quantifier. *) - val mk_quantifier : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier + val mk_quantifier_const : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier (** A string representation of the quantifier. *) val to_string : quantifier -> string diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c73e2f1d8..68d24d0a9 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1875,7 +1875,6 @@ void ast_manager::delete_node(ast * n) { while ((n = m_ast_table.pop_erase())) { - TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";); CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";); TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 146c7359f..71b35f914 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -454,23 +454,24 @@ namespace datatype { } void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) { + std::ostream& out = m_manager->trace_stream(); symbol const& family_name = m_manager->get_family_name(get_family_id()); for (constructor const* c : *m_defs[s]) { func_decl_ref f = c->instantiate(new_sort); const unsigned num_args = f->get_arity(); if (num_args == 0) continue; for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; + out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; ++m_id_counter; } const unsigned constructor_id = m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); + out << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; + out << " " << family_name << "#" << constructor_id - num_args + i; } - m_manager->trace_stream() << "\n"; + out << "\n"; ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; + out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; ++m_id_counter; m_axiom_bases.insert(f->get_name(), constructor_id + 4); std::ostringstream var_sorts; @@ -481,14 +482,14 @@ namespace datatype { unsigned i = 0; for (accessor const* a : *c) { func_decl_ref acc = a->instantiate(new_sort); - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; + out << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i + out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i << " " << family_name << "#" << m_id_counter - 1 << "\n"; ++m_id_counter; - m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 + out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 << " " << family_name << "#" << m_id_counter - 1 << "\n"; - m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; + out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; ++m_id_counter; ++i; } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 1b586b4b6..9390e21ee 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -583,6 +583,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; m().trace_stream() << "[end-of-instance]\n"; + m().trace_stream().flush(); } if (st != BR_DONE && st != BR_FAILED) { diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index f981270b6..e1d90516c 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -203,7 +203,7 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) { } tout << "Old: " << mk_ismt2_pp(get_entry(args)->get_result(), m_manager) << "\n"; ); - SASSERT(get_entry(args) == 0); + SASSERT(get_entry(args) == nullptr); func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r); if (!new_entry->args_are_values()) m_args_are_values = false; diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp index b85fed02d..c969cc559 100644 --- a/src/smt/smt_cg_table.cpp +++ b/src/smt/smt_cg_table.cpp @@ -22,81 +22,6 @@ Revision History: namespace smt { -#if 0 - unsigned cg_table::cg_hash::operator()(enode * n) const { - if (n->is_commutative()) { - return combine_hash(n->get_decl_id(), - n->get_arg(0)->get_root()->hash() * - n->get_arg(1)->get_root()->hash()); - } - else { - unsigned num = n->get_num_args(); - switch (num) { - case 0: UNREACHABLE(); return 0; - case 1: - return combine_hash(n->get_decl_id(), n->get_arg(0)->get_root()->hash()); - case 2: { - unsigned a = n->get_decl_id(); - unsigned b = n->get_arg(0)->get_root()->hash(); - unsigned c = n->get_arg(1)->get_root()->hash(); - mix(a,b,c); - return c; - } - default: - return get_composite_hash(n, n->get_num_args(), m_khasher, m_chasher); - } - } - } - - bool cg_table::cg_eq::operator()(enode * n1, enode * n2) const { -#if 0 - static unsigned counter = 0; - static unsigned failed = 0; - bool r = congruent(n1, n2, m_commutativity); - if (!r) - failed++; - counter++; - if (counter % 100000 == 0) - std::cout << "cg_eq: " << counter << " " << failed << "\n"; - return r; -#else - return congruent(n1, n2, m_commutativity); -#endif - } - - cg_table::cg_table(ast_manager & m): - m_manager(m), - m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, cg_hash(), cg_eq(m_commutativity)) { - } - - void cg_table::display(std::ostream & out) const { - out << "congruence table:\n"; - for (enode * n : m_table) { - out << mk_pp(n->get_owner(), m_manager) << "\n"; - } - } - - void cg_table::display_compact(std::ostream & out) const { - if (!m_table.empty()) { - out << "congruence table:\n"; - for (enode * n : m_table) { - out << "#" << n->get_owner()->get_id() << " "; - } - out << "\n"; - } - } - -#ifdef Z3DEBUG - bool cg_table::check_invariant() const { - for (enode * n : m_table) { - CTRACE("cg_table", !contains_ptr(n), tout << "#" << n->get_owner_id() << "\n";); - SASSERT(contains_ptr(n)); - } - return true; - } -#endif - -#else // one table per func_decl implementation unsigned cg_table::cg_hash::operator()(enode * n) const { SASSERT(n->get_decl()->is_flat_associative() || n->get_num_args() >= 3); @@ -222,18 +147,116 @@ namespace smt { } void cg_table::display(std::ostream & out) const { + for (auto const& kv : m_func_decl2id) { + void * t = m_tables[kv.m_value]; + out << mk_pp(kv.m_key, m_manager) << ": "; + switch (GET_TAG(t)) { + case UNARY: + display_unary(out, t); + break; + case BINARY: + display_binary(out, t); + break; + case BINARY_COMM: + display_binary_comm(out, t); + break; + case NARY: + display_nary(out, t); + break; + } + } } + void cg_table::display_binary(std::ostream& out, void* t) const { + binary_table* tb = UNTAG(binary_table*, t); + out << "b "; + for (enode* n : *tb) { + out << n->get_owner_id() << " " << cg_binary_hash()(n) << " "; + } + out << "\n"; + } + + void cg_table::display_binary_comm(std::ostream& out, void* t) const { + comm_table* tb = UNTAG(comm_table*, t); + out << "bc "; + for (enode* n : *tb) { + out << n->get_owner_id() << " "; + } + out << "\n"; + } + + void cg_table::display_unary(std::ostream& out, void* t) const { + unary_table* tb = UNTAG(unary_table*, t); + out << "un "; + for (enode* n : *tb) { + out << n->get_owner_id() << " "; + } + out << "\n"; + } + + void cg_table::display_nary(std::ostream& out, void* t) const { + table* tb = UNTAG(table*, t); + out << "nary "; + for (enode* n : *tb) { + out << n->get_owner_id() << " "; + } + out << "\n"; + } + + + enode_bool_pair cg_table::insert(enode * n) { + // it doesn't make sense to insert a constant. + SASSERT(n->get_num_args() > 0); + SASSERT(!m_manager.is_and(n->get_owner())); + SASSERT(!m_manager.is_or(n->get_owner())); + enode * n_prime; + void * t = get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, false); + case BINARY: + n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); + TRACE("cg_table", tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n"; + display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); + return enode_bool_pair(n_prime, false); + case BINARY_COMM: + m_commutativity = false; + n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, m_commutativity); + default: + n_prime = UNTAG(table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, false); + } + } + + void cg_table::erase(enode * n) { + SASSERT(n->get_num_args() > 0); + void * t = get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + UNTAG(unary_table*, t)->erase(n); + break; + case BINARY: + TRACE("cg_table", tout << "erase: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";); + UNTAG(binary_table*, t)->erase(n); + break; + case BINARY_COMM: + UNTAG(comm_table*, t)->erase(n); + break; + default: + UNTAG(table*, t)->erase(n); + break; + } + } + + void cg_table::display_compact(std::ostream & out) const { } -#ifdef Z3DEBUG bool cg_table::check_invariant() const { return true; } -#endif - -#endif }; diff --git a/src/smt/smt_cg_table.h b/src/smt/smt_cg_table.h index 4085ccc5f..78babf3b3 100644 --- a/src/smt/smt_cg_table.h +++ b/src/smt/smt_cg_table.h @@ -27,89 +27,6 @@ namespace smt { typedef std::pair enode_bool_pair; -#if 0 - /** - \brief Congruence table. - */ - class cg_table { - struct cg_khasher { - unsigned operator()(enode const * n) const { return n->get_decl_id(); } - }; - - struct cg_chasher { - unsigned operator()(enode const * n, unsigned idx) const { - return n->get_arg(idx)->get_root()->hash(); - } - }; - - struct cg_hash { - cg_khasher m_khasher; - cg_chasher m_chasher; - public: - unsigned operator()(enode * n) const; - }; - - struct cg_eq { - bool & m_commutativity; - cg_eq(bool & comm):m_commutativity(comm) {} - bool operator()(enode * n1, enode * n2) const; - }; - - typedef ptr_hashtable table; - - ast_manager & m_manager; - bool m_commutativity; //!< true if the last found congruence used commutativity - table m_table; - public: - cg_table(ast_manager & m); - - /** - \brief Try to insert n into the table. If the table already - contains an element n' congruent to n, then do nothing and - return n' and a boolean indicating whether n and n' are congruence - modulo commutativity, otherwise insert n and return (n,false). - */ - enode_bool_pair insert(enode * n) { - // it doesn't make sense to insert a constant. - SASSERT(n->get_num_args() > 0); - m_commutativity = false; - enode * n_prime = m_table.insert_if_not_there(n); - SASSERT(contains(n)); - return enode_bool_pair(n_prime, m_commutativity); - } - - void erase(enode * n) { - SASSERT(n->get_num_args() > 0); - m_table.erase(n); - SASSERT(!contains(n)); - } - - bool contains(enode * n) const { - return m_table.contains(n); - } - - enode * find(enode * n) const { - enode * r = 0; - return m_table.find(n, r) ? r : 0; - } - - bool contains_ptr(enode * n) const { - enode * n_prime; - return m_table.find(n, n_prime) && n == n_prime; - } - - void reset() { - m_table.reset(); - } - - void display(std::ostream & out) const; - - void display_compact(std::ostream & out) const; -#ifdef Z3DEBUG - bool check_invariant() const; -#endif - }; -#else // one table per function symbol /** @@ -137,9 +54,6 @@ namespace smt { struct cg_binary_hash { unsigned operator()(enode * n) const { SASSERT(n->get_num_args() == 2); - // too many collisions - // unsigned r = 17 + n->get_arg(0)->get_root()->hash(); - // return r * 31 + n->get_arg(1)->get_root()->hash(); return combine_hash(n->get_arg(0)->get_root()->hash(), n->get_arg(1)->get_root()->hash()); } }; @@ -149,23 +63,9 @@ namespace smt { SASSERT(n1->get_num_args() == 2); SASSERT(n2->get_num_args() == 2); SASSERT(n1->get_decl() == n2->get_decl()); -#if 1 return n1->get_arg(0)->get_root() == n2->get_arg(0)->get_root() && n1->get_arg(1)->get_root() == n2->get_arg(1)->get_root(); -#else - bool r = - n1->get_arg(0)->get_root() == n2->get_arg(0)->get_root() && - n1->get_arg(1)->get_root() == n2->get_arg(1)->get_root(); - static unsigned counter = 0; - static unsigned failed = 0; - if (!r) - failed++; - counter++; - if (counter % 100000 == 0) - std::cerr << "[cg_eq] " << counter << " " << failed << "\n"; - return r; -#endif } }; @@ -249,48 +149,9 @@ namespace smt { return n' and a boolean indicating whether n and n' are congruence modulo commutativity, otherwise insert n and return (n,false). */ - enode_bool_pair insert(enode * n) { - // it doesn't make sense to insert a constant. - SASSERT(n->get_num_args() > 0); - SASSERT(!m_manager.is_and(n->get_owner())); - SASSERT(!m_manager.is_or(n->get_owner())); - enode * n_prime; - void * t = get_table(n); - switch (static_cast(GET_TAG(t))) { - case UNARY: - n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, false); - case BINARY: - n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, false); - case BINARY_COMM: - m_commutativity = false; - n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, m_commutativity); - default: - n_prime = UNTAG(table*, t)->insert_if_not_there(n); - return enode_bool_pair(n_prime, false); - } - } + enode_bool_pair insert(enode * n); - void erase(enode * n) { - SASSERT(n->get_num_args() > 0); - void * t = get_table(n); - switch (static_cast(GET_TAG(t))) { - case UNARY: - UNTAG(unary_table*, t)->erase(n); - break; - case BINARY: - UNTAG(binary_table*, t)->erase(n); - break; - case BINARY_COMM: - UNTAG(comm_table*, t)->erase(n); - break; - default: - UNTAG(table*, t)->erase(n); - break; - } - } + void erase(enode * n); bool contains(enode * n) const { SASSERT(n->get_num_args() > 0); @@ -343,13 +204,19 @@ namespace smt { void display(std::ostream & out) const; + void display_binary(std::ostream& out, void* t) const; + + void display_binary_comm(std::ostream& out, void* t) const; + + void display_unary(std::ostream& out, void* t) const; + + void display_nary(std::ostream& out, void* t) const; + void display_compact(std::ostream & out) const; -#ifdef Z3DEBUG + bool check_invariant() const; -#endif }; -#endif }; #endif /* SMT_CG_TABLE_H_ */ diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5715e067d..63979e657 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -86,7 +86,8 @@ namespace smt { m_generation(0), m_last_search_result(l_undef), m_last_search_failure(UNKNOWN), - m_searching(false) { + m_searching(false), + m_propagating(false) { SASSERT(m_scope_lvl == 0); SASSERT(m_base_lvl == 0); @@ -131,8 +132,13 @@ namespace smt { return literal(v, lit.sign()); } + /** + \brief retrieve flag for when cancelation is possible. + Cancelation is not safe during propagation at base level because + congruences cannot be retracted to a consistent state. + */ bool context::get_cancel_flag() { - return !m_manager.limit().inc(); + return !m_manager.limit().inc() && !(at_base_level() && m_propagating); } void context::updt_params(params_ref const& p) { @@ -548,14 +554,10 @@ namespace smt { mark_as_relevant(r1); } - TRACE("add_eq", tout << "to trail\n";); - push_trail(add_eq_trail(r1, n1, r2->get_num_parents())); - TRACE("add_eq", tout << "qmanager add_eq\n";); m_qmanager->add_eq_eh(r1, r2); - TRACE("add_eq", tout << "merge theory_vars\n";); merge_theory_vars(n2, n1, js); // 'Proof' tree @@ -571,25 +573,6 @@ namespace smt { // r1 -> .. -> n1 -> n2 -> ... -> r2 -#if 0 - { - static unsigned counter = 0; - static unsigned num_adds = 0; - static unsigned num_bad_adds = 0; - num_adds++; - if (r1->get_class_size() <= r2->get_class_size() && - r1->m_parents.size() > r2->m_parents.size()) { - num_bad_adds++; - } - if (num_adds % 100000 == 0) { - verbose_stream() << "[add-eq]: " << num_bad_adds << " " << num_adds << " " - << static_cast(num_bad_adds)/static_cast(num_adds) << "\n"; - } - } -#endif - - - TRACE("add_eq", tout << "remove_parents_from_cg_table\n";); remove_parents_from_cg_table(r1); enode * curr = r1; @@ -600,11 +583,8 @@ namespace smt { while(curr != r1); SASSERT(r1->get_root() == r2); - - TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";); reinsert_parents_into_cg_table(r1, r2, n1, n2, js); - TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";); if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); @@ -632,25 +612,21 @@ namespace smt { void context::remove_parents_from_cg_table(enode * r1) { // Remove parents from the congruence table for (enode * parent : enode::parents(r1)) { -#if 0 - { - static unsigned num_eqs = 0; - static unsigned num_parents = 0; - static unsigned counter = 0; - if (parent->is_eq()) - num_eqs++; - num_parents++; - if (num_parents % 100000 == 0) { - verbose_stream() << "[remove-cg] " << num_eqs << " " << num_parents << " " - << static_cast(num_eqs)/static_cast(num_parents) << "\n"; - } - } -#endif - SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || - (!parent->is_true_eq() && parent->is_cgr() == m_cg_table.contains_ptr(parent)) || - (parent->is_true_eq() && !m_cg_table.contains_ptr(parent))); + CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";); + CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() && parent->is_cgr() && !m_cg_table.contains_ptr(parent), + tout << "cgr !contains " << parent->get_owner_id() << " " << mk_pp(parent->get_decl(), m_manager) << "\n"; + for (enode* n : enode::args(parent)) tout << n->get_root()->get_owner_id() << " " << n->get_root()->hash() << " "; + tout << "\n"; + tout << "contains: " << m_cg_table.contains(parent) << "\n"; + if (m_cg_table.contains(parent)) { + tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n"; + } + m_cg_table.display(tout); + ); + CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() && !parent->is_cgr() && m_cg_table.contains_ptr(parent), tout << "!cgr contains " << parent->get_owner_id() << "\n";); + SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || parent->is_true_eq() || parent->is_cgr() == m_cg_table.contains_ptr(parent)); + SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || !parent->is_true_eq() || !m_cg_table.contains_ptr(parent)); if (!parent->is_marked() && parent->is_cgr() && !parent->is_true_eq()) { - TRACE("add_eq_parents", tout << "add_eq removing: #" << parent->get_owner_id() << "\n";); SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent)); parent->set_mark(); if (parent->is_cgc_enabled()) { @@ -704,7 +680,6 @@ namespace smt { enode_bool_pair pair = m_cg_table.insert(parent); enode * parent_prime = pair.first; if (parent_prime == parent) { - TRACE("add_eq_parents", tout << "add_eq reinserting: #" << parent->get_owner_id() << "\n";); SASSERT(parent); SASSERT(parent->is_cgr()); SASSERT(m_cg_table.contains_ptr(parent)); @@ -983,7 +958,6 @@ namespace smt { for (; it != end; ++it) { enode * parent = *it; if (parent->is_cgc_enabled()) { - TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";); CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent), tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" << parent->get_owner_id() << ", parents: \n"; @@ -1011,14 +985,13 @@ namespace smt { for (enode * parent : enode::parents(r1)) { TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";); if (parent->is_cgc_enabled()) { - enode * cg = parent->m_cg; + enode * cg = parent->m_cg; if (!parent->is_true_eq() && - (parent == cg || // parent was root of the congruence class before and after the merge - !congruent(parent, cg) // parent was root of the congruence class before but not after the merge + (parent == cg || // parent was root of the congruence class before and after the merge + !congruent(parent, cg) // parent was root of the congruence class before but not after the merge )) { - TRACE("add_eq_parents", tout << "trying to reinsert\n";); - m_cg_table.insert(parent); - parent->m_cg = parent; + enode_bool_pair p = m_cg_table.insert(parent); + parent->m_cg = p.first; } } } @@ -1353,13 +1326,14 @@ namespace smt { \remark The method assign_eq adds a new entry on this queue. */ bool context::propagate_eqs() { - TRACE("add_eq", tout << m_eq_propagation_queue.size() << "\n";); - for (unsigned i = 0; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) { + unsigned i = 0; + for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) { new_eq & entry = m_eq_propagation_queue[i]; add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification); if (inconsistent()) return false; } + TRACE("add_eq", tout << m_eq_propagation_queue.size() << " " << i << "\n";); m_eq_propagation_queue.reset(); return true; } @@ -1728,6 +1702,7 @@ namespace smt { } bool context::propagate() { + flet _prop(m_propagating, true); TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";); while (true) { if (inconsistent()) @@ -4449,7 +4424,7 @@ namespace smt { void context::add_rec_funs_to_model() { ast_manager& m = m_manager; - SASSERT(m_model); + if (!m_model) return; for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) { expr* e = m_asserted_formulas.get_formula(i); if (is_quantifier(e)) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index d4d4ec6fb..42111c591 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -923,6 +923,7 @@ namespace smt { failure m_last_search_failure; ptr_vector m_incomplete_theories; //!< theories that failed to produce a model bool m_searching; + bool m_propagating; unsigned m_num_conflicts; unsigned m_num_conflicts_since_restart; unsigned m_num_conflicts_since_lemma_gc; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 065e5d952..767b9e06e 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -427,14 +427,8 @@ namespace smt { } tout << "\n"; tout << "value: #" << n->get_owner_id() << "\n" << mk_ismt2_pp(result, m_manager) << "\n";); - if (m_context->get_last_search_failure() == smt::THEORY) { - // if the theory solvers are incomplete, then we cannot assume the e-graph is close under congruence - if (fi->get_entry(args.c_ptr()) == nullptr) - fi->insert_new_entry(args.c_ptr(), result); - } - else { + if (fi->get_entry(args.c_ptr()) == nullptr) fi->insert_new_entry(args.c_ptr(), result); - } } } } diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 63c6d7417..b791991f2 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -137,5 +137,56 @@ namespace smt { theory::~theory() { } + + void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector> & used_enodes) { + ast_manager & m = get_manager(); + std::ostream& out = m.trace_stream(); + symbol const & family_name = m.get_family_name(get_family_id()); + if (pattern_id == UINT_MAX) { + out << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << family_name << "#"; + if (axiom_id != UINT_MAX) + out << axiom_id; + for (unsigned i = 0; i < num_bindings; ++i) { + out << " #" << bindings[i]->get_id(); + } + if (used_enodes.size() > 0) { + out << " ;"; + for (auto n : used_enodes) { + enode *substituted = std::get<1>(n); + SASSERT(std::get<0>(n) == nullptr); + out << " #" << substituted->get_owner_id(); + } + } + } else { + SASSERT(axiom_id != UINT_MAX); + obj_hashtable already_visited; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig != nullptr) { + quantifier_manager::log_justification_to_root(out, orig, already_visited, get_context(), get_manager()); + quantifier_manager::log_justification_to_root(out, substituted, already_visited, get_context(), get_manager()); + } + } + out << "[new-match] " << static_cast(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id; + for (unsigned i = 0; i < num_bindings; ++i) { + out << " #" << bindings[i]->get_id(); + } + out << " ;"; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig == nullptr) { + out << " #" << substituted->get_owner_id(); + } else { + out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; + } + } + } + out << "\n"; + out << "[instance] " << static_cast(nullptr) << " #" << r->get_id() << "\n"; + out.flush(); + } + }; diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index f1f304fa6..92aa87163 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -360,55 +360,15 @@ namespace smt { std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_owner()); } protected: - void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { - ast_manager & m = get_manager(); - symbol const & family_name = m.get_family_name(get_family_id()); - if (pattern_id == UINT_MAX) { - m.trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << family_name << "#"; - if (axiom_id != UINT_MAX) - m.trace_stream() << axiom_id; - for (unsigned i = 0; i < num_bindings; ++i) { - m.trace_stream() << " #" << bindings[i]->get_id(); - } - if (used_enodes.size() > 0) { - m.trace_stream() << " ;"; - for (auto n : used_enodes) { - enode *substituted = std::get<1>(n); - SASSERT(std::get<0>(n) == nullptr); - m.trace_stream() << " #" << substituted->get_owner_id(); - } - } - } else { - SASSERT(axiom_id != UINT_MAX); - obj_hashtable already_visited; - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig != nullptr) { - quantifier_manager::log_justification_to_root(m.trace_stream(), orig, already_visited, get_context(), get_manager()); - quantifier_manager::log_justification_to_root(m.trace_stream(), substituted, already_visited, get_context(), get_manager()); - } - } - m.trace_stream() << "[new-match] " << static_cast(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id; - for (unsigned i = 0; i < num_bindings; ++i) { - m.trace_stream() << " #" << bindings[i]->get_id(); - } - m.trace_stream() << " ;"; - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig == nullptr) { - m.trace_stream() << " #" << substituted->get_owner_id(); - } else { - m.trace_stream() << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; - } - } - } - m.trace_stream() << "\n"; - m.trace_stream() << "[instance] " << static_cast(nullptr) << " #" << r->get_id() << "\n"; - } + void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, + app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, + const vector> & used_enodes = vector>()); - void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); } + void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, + app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, + const vector> & used_enodes = vector>()) { + log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); + } void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) { vector> used_enodes; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 736218bc4..b2207199c 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -97,30 +97,6 @@ namespace smt { // This will also force the creation of all bits for x. enode * first_arg_enode = ctx.get_enode(first_arg); get_var(first_arg_enode); -#if 0 - // constant axiomatization moved to catch all case in the end of function. - - // numerals are not blasted into bit2bool, so we do this directly. - rational val; - unsigned sz; - if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) { - - TRACE("bv", tout << "bit2bool constants\n";); - theory_var v = first_arg_enode->get_th_var(get_id()); - app* owner = first_arg_enode->get_owner(); - for (unsigned i = 0; i < sz; ++i) { - app* e = mk_bit2bool(owner, i); - ctx.internalize(e, true); - } - m_bits[v].reset(); - rational bit; - for (unsigned i = 0; i < sz; ++i) { - div(val, rational::power_of_two(i), bit); - mod(bit, rational(2), bit); - m_bits[v].push_back(bit.is_zero()?false_literal:true_literal); - } - } -#endif } enode * arg = ctx.get_enode(first_arg); @@ -144,6 +120,13 @@ namespace smt { unsigned idx = n->get_decl()->get_parameter(0).get_int(); SASSERT(a->m_occs == 0); a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); +#if 0 + // possible fix for #2162, but effect of fix needs to be checked. + if (idx < m_bits[v_arg].size()) { + ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true)); + ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false)); + } +#endif } // axiomatize bit2bool on constants. rational val; @@ -782,6 +765,7 @@ namespace smt { bits.swap(new_bits); \ } \ init_bits(e, bits); \ + TRACE("bv", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \ } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index f26791639..dd1b302e1 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -139,7 +139,7 @@ namespace smt { expr * acc = m.mk_app(d, n->get_owner()); args.push_back(acc); } - expr * mk = m.mk_app(c, args.size(), args.c_ptr()); + expr_ref mk(m.mk_app(c, args.size(), args.c_ptr()), m); if (m.has_trace_stream()) { app_ref body(m); body = m.mk_eq(n->get_owner(), mk); @@ -175,7 +175,7 @@ namespace smt { unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0; unsigned i = 0; for (func_decl * acc : accessors) { - app * acc_app = m.mk_app(acc, n->get_owner()); + app_ref acc_app(m.mk_app(acc, n->get_owner()), m); enode * arg = n->get_arg(i); if (m.has_trace_stream()) { app_ref body(m); @@ -239,7 +239,7 @@ namespace smt { ctx.internalize(acc_app, false); arg = ctx.get_enode(acc_app); } - app * acc_own = m.mk_app(acc1, own); + app_ref acc_own(m.mk_app(acc1, own), m); if (m.has_trace_stream()) { app_ref body(m); body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own)); @@ -249,8 +249,7 @@ namespace smt { if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // update_field is identity if 'n' is not created by a matching constructor. - app_ref imp(m); - imp = m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1)); + app_ref imp(m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1)), m); if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n); assert_eq_axiom(n, arg1, ~is_con); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; diff --git a/src/util/trace.cpp b/src/util/trace.cpp index e4b210021..5e2930999 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -20,6 +20,7 @@ Revision History: #include "util/str_hashtable.h" #ifdef _TRACE + std::ofstream tout(".z3-trace"); static bool g_enable_all_trace_tags = false;