mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

keep track of search level ourselves

Browse source
This commit is contained in:
Murphy Berzish 2015-12-01 14:41:11 -05:00
parent dd0bc13be7
commit c44d49b625
2 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_str.cpp
View file

@ -29,6 +29,7 @@ theory_str::theory_str(ast_manager & m):
search_started(false),
m_autil(m),
m_strutil(m),
sLevel(0),
tmpStringVarCount(0),
tmpXorVarCount(0),
avoidLoopCut(true),
@ -331,7 +332,6 @@ expr * theory_str::mk_internal_valTest_var(expr * node, int len, int vTries) {
void theory_str::track_variable_scope(expr * var) {
context & ctx = get_context();
int sLevel = ctx.get_scope_level();
if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) {
internal_variable_scope_levels[sLevel] = std::set<expr*>();
}
@ -361,7 +361,6 @@ app * theory_str::mk_str_var(std::string name) {
context & ctx = get_context();
ast_manager & m = get_manager();
int sLevel = ctx.get_scope_level();
TRACE("t_str_detail", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = m.mk_sort(m_strutil.get_family_id(), STRING_SORT);
@ -393,8 +392,6 @@ app * theory_str::mk_nonempty_str_var() {
tmpStringVarCount++;
std::string name = "$$_str" + ss.str();
int sLevel = ctx.get_scope_level();
TRACE("t_str_detail", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = m.mk_sort(m_strutil.get_family_id(), STRING_SORT);
@ -2637,13 +2634,13 @@ void theory_str::assign_eh(bool_var v, bool is_true) {
void theory_str::push_scope_eh() {
context & ctx = get_context();
int sLevel = ctx.get_scope_level();
sLevel += 1;
TRACE("t_str", tout << "push to " << sLevel << std::endl;);
}
void theory_str::pop_scope_eh(unsigned num_scopes) {
context & ctx = get_context();
int sLevel = ctx.get_scope_level();
sLevel -= num_scopes;
TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
@ -3777,8 +3774,6 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator,
context & ctx = get_context();
ast_manager & m = get_manager();
int sLevel = ctx.get_scope_level();
int len = atoi(len_valueStr.c_str());
if (fvar_valueTester_map[freeVar].find(len) == fvar_valueTester_map[freeVar].end()) {

1
src/smt/theory_str.h
View file

@ -63,6 +63,7 @@ namespace smt {
};
protected:
bool search_started;
int sLevel;
arith_util m_autil;
str_util m_strutil;