mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixed vc++ compaibility issues

Browse source
This commit is contained in:
Ken McMillan 2013-11-05 14:45:44 -08:00
parent f83bca11a0
commit fa05116e66
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/interp/iz3mgr.cpp
View file

@ -708,7 +708,7 @@ iz3mgr::ast iz3mgr::mk_idiv(const ast& t, const ast &d){
// does variable occur in expression? // does variable occur in expression?
int iz3mgr::occurs_in1(hash_map<ast,bool> &occurs_in_memo,ast var, ast e){ int iz3mgr::occurs_in1(stl_ext::hash_map<ast,bool> &occurs_in_memo,ast var, ast e){
std::pair<ast,bool> foo(e,false); std::pair<ast,bool> foo(e,false);
std::pair<hash_map<ast,bool>::iterator,bool> bar = occurs_in_memo.insert(foo); std::pair<hash_map<ast,bool>::iterator,bool> bar = occurs_in_memo.insert(foo);
bool &res = bar.first->second; bool &res = bar.first->second;
@ -732,7 +732,7 @@ int iz3mgr::occurs_in(ast var, ast e){
// false would force the formula to have the specifid truth value // false would force the formula to have the specifid truth value
// returns t, or null if no such // returns t, or null if no such
iz3mgr::ast iz3mgr::cont_eq(hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e){ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e){
if(is_not(e)) return cont_eq(cont_eq_memo, !truth,v,arg(e,0)); if(is_not(e)) return cont_eq(cont_eq_memo, !truth,v,arg(e,0));
if(cont_eq_memo.find(e) != cont_eq_memo.end()) if(cont_eq_memo.find(e) != cont_eq_memo.end())
return ast(); return ast();
@ -759,7 +759,7 @@ iz3mgr::ast iz3mgr::cont_eq(hash_set<ast> &cont_eq_memo, bool truth, ast v, ast
// substitute a term t for unbound occurrences of variable v in e // substitute a term t for unbound occurrences of variable v in e
iz3mgr::ast iz3mgr::subst(hash_map<ast,ast> &subst_memo, ast var, ast t, ast e){ iz3mgr::ast iz3mgr::subst(stl_ext::hash_map<ast,ast> &subst_memo, ast var, ast t, ast e){
if(e == var) return t; if(e == var) return t;
std::pair<ast,ast> foo(e,ast()); std::pair<ast,ast> foo(e,ast());
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo); std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);

2
src/interp/iz3proof_itp.cpp
View file

@ -2058,7 +2058,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
bool is_placeholder(const ast &e){ bool is_placeholder(const ast &e){
if(op(e) == Uninterpreted){ if(op(e) == Uninterpreted){
std::string name = string_of_symbol(sym(e)); std::string name = string_of_symbol(sym(e));
if(name.size() > 2 && name[0] == '@' and name[1] == 'p') if(name.size() > 2 && name[0] == '@' && name[1] == 'p')
return true; return true;
} }
return false; return false;