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

experimental non-reuse of XOR vars in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-11-30 15:52:58 -05:00
parent 599cc1e75d
commit fd1bf65b64
1 changed files with 10 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_str.cpp
View file

@ -2815,13 +2815,12 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
if (entry1InScope) {
t1 = varForBreakConcat[key1][0];
t2 = varForBreakConcat[key1][1];
xorFlag = varForBreakConcat[key1][2];
xorFlag = mk_internal_xor_var();
} else {
t1 = varForBreakConcat[key2][0];
t2 = varForBreakConcat[key2][1];
xorFlag = varForBreakConcat[key2][2];
xorFlag = mk_internal_xor_var();
}
// TODO do I need to refresh the xorFlag, which is an integer var, and if so, how?
refresh_theory_var(t1);
refresh_theory_var(t2);
}
@ -3141,12 +3140,11 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
} else {
if (entry1InScope) {
temp1 = varForBreakConcat[key1][0];
xorFlag = varForBreakConcat[key1][1];
xorFlag = mk_internal_xor_var();
} else if (entry2InScope) {
temp1 = varForBreakConcat[key2][0];
xorFlag = varForBreakConcat[key2][1];
xorFlag = mk_internal_xor_var();
}
// TODO refresh xorFlag?
refresh_theory_var(temp1);
}
@ -3451,10 +3449,10 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
} else {
if (entry1InScope) {
temp1 = varForBreakConcat[key1][0];
xorFlag = varForBreakConcat[key1][1];
xorFlag = mk_internal_xor_var();
} else if (varForBreakConcat.find(key2) != varForBreakConcat.end()) {
temp1 = varForBreakConcat[key2][0];
xorFlag = varForBreakConcat[key2][1];
xorFlag = mk_internal_xor_var();
}
refresh_theory_var(temp1);
}
@ -3948,10 +3946,10 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
} else {
if (entry1InScope) {
commonVar = (entry1->second)[0];
xorFlag = (entry1->second)[1];
xorFlag = mk_internal_xor_var();
} else {
commonVar = (entry2->second)[0];
xorFlag = (entry2->second)[1];
xorFlag = mk_internal_xor_var();
}
refresh_theory_var(commonVar);
}
@ -6113,9 +6111,9 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
xorFlag = mk_internal_xor_var();
varForBreakConcat[key1][0] = xorFlag;
} else if (entry1InScope) {
xorFlag = varForBreakConcat[key1][0];
xorFlag = mk_internal_xor_var();
} else { // entry2InScope
xorFlag = varForBreakConcat[key2][0];
xorFlag = mk_internal_xor_var();
}
int concatStrLen = const_str.length();