From e4cab7bc834b81c8f4d0dcf3fd62668f61e916a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Filipe=20Gon=C3=A7alves?= Date: Fri, 16 Mar 2018 22:04:39 +1000 Subject: [PATCH 1/4] Fix #1540 Remove extraneous function Remove extra __deepcopy__ function definition that shadows working implementation. --- src/api/python/z3/z3.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e68d7280d..d4ff556fe 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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`. From 0a0b7a9635d416d117b488639666d25d6b5491be Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 16 Mar 2018 20:56:06 +0700 Subject: [PATCH 2/4] Fix minor issues in docs. --- src/api/z3_algebraic.h | 2 +- src/api/z3_api.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h index faa41bfea..49c61afef 100644 --- a/src/api/z3_algebraic.h +++ b/src/api/z3_algebraic.h @@ -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))) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 88d6aa1cf..87bb4d818 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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))) */ From 86d3bbe6cb8815a20bee5ee29caff12dac9f5202 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Mar 2018 07:46:27 -0700 Subject: [PATCH 3/4] added TODO markers in theory_str.h for moving to obj_map, remove include of stdbool for now Signed-off-by: Nikolaj Bjorner --- src/api/z3.h | 1 - src/smt/smt_context_pp.cpp | 50 ++++++++++++----------------------- src/smt/theory_str.cpp | 17 +++++------- src/smt/theory_str.h | 34 ++++++++---------------- src/util/obj_pair_hashtable.h | 13 +++++++++ 5 files changed, 48 insertions(+), 67 deletions(-) diff --git a/src/api/z3.h b/src/api/z3.h index b29f1d6ba..e08b0c073 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -22,7 +22,6 @@ Notes: #define Z3_H_ #include -#include #include "z3_macros.h" #include "z3_api.h" #include "z3_ast_containers.h" diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index e883e0a09..f072a1d13 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -43,11 +43,10 @@ namespace smt { return out << "RESOURCE_LIMIT"; case THEORY: if (!m_incomplete_theories.empty()) { - ptr_vector::const_iterator it = m_incomplete_theories.begin(); - ptr_vector::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::const_iterator it = m_watches.begin(); - vector::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::const_iterator it = m_theory_set.begin(); - ptr_vector::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::const_iterator it = m_theory_set.begin(); - ptr_vector::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::const_iterator it = m_enodes.begin(); - ptr_vector::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::const_iterator it = m_enodes.begin(); - ptr_vector::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::const_iterator it1 = m_decl2enodes.begin(); - 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; } } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0016b8f36..30092097a 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -288,10 +288,9 @@ namespace smt { } } - static void cut_vars_map_copy(std::map & dest, std::map & src) { - std::map::iterator itor = src.begin(); - for (; itor != src.end(); itor++) { - dest[itor->first] = 1; + static void cut_vars_map_copy(obj_map & dest, obj_map & src) { + for (auto const& kv : src) { + dest.insert(kv.m_key, 1); } } @@ -306,9 +305,8 @@ namespace smt { return false; } - std::map::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; } } @@ -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::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; } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 64ede71b5..09d6498a4 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -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 { -public: - expr * operator[](std::pair 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 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 {}; template class binary_search_trail : public trail { @@ -169,7 +152,7 @@ class theory_str : public theory { struct T_cut { int level; - std::map vars; + obj_map vars; T_cut() { level = -100; @@ -292,8 +275,8 @@ protected: int tmpXorVarCount; int tmpLenTestVarCount; int tmpValTestVarCount; - std::map, std::map > varForBreakConcat; - + // obj_pair_map > varForBreakConcat; + std::map, std::map > varForBreakConcat; bool avoidLoopCut; bool loopDetected; obj_map > cut_var_map; @@ -312,9 +295,11 @@ protected: obj_hashtable input_var_in_len; obj_map fvar_len_count_map; + // TBD: need to replace by obj_map for determinism std::map > fvar_lenTester_map; obj_map lenTester_fvar_map; + // TBD: need to replace by obj_map for determinism std::map > > > fvar_valueTester_map; std::map 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, ptr_vector > > unroll_tries_map; std::map unroll_var_map; + // TBD: need to replace by obj_pair_map for determinism std::map, expr*> concat_eq_unroll_ast_map; expr_ref_vector contains_map; @@ -332,9 +319,10 @@ protected: //obj_map > contain_pair_idx_map; std::map > > contain_pair_idx_map; + // TBD: do a curried map for determinism. std::map, expr*> regex_in_bool_map; + // TBD: need to replace by obj_map for determinism std::map > regex_in_var_reg_str_map; - std::map regex_nfa_cache; // Regex term --> NFA svector char_set; diff --git a/src/util/obj_pair_hashtable.h b/src/util/obj_pair_hashtable.h index f002a7807..2b8924e9f 100644 --- a/src/util/obj_pair_hashtable.h +++ b/src/util/obj_pair_hashtable.h @@ -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 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 const& key) const { + return contains(key.first, key.second); + } void erase(Key1 * k1, Key2 * k2) { m_table.remove(key_data(k1, k2)); From b12a1caa0759052380d60fbd1f71a5d8436ac047 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Mar 2018 09:05:44 -0700 Subject: [PATCH 4/4] fix build Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 30092097a..e1340c301 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -321,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()); 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;); @@ -330,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 { @@ -339,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()");