mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
ce8263cf27
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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";);
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -583,6 +583,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
m().trace_stream() << "[instance] " << static_cast<void *>(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) {
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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<enode *, cg_khasher, cg_chasher>(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<table_kind>(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<table_kind>(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
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -27,89 +27,6 @@ namespace smt {
|
|||
|
||||
typedef std::pair<enode *, bool> 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<enode, cg_hash, cg_eq> 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<table_kind>(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<table_kind>(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_ */
|
||||
|
|
|
@ -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<double>(num_bad_adds)/static_cast<double>(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<double>(num_eqs)/static_cast<double>(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<bool> _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)) {
|
||||
|
|
|
@ -923,6 +923,7 @@ namespace smt {
|
|||
failure m_last_search_failure;
|
||||
ptr_vector<theory> 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;
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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<std::tuple<enode *, enode *>> & 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<void *>(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<enode> 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<void *>(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<void *>(nullptr) << " #" << r->get_id() << "\n";
|
||||
out.flush();
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -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<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
|
||||
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<void *>(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<enode> 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<void *>(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<void *>(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<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>());
|
||||
|
||||
void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); }
|
||||
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<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
|
||||
log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes);
|
||||
}
|
||||
|
||||
void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) {
|
||||
vector<std::tuple<enode *, enode *>> used_enodes;
|
||||
|
|
|
@ -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";); \
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -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";
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue