mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
f59d4c6ac0
|
@ -368,9 +368,6 @@ class AstRef(Z3PPObject):
|
|||
def __copy__(self):
|
||||
return self.translate(self.ctx)
|
||||
|
||||
def __deepcopy__(self):
|
||||
return self.translate(self.ctx)
|
||||
|
||||
def hash(self):
|
||||
"""Return a hashcode for the `self`.
|
||||
|
||||
|
|
|
@ -31,7 +31,7 @@ extern "C" {
|
|||
/** @name Algebraic Numbers */
|
||||
/*@{*/
|
||||
/**
|
||||
\brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
|
||||
\brief Return Z3_TRUE if \c a can be used as value in the Z3 real algebraic
|
||||
number package.
|
||||
|
||||
def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
|
|
|
@ -4350,7 +4350,7 @@ extern "C" {
|
|||
Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return true if the give AST is a real algebraic number.
|
||||
\brief Return true if the given AST is a real algebraic number.
|
||||
|
||||
def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
|
|
|
@ -43,11 +43,10 @@ namespace smt {
|
|||
return out << "RESOURCE_LIMIT";
|
||||
case THEORY:
|
||||
if (!m_incomplete_theories.empty()) {
|
||||
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
|
||||
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
|
||||
for (bool first = true; it != end; ++it) {
|
||||
bool first = true;
|
||||
for (theory* th : m_incomplete_theories) {
|
||||
if (first) first = false; else out << " ";
|
||||
out << (*it)->get_name();
|
||||
out << th->get_name();
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -173,12 +172,10 @@ namespace smt {
|
|||
|
||||
void context::display_binary_clauses(std::ostream & out) const {
|
||||
bool first = true;
|
||||
vector<watch_list>::const_iterator it = m_watches.begin();
|
||||
vector<watch_list>::const_iterator end = m_watches.end();
|
||||
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
|
||||
literal l1 = to_literal(l_idx);
|
||||
unsigned l_idx = 0;
|
||||
for (watch_list const& wl : m_watches) {
|
||||
literal l1 = to_literal(l_idx++);
|
||||
literal neg_l1 = ~l1;
|
||||
watch_list const & wl = *it;
|
||||
literal const * it2 = wl.begin_literals();
|
||||
literal const * end2 = wl.end_literals();
|
||||
for (; it2 != end2; ++it2) {
|
||||
|
@ -291,10 +288,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::display_theories(std::ostream & out) const {
|
||||
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
|
||||
ptr_vector<theory>::const_iterator end = m_theory_set.end();
|
||||
for (; it != end; ++it) {
|
||||
theory * th = *it;
|
||||
for (theory* th : m_theory_set) {
|
||||
th->display(out);
|
||||
}
|
||||
}
|
||||
|
@ -393,10 +387,8 @@ namespace smt {
|
|||
#endif
|
||||
m_qmanager->collect_statistics(st);
|
||||
m_asserted_formulas.collect_statistics(st);
|
||||
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
|
||||
ptr_vector<theory>::const_iterator end = m_theory_set.end();
|
||||
for (; it != end; ++it) {
|
||||
(*it)->collect_statistics(st);
|
||||
for (theory* th : m_theory_set) {
|
||||
th->collect_statistics(st);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -498,10 +490,7 @@ namespace smt {
|
|||
*/
|
||||
void context::display_normalized_enodes(std::ostream & out) const {
|
||||
out << "normalized enodes:\n";
|
||||
ptr_vector<enode>::const_iterator it = m_enodes.begin();
|
||||
ptr_vector<enode>::const_iterator end = m_enodes.end();
|
||||
for (; it != end; ++it) {
|
||||
enode * n = *it;
|
||||
for (enode * n : m_enodes) {
|
||||
out << "#";
|
||||
out.width(5);
|
||||
out << std::left << n->get_owner_id() << " #";
|
||||
|
@ -532,28 +521,23 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::display_enodes_lbls(std::ostream & out) const {
|
||||
ptr_vector<enode>::const_iterator it = m_enodes.begin();
|
||||
ptr_vector<enode>::const_iterator end = m_enodes.end();
|
||||
for (; it != end; ++it) {
|
||||
enode * n = *it;
|
||||
for (enode* n : m_enodes) {
|
||||
n->display_lbls(out);
|
||||
}
|
||||
}
|
||||
|
||||
void context::display_decl2enodes(std::ostream & out) const {
|
||||
out << "decl2enodes:\n";
|
||||
vector<enode_vector>::const_iterator it1 = m_decl2enodes.begin();
|
||||
vector<enode_vector>::const_iterator end1 = m_decl2enodes.end();
|
||||
for (unsigned id = 0; it1 != end1; ++it1, ++id) {
|
||||
enode_vector const & v = *it1;
|
||||
unsigned id = 0;
|
||||
for (enode_vector const& v : m_decl2enodes) {
|
||||
if (!v.empty()) {
|
||||
out << "id " << id << " ->";
|
||||
enode_vector::const_iterator it2 = v.begin();
|
||||
enode_vector::const_iterator end2 = v.end();
|
||||
for (; it2 != end2; ++it2)
|
||||
out << " #" << (*it2)->get_owner_id();
|
||||
for (enode* n : v) {
|
||||
out << " #" << n->get_owner_id();
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
++id;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -288,10 +288,9 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
static void cut_vars_map_copy(std::map<expr*, int> & dest, std::map<expr*, int> & src) {
|
||||
std::map<expr*, int>::iterator itor = src.begin();
|
||||
for (; itor != src.end(); itor++) {
|
||||
dest[itor->first] = 1;
|
||||
static void cut_vars_map_copy(obj_map<expr, int> & dest, obj_map<expr, int> & src) {
|
||||
for (auto const& kv : src) {
|
||||
dest.insert(kv.m_key, 1);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -306,9 +305,8 @@ namespace smt {
|
|||
return false;
|
||||
}
|
||||
|
||||
std::map<expr*, int>::iterator itor = cut_var_map[n1].top()->vars.begin();
|
||||
for (; itor != cut_var_map[n1].top()->vars.end(); ++itor) {
|
||||
if (cut_var_map[n2].top()->vars.find(itor->first) != cut_var_map[n2].top()->vars.end()) {
|
||||
for (auto const& kv : cut_var_map[n1].top()->vars) {
|
||||
if (cut_var_map[n2].top()->vars.contains(kv.m_key)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
@ -323,7 +321,7 @@ namespace smt {
|
|||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
varInfo->vars.insert(node, 1);
|
||||
cut_var_map.insert(baseNode, std::stack<T_cut*>());
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
|
||||
|
@ -332,7 +330,7 @@ namespace smt {
|
|||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
varInfo->vars.insert(node, 1);
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
|
||||
} else {
|
||||
|
@ -341,11 +339,11 @@ namespace smt {
|
|||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
|
||||
varInfo->vars[node] = 1;
|
||||
varInfo->vars.insert(node, 1);
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
|
||||
} else if (cut_var_map[baseNode].top()->level == slevel) {
|
||||
cut_var_map[baseNode].top()->vars[node] = 1;
|
||||
cut_var_map[baseNode].top()->vars.insert(node, 1);
|
||||
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
|
||||
} else {
|
||||
get_manager().raise_exception("entered illegal state during add_cut_info_one_node()");
|
||||
|
@ -2572,9 +2570,8 @@ namespace smt {
|
|||
if (cut_var_map.contains(node)) {
|
||||
if (!cut_var_map[node].empty()) {
|
||||
xout << "[" << cut_var_map[node].top()->level << "] ";
|
||||
std::map<expr*, int>::iterator itor = cut_var_map[node].top()->vars.begin();
|
||||
for (; itor != cut_var_map[node].top()->vars.end(); ++itor) {
|
||||
xout << mk_pp(itor->first, m) << ", ";
|
||||
for (auto const& kv : cut_var_map[node].top()->vars) {
|
||||
xout << mk_pp(kv.m_key, m) << ", ";
|
||||
}
|
||||
xout << std::endl;
|
||||
}
|
||||
|
|
|
@ -77,25 +77,8 @@ public:
|
|||
void register_value(expr * n) override { /* Ignore */ }
|
||||
};
|
||||
|
||||
// rather than modify obj_pair_map I inherit from it and add my own helper methods
|
||||
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
|
||||
public:
|
||||
expr * operator[](std::pair<expr*, expr*> key) const {
|
||||
expr * value;
|
||||
bool found = this->find(key.first, key.second, value);
|
||||
if (found) {
|
||||
return value;
|
||||
} else {
|
||||
TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
bool contains(std::pair<expr*, expr*> key) const {
|
||||
expr * unused;
|
||||
return this->find(key.first, key.second, unused);
|
||||
}
|
||||
};
|
||||
// NSB: added operator[] and contains to obj_pair_hashtable
|
||||
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
|
||||
|
||||
template<typename Ctx>
|
||||
class binary_search_trail : public trail<Ctx> {
|
||||
|
@ -169,7 +152,7 @@ class theory_str : public theory {
|
|||
struct T_cut
|
||||
{
|
||||
int level;
|
||||
std::map<expr*, int> vars;
|
||||
obj_map<expr, int> vars;
|
||||
|
||||
T_cut() {
|
||||
level = -100;
|
||||
|
@ -292,8 +275,8 @@ protected:
|
|||
int tmpXorVarCount;
|
||||
int tmpLenTestVarCount;
|
||||
int tmpValTestVarCount;
|
||||
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
|
||||
|
||||
// obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
|
||||
std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
|
||||
bool avoidLoopCut;
|
||||
bool loopDetected;
|
||||
obj_map<expr, std::stack<T_cut*> > cut_var_map;
|
||||
|
@ -312,9 +295,11 @@ protected:
|
|||
obj_hashtable<expr> input_var_in_len;
|
||||
|
||||
obj_map<expr, unsigned int> fvar_len_count_map;
|
||||
// TBD: need to replace by obj_map for determinism
|
||||
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
|
||||
obj_map<expr, expr*> lenTester_fvar_map;
|
||||
|
||||
// TBD: need to replace by obj_map for determinism
|
||||
std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
|
||||
std::map<expr*, expr*> valueTester_fvar_map;
|
||||
|
||||
|
@ -322,8 +307,10 @@ protected:
|
|||
|
||||
// This can't be an expr_ref_vector because the constructor is wrong,
|
||||
// we would need to modify the allocator so we pass in ast_manager
|
||||
// TBD: need to replace by obj_map for determinism
|
||||
std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
|
||||
std::map<expr*, expr*> unroll_var_map;
|
||||
// TBD: need to replace by obj_pair_map for determinism
|
||||
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
|
||||
|
||||
expr_ref_vector contains_map;
|
||||
|
@ -332,9 +319,10 @@ protected:
|
|||
//obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
|
||||
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
|
||||
|
||||
// TBD: do a curried map for determinism.
|
||||
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
|
||||
// TBD: need to replace by obj_map for determinism
|
||||
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
|
||||
|
||||
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
|
||||
|
||||
svector<char> char_set;
|
||||
|
|
|
@ -160,10 +160,23 @@ public:
|
|||
}
|
||||
return (nullptr != e);
|
||||
}
|
||||
|
||||
Value const & find(Key1 * k1, Key2 * k2) const {
|
||||
entry * e = find_core(k1, k2);
|
||||
return e->get_data().get_value();
|
||||
}
|
||||
|
||||
Value const& operator[](std::pair<Key1 *, Key2 *> const& key) const {
|
||||
return find(key.first, key.second);
|
||||
}
|
||||
|
||||
bool contains(Key1 * k1, Key2 * k2) const {
|
||||
return find_core(k1, k2) != nullptr;
|
||||
}
|
||||
|
||||
bool contains(std::pair<Key1 *, Key2 *> const& key) const {
|
||||
return contains(key.first, key.second);
|
||||
}
|
||||
|
||||
void erase(Key1 * k1, Key2 * k2) {
|
||||
m_table.remove(key_data(k1, k2));
|
||||
|
|
Loading…
Reference in a new issue