mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

remove python doc test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-20 13:37:04 -07:00
parent 8c4ea7983f
commit 931dbd5933
5 changed files with 55 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
scripts/vsts-vs2013.cmd
View file

@ -8,13 +8,13 @@ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BIN
nmake nmake
if ERRORLEVEL 1 exit 1 if ERRORLEVEL 1 exit 1
echo "Test python bindings" rem echo "Test python bindings"
pushd python rem pushd python
python z3test.py z3 rem python z3test.py z3
if ERRORLEVEL 1 exit 1 rem if ERRORLEVEL 1 exit 1
python z3test.py z3num rem python z3test.py z3num
if ERRORLEVEL 1 exit 1 rem if ERRORLEVEL 1 exit 1
popd rem popd
echo "Build and run examples" echo "Build and run examples"
nmake cpp_example nmake cpp_example

87
src/smt/theory_str.cpp
View file

@ -169,6 +169,8 @@ namespace smt {
} }
void theory_str::assert_axiom(expr * _e) { void theory_str::assert_axiom(expr * _e) {
if (_e == nullptr)
return;
if (opt_VerifyFinalCheckProgress) { if (opt_VerifyFinalCheckProgress) {
finalCheckProgressIndicator = true; finalCheckProgressIndicator = true;
} }
@ -6914,10 +6916,8 @@ namespace smt {
if (!map_effectively_empty) { if (!map_effectively_empty) {
map_effectively_empty = true; map_effectively_empty = true;
ptr_vector<expr> indicator_set = fvar_lenTester_map[v]; for (expr * indicator : fvar_lenTester_map[v]) {
for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { if (internal_variable_set.contains(indicator)) {
expr * indicator = *it;
if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
map_effectively_empty = false; map_effectively_empty = false;
break; break;
} }
@ -8977,12 +8977,12 @@ namespace smt {
CTRACE("str", needToAssignFreeVars, CTRACE("str", needToAssignFreeVars,
tout << "Need to assign values to the following free variables:" << std::endl; tout << "Need to assign values to the following free variables:" << std::endl;
for (std::set<expr*>::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) { for (expr* v : free_variables) {
tout << mk_ismt2_pp(*itx, m) << std::endl; tout << mk_ismt2_pp(v, m) << std::endl;
} }
tout << "freeVar_map has the following entries:" << std::endl; tout << "freeVar_map has the following entries:" << std::endl;
for (std::map<expr*, int>::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { for (auto const& kv : freeVar_map) {
expr * var = fvIt->first; expr * var = kv.first;
tout << mk_ismt2_pp(var, m) << std::endl; tout << mk_ismt2_pp(var, m) << std::endl;
} }
); );
@ -9360,7 +9360,7 @@ namespace smt {
// check whether any value tester is actually in scope // check whether any value tester is actually in scope
TRACE("str", tout << "checking scope of previous value testers" << std::endl;); TRACE("str", tout << "checking scope of previous value testers" << std::endl;);
bool map_effectively_empty = true; 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 // there's *something* in the map, but check its scope
svector<std::pair<int, expr*> > entries = fvar_valueTester_map[freeVar][len]; svector<std::pair<int, expr*> > entries = fvar_valueTester_map[freeVar][len];
for (svector<std::pair<int,expr*> >::iterator it = entries.begin(); it != entries.end(); ++it) { for (svector<std::pair<int,expr*> >::iterator it = entries.begin(); it != entries.end(); ++it) {
@ -9721,8 +9721,8 @@ namespace smt {
int dist = opt_LCMUnrollStep; int dist = opt_LCMUnrollStep;
expr_ref_vector litems(mgr); expr_ref_vector litems(mgr);
expr_ref moreAst(mk_string("more"), mgr); expr_ref moreAst(mk_string("more"), mgr);
for (std::set<expr*>::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { for (expr * e : unrolls) {
expr_ref item(ctx.mk_eq_atom(var, *itor), mgr); expr_ref item(ctx.mk_eq_atom(var, e), mgr);
TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;);
litems.push_back(item); litems.push_back(item);
} }
@ -9731,10 +9731,8 @@ namespace smt {
ptr_vector<expr> outOfScopeTesters; ptr_vector<expr> outOfScopeTesters;
for (ptr_vector<expr>::iterator it = unroll_tries_map[var][unrolls].begin(); for (expr * tester : unroll_tries_map[var][unrolls]) {
it != unroll_tries_map[var][unrolls].end(); ++it) { bool inScope = internal_unrollTest_vars.contains(tester);
expr * tester = *it;
bool inScope = (internal_unrollTest_vars.find(tester) != internal_unrollTest_vars.end());
TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr)
<< (inScope ? " in scope" : " out of scope") << (inScope ? " in scope" : " out of scope")
<< std::endl;); << std::endl;);
@ -9743,12 +9741,10 @@ namespace smt {
} }
} }
for (ptr_vector<expr>::iterator it = outOfScopeTesters.begin(); for (expr* e : outOfScopeTesters) {
it != outOfScopeTesters.end(); ++it) { unroll_tries_map[var][unrolls].erase(e);
unroll_tries_map[var][unrolls].erase(*it);
} }
if (unroll_tries_map[var][unrolls].size() == 0) { if (unroll_tries_map[var][unrolls].size() == 0) {
unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var()); unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var());
} }
@ -10265,9 +10261,8 @@ namespace smt {
// assume empty and find a counterexample // assume empty and find a counterexample
map_effectively_empty = true; map_effectively_empty = true;
ptr_vector<expr> indicator_set = fvar_lenTester_map[freeVar]; ptr_vector<expr> indicator_set = fvar_lenTester_map[freeVar];
for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { for (expr * indicator : indicator_set) {
expr * indicator = *it; if (internal_variable_set.contains(indicator)) {
if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m)
<< " in fvar_lenTester_map[freeVar]" << std::endl;); << " in fvar_lenTester_map[freeVar]" << std::endl;);
map_effectively_empty = false; map_effectively_empty = false;
@ -10437,14 +10432,14 @@ namespace smt {
void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) { void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
context & ctx = get_context(); context & ctx = get_context();
std::set<expr*> eqcRepSet; obj_hashtable<expr> eqcRepSet;
std::set<expr*> leafVarSet; obj_hashtable<expr> leafVarSet;
std::map<int, std::set<expr*> > aloneVars; std::map<int, obj_hashtable<expr> > aloneVars;
for (std::map<expr*, int>::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { for (auto const& kv : freeVar_map) {
expr * freeVar = fvIt->first; expr * freeVar = kv.first;
// skip all regular expression vars // skip all regular expression vars
if (regex_variable_set.find(freeVar) != regex_variable_set.end()) { if (regex_variable_set.contains(freeVar)) {
continue; continue;
} }
@ -10454,10 +10449,10 @@ namespace smt {
get_var_in_eqc(freeVar, eqVarSet); get_var_in_eqc(freeVar, eqVarSet);
bool duplicated = false; bool duplicated = false;
expr * dupVar = nullptr; expr * dupVar = nullptr;
for (std::set<expr*>::iterator itorEqv = eqVarSet.begin(); itorEqv != eqVarSet.end(); itorEqv++) { for (expr* eq : eqVarSet) {
if (eqcRepSet.find(*itorEqv) != eqcRepSet.end()) { if (eqcRepSet.contains(eq)) {
duplicated = true; duplicated = true;
dupVar = *itorEqv; dupVar = eq;
break; break;
} }
} }
@ -10470,13 +10465,9 @@ namespace smt {
} }
} }
for (std::set<expr*>::iterator fvIt = eqcRepSet.begin(); fvIt != eqcRepSet.end(); fvIt++) { for (expr * freeVar : eqcRepSet) {
bool standAlone = true;
expr * freeVar = *fvIt;
// has length constraint initially // has length constraint initially
if (input_var_in_len.find(freeVar) != input_var_in_len.end()) { bool standAlone = !input_var_in_len.contains(freeVar);
standAlone = false;
}
// iterate parents // iterate parents
if (standAlone) { if (standAlone) {
// I hope this works! // I hope this works!
@ -10507,25 +10498,19 @@ namespace smt {
} }
} }
for(std::set<expr*>::iterator itor1 = leafVarSet.begin(); for (expr* lv : leafVarSet) {
itor1 != leafVarSet.end(); ++itor1) { expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, "");
expr * toAssert = gen_len_val_options_for_free_var(*itor1, nullptr, "");
// gen_len_val_options_for_free_var() can legally return NULL, // gen_len_val_options_for_free_var() can legally return NULL,
// as methods that it calls may assert their own axioms instead. // as methods that it calls may assert their own axioms instead.
if (toAssert != nullptr) { if (toAssert) assert_axiom(toAssert);
assert_axiom(toAssert);
}
} }
for (std::map<int, std::set<expr*> >::iterator mItor = aloneVars.begin(); for (auto const& kv : aloneVars) {
mItor != aloneVars.end(); ++mItor) { for (expr* av : kv.second) {
std::set<expr*>::iterator itor2 = mItor->second.begin(); expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, "");
for(; itor2 != mItor->second.end(); ++itor2) {
expr * toAssert = gen_len_val_options_for_free_var(*itor2, nullptr, "");
// same deal with returning a NULL axiom here // same deal with returning a NULL axiom here
if(toAssert != nullptr) { if (toAssert) assert_axiom(toAssert);
assert_axiom(toAssert);
}
} }
} }
} }

3
src/smt/theory_str.h
View file

@ -295,7 +295,8 @@ protected:
obj_hashtable<expr> input_var_in_len; obj_hashtable<expr> input_var_in_len;
obj_map<expr, unsigned int> fvar_len_count_map; obj_map<expr, unsigned int> fvar_len_count_map;
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map; // std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_map; obj_map<expr, expr*> lenTester_fvar_map;
// TBD: need to replace by obj_map for determinism // TBD: need to replace by obj_map for determinism

17
src/util/hashtable.h
View file

@ -600,9 +600,8 @@ public:
core_hashtable& operator|=(core_hashtable const& other) { core_hashtable& operator|=(core_hashtable const& other) {
if (this == &other) return *this; if (this == &other) return *this;
iterator i = other.begin(), e = other.end(); for (const data& d : other) {
for (; i != e; ++i) { insert(d);
insert(*i);
} }
return *this; return *this;
} }
@ -610,10 +609,9 @@ public:
core_hashtable& operator&=(core_hashtable const& other) { core_hashtable& operator&=(core_hashtable const& other) {
if (this == &other) return *this; if (this == &other) return *this;
core_hashtable copy(*this); core_hashtable copy(*this);
iterator i = copy.begin(), e = copy.end(); for (const data& d : copy) {
for (; i != e; ++i) { if (!other.contains(d)) {
if (!other.contains(*i)) { remove(d);
remove(*i);
} }
} }
return *this; return *this;
@ -622,9 +620,8 @@ public:
core_hashtable& operator=(core_hashtable const& other) { core_hashtable& operator=(core_hashtable const& other) {
if (this == &other) return *this; if (this == &other) return *this;
reset(); reset();
iterator i = other.begin(), e = other.end(); for (const data& d : e) {
for (; i != e; ++i) { insert(d);
insert(*i);
} }
return *this; return *this;
} }

3
src/util/obj_hashtable.h
View file

@ -174,6 +174,9 @@ public:
value & find(key * k) { value & find(key * k) {
obj_map_entry * e = find_core(k); obj_map_entry * e = find_core(k);
if (!e) {
e = insert_if_not_there2(k, value());
}
SASSERT(e); SASSERT(e);
return e->get_data().m_value; return e->get_data().m_value;
} }