mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

z3str3: refactor app* to app_ref

Browse source
This commit is contained in:
Murphy Berzish 2019-11-22 17:08:58 -05:00 committed by Nikolaj Bjorner
parent b2c3025e21
commit 415260b93d
2 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_str.cpp
View file

@ -604,7 +604,7 @@ namespace smt {
}
}
app * theory_str::mk_nonempty_str_var() {
app_ref theory_str::mk_nonempty_str_var() {
context & ctx = get_context();
ast_manager & m = get_manager();
@ -616,7 +616,7 @@ namespace smt {
TRACE("str", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const(name.c_str(), string_sort);
app_ref a(mk_fresh_const(name.c_str(), string_sort), m);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != nullptr);
@ -3300,8 +3300,7 @@ namespace smt {
<< "split type " << splitType << std::endl;
);
expr * t1 = nullptr;
expr * t2 = nullptr;
expr_ref t1(mgr), t2(mgr);
expr * xorFlag = nullptr;
std::pair<expr*, expr*> key1(concatAst1, concatAst2);
@ -3705,7 +3704,7 @@ namespace smt {
// setup
expr * xorFlag = nullptr;
expr * temp1 = nullptr;
expr_ref temp1(mgr);
std::pair<expr*, expr*> key1(concatAst1, concatAst2);
std::pair<expr*, expr*> key2(concatAst2, concatAst1);
@ -4643,7 +4642,7 @@ namespace smt {
}
//----------------------------------------------------------------
expr * commonVar = nullptr;
expr_ref commonVar(mgr);
expr * xorFlag = nullptr;
std::pair<expr*, expr*> key1(concatAst1, concatAst2);
std::pair<expr*, expr*> key2(concatAst2, concatAst1);

2
src/smt/theory_str.h
View file

@ -515,7 +515,7 @@ protected:
void track_variable_scope(expr * var);
app * mk_str_var(std::string name);
app * mk_int_var(std::string name);
app * mk_nonempty_str_var();
app_ref mk_nonempty_str_var();
app * mk_internal_xor_var();
expr * mk_internal_valTest_var(expr * node, int len, int vTries);
app * mk_regex_rep_var();