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

use mk_int_var to make xor terms

Browse source
This commit is contained in:
Murphy Berzish 2016-09-14 19:01:14 -04:00
parent d334403720
commit 15055c8041
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -32,7 +32,7 @@ theory_str::theory_str(ast_manager & m):
/* Options */
opt_AggressiveLengthTesting(false),
opt_AggressiveValueTesting(false),
opt_AggressiveUnrollTesting(false),
opt_AggressiveUnrollTesting(true),
opt_EagerStringConstantLengthAssertions(true),
opt_VerifyFinalCheckProgress(true),
opt_LCMUnrollStep(2),
@ -453,6 +453,7 @@ void theory_str::track_variable_scope(expr * var) {
}
app * theory_str::mk_internal_xor_var() {
/*
ast_manager & m = get_manager();
std::stringstream ss;
ss << tmpXorVarCount;
@ -460,6 +461,7 @@ app * theory_str::mk_internal_xor_var() {
std::string name = "$$_xor_" + ss.str();
// Z3_sort r = of_sort(mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), INT_SORT));
sort * int_sort = m.mk_sort(m_autil.get_family_id(), INT_SORT);
char * new_buffer = alloc_svect(char, name.length() + 1);
strcpy(new_buffer, name.c_str());
symbol sym(new_buffer);
@ -467,6 +469,8 @@ app * theory_str::mk_internal_xor_var() {
app * a = m.mk_const(m.mk_const_decl(sym, int_sort));
m_trail.push_back(a);
return a;
*/
return mk_int_var("$$_xor");
}
app * theory_str::mk_int_var(std::string name) {