From 931dbd5933d77ba4a63b63259a339fa03410f661 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Mar 2018 13:37:04 -0700 Subject: [PATCH] remove python doc test Signed-off-by: Nikolaj Bjorner --- scripts/vsts-vs2013.cmd | 14 +++---- src/smt/theory_str.cpp | 87 +++++++++++++++++----------------------- src/smt/theory_str.h | 3 +- src/util/hashtable.h | 17 ++++---- src/util/obj_hashtable.h | 3 ++ 5 files changed, 55 insertions(+), 69 deletions(-) diff --git a/scripts/vsts-vs2013.cmd b/scripts/vsts-vs2013.cmd index 203c2668e..1676f3e2d 100644 --- a/scripts/vsts-vs2013.cmd +++ b/scripts/vsts-vs2013.cmd @@ -8,13 +8,13 @@ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BIN nmake if ERRORLEVEL 1 exit 1 -echo "Test python bindings" -pushd python -python z3test.py z3 -if ERRORLEVEL 1 exit 1 -python z3test.py z3num -if ERRORLEVEL 1 exit 1 -popd +rem echo "Test python bindings" +rem pushd python +rem python z3test.py z3 +rem if ERRORLEVEL 1 exit 1 +rem python z3test.py z3num +rem if ERRORLEVEL 1 exit 1 +rem popd echo "Build and run examples" nmake cpp_example diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 69cf80de6..f61293a5f 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -169,6 +169,8 @@ namespace smt { } void theory_str::assert_axiom(expr * _e) { + if (_e == nullptr) + return; if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = true; } @@ -6914,10 +6916,8 @@ namespace smt { if (!map_effectively_empty) { map_effectively_empty = true; - ptr_vector indicator_set = fvar_lenTester_map[v]; - for (ptr_vector::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { - expr * indicator = *it; - if (internal_variable_set.find(indicator) != internal_variable_set.end()) { + for (expr * indicator : fvar_lenTester_map[v]) { + if (internal_variable_set.contains(indicator)) { map_effectively_empty = false; break; } @@ -8977,12 +8977,12 @@ namespace smt { CTRACE("str", needToAssignFreeVars, tout << "Need to assign values to the following free variables:" << std::endl; - for (std::set::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) { - tout << mk_ismt2_pp(*itx, m) << std::endl; + for (expr* v : free_variables) { + tout << mk_ismt2_pp(v, m) << std::endl; } tout << "freeVar_map has the following entries:" << std::endl; - for (std::map::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { - expr * var = fvIt->first; + for (auto const& kv : freeVar_map) { + expr * var = kv.first; tout << mk_ismt2_pp(var, m) << std::endl; } ); @@ -9360,7 +9360,7 @@ namespace smt { // check whether any value tester is actually in scope TRACE("str", tout << "checking scope of previous value testers" << std::endl;); bool map_effectively_empty = true; - if (fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { + if (fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { // there's *something* in the map, but check its scope svector > entries = fvar_valueTester_map[freeVar][len]; for (svector >::iterator it = entries.begin(); it != entries.end(); ++it) { @@ -9721,8 +9721,8 @@ namespace smt { int dist = opt_LCMUnrollStep; expr_ref_vector litems(mgr); expr_ref moreAst(mk_string("more"), mgr); - for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { - expr_ref item(ctx.mk_eq_atom(var, *itor), mgr); + for (expr * e : unrolls) { + expr_ref item(ctx.mk_eq_atom(var, e), mgr); TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); litems.push_back(item); } @@ -9731,10 +9731,8 @@ namespace smt { ptr_vector outOfScopeTesters; - for (ptr_vector::iterator it = unroll_tries_map[var][unrolls].begin(); - it != unroll_tries_map[var][unrolls].end(); ++it) { - expr * tester = *it; - bool inScope = (internal_unrollTest_vars.find(tester) != internal_unrollTest_vars.end()); + for (expr * tester : unroll_tries_map[var][unrolls]) { + bool inScope = internal_unrollTest_vars.contains(tester); TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) << (inScope ? " in scope" : " out of scope") << std::endl;); @@ -9743,12 +9741,10 @@ namespace smt { } } - for (ptr_vector::iterator it = outOfScopeTesters.begin(); - it != outOfScopeTesters.end(); ++it) { - unroll_tries_map[var][unrolls].erase(*it); + for (expr* e : outOfScopeTesters) { + unroll_tries_map[var][unrolls].erase(e); } - if (unroll_tries_map[var][unrolls].size() == 0) { unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var()); } @@ -10265,9 +10261,8 @@ namespace smt { // assume empty and find a counterexample map_effectively_empty = true; ptr_vector indicator_set = fvar_lenTester_map[freeVar]; - for (ptr_vector::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { - expr * indicator = *it; - if (internal_variable_set.find(indicator) != internal_variable_set.end()) { + for (expr * indicator : indicator_set) { + if (internal_variable_set.contains(indicator)) { TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) << " in fvar_lenTester_map[freeVar]" << std::endl;); map_effectively_empty = false; @@ -10437,14 +10432,14 @@ namespace smt { void theory_str::process_free_var(std::map & freeVar_map) { context & ctx = get_context(); - std::set eqcRepSet; - std::set leafVarSet; - std::map > aloneVars; + obj_hashtable eqcRepSet; + obj_hashtable leafVarSet; + std::map > aloneVars; - for (std::map::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { - expr * freeVar = fvIt->first; + for (auto const& kv : freeVar_map) { + expr * freeVar = kv.first; // skip all regular expression vars - if (regex_variable_set.find(freeVar) != regex_variable_set.end()) { + if (regex_variable_set.contains(freeVar)) { continue; } @@ -10454,10 +10449,10 @@ namespace smt { get_var_in_eqc(freeVar, eqVarSet); bool duplicated = false; expr * dupVar = nullptr; - for (std::set::iterator itorEqv = eqVarSet.begin(); itorEqv != eqVarSet.end(); itorEqv++) { - if (eqcRepSet.find(*itorEqv) != eqcRepSet.end()) { + for (expr* eq : eqVarSet) { + if (eqcRepSet.contains(eq)) { duplicated = true; - dupVar = *itorEqv; + dupVar = eq; break; } } @@ -10470,13 +10465,9 @@ namespace smt { } } - for (std::set::iterator fvIt = eqcRepSet.begin(); fvIt != eqcRepSet.end(); fvIt++) { - bool standAlone = true; - expr * freeVar = *fvIt; + for (expr * freeVar : eqcRepSet) { // has length constraint initially - if (input_var_in_len.find(freeVar) != input_var_in_len.end()) { - standAlone = false; - } + bool standAlone = !input_var_in_len.contains(freeVar); // iterate parents if (standAlone) { // I hope this works! @@ -10507,25 +10498,19 @@ namespace smt { } } - for(std::set::iterator itor1 = leafVarSet.begin(); - itor1 != leafVarSet.end(); ++itor1) { - expr * toAssert = gen_len_val_options_for_free_var(*itor1, nullptr, ""); + for (expr* lv : leafVarSet) { + expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, ""); // gen_len_val_options_for_free_var() can legally return NULL, // as methods that it calls may assert their own axioms instead. - if (toAssert != nullptr) { - assert_axiom(toAssert); - } + if (toAssert) assert_axiom(toAssert); + } - for (std::map >::iterator mItor = aloneVars.begin(); - mItor != aloneVars.end(); ++mItor) { - std::set::iterator itor2 = mItor->second.begin(); - for(; itor2 != mItor->second.end(); ++itor2) { - expr * toAssert = gen_len_val_options_for_free_var(*itor2, nullptr, ""); + for (auto const& kv : aloneVars) { + for (expr* av : kv.second) { + expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, ""); // same deal with returning a NULL axiom here - if(toAssert != nullptr) { - assert_axiom(toAssert); - } + if (toAssert) assert_axiom(toAssert); } } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 508a1c905..0a8495b14 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -295,7 +295,8 @@ protected: obj_hashtable input_var_in_len; obj_map fvar_len_count_map; - std::map > fvar_lenTester_map; + // std::map > fvar_lenTester_map; + obj_map > fvar_lenTester_map; obj_map lenTester_fvar_map; // TBD: need to replace by obj_map for determinism diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 742438814..4dc05fe4d 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -600,9 +600,8 @@ public: core_hashtable& operator|=(core_hashtable const& other) { if (this == &other) return *this; - iterator i = other.begin(), e = other.end(); - for (; i != e; ++i) { - insert(*i); + for (const data& d : other) { + insert(d); } return *this; } @@ -610,10 +609,9 @@ public: core_hashtable& operator&=(core_hashtable const& other) { if (this == &other) return *this; core_hashtable copy(*this); - iterator i = copy.begin(), e = copy.end(); - for (; i != e; ++i) { - if (!other.contains(*i)) { - remove(*i); + for (const data& d : copy) { + if (!other.contains(d)) { + remove(d); } } return *this; @@ -622,9 +620,8 @@ public: core_hashtable& operator=(core_hashtable const& other) { if (this == &other) return *this; reset(); - iterator i = other.begin(), e = other.end(); - for (; i != e; ++i) { - insert(*i); + for (const data& d : e) { + insert(d); } return *this; } diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 8826e8b76..d042779a8 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -174,6 +174,9 @@ public: value & find(key * k) { obj_map_entry * e = find_core(k); + if (!e) { + e = insert_if_not_there2(k, value()); + } SASSERT(e); return e->get_data().m_value; }