mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Merge pull request #4320 from mtrberzi/mc-rational

Browse source 
z3str3: use rational in place of unsigned during model construction
This commit is contained in:
Murphy Berzish 2020-05-15 20:42:19 -05:00 • committed by GitHub
commit fcbcad6c10
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 36 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/smt/theory_str.cpp
View file

@ -8961,7 +8961,7 @@ namespace smt {
out << "TODO: theory_str display" << std::endl;
}
unsigned theory_str::get_refine_length(expr* ex, expr_ref_vector& extra_deps){
rational theory_str::get_refine_length(expr* ex, expr_ref_vector& extra_deps){
ast_manager & m = get_manager();
TRACE("str_fl", tout << "finding length for " << mk_ismt2_pp(ex, m) << std::endl;);
@ -8971,7 +8971,7 @@ namespace smt {
SASSERT(str_exists);
zstring str_const;
u.str.is_string(str, str_const);
return str_const.length();
return rational(str_const.length());
} else if (u.str.is_itos(ex)) {
expr* fromInt = nullptr;
u.str.is_itos(ex, fromInt);
@ -8983,7 +8983,7 @@ namespace smt {
std::string s = std::to_string(val.get_int32());
extra_deps.push_back(ctx.mk_eq_atom(fromInt, mk_int(val)));
return static_cast<unsigned>(s.length());
return rational((unsigned)s.length());
} else if (u.str.is_at(ex)) {
expr* substrBase = nullptr;
@ -8995,7 +8995,7 @@ namespace smt {
VERIFY(v.get_value(substrPos, pos));
extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(pos)));
return 1;
return rational::one();
} else if (u.str.is_extract(ex)) {
expr* substrBase = nullptr;
@ -9009,7 +9009,7 @@ namespace smt {
VERIFY(v.get_value(substrPos, pos));
extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(pos)));
return len.get_unsigned();
return len;
} else if (u.str.is_replace(ex)) {
TRACE("str_fl", tout << "replace is like contains---not in conjunctive fragment!" << std::endl;);
@ -9045,8 +9045,8 @@ namespace smt {
return nullptr;
}
expr* theory_str::refine_eq(expr* lhs, expr* rhs, unsigned offset) {
TRACE("str_fl", tout << "refine eq " << offset << std::endl;);
expr* theory_str::refine_eq(expr* lhs, expr* rhs, unsigned _offset) {
TRACE("str_fl", tout << "refine eq " << _offset << std::endl;);
ast_manager & m = get_manager();
expr_ref_vector Gamma(m);
@ -9057,9 +9057,11 @@ namespace smt {
}
expr_ref_vector extra_deps(m);
rational offset(_offset);
// find len(Gamma[:i])
unsigned left_count = 0, left_length = 0, last_length = 0;
unsigned left_count = 0;
rational left_length(0), last_length(0);
while(left_count < Gamma.size() && left_length <= offset) {
last_length = get_refine_length(Gamma.get(left_count), extra_deps);
left_length += last_length;
@ -9075,7 +9077,8 @@ namespace smt {
if (!u.str.is_string(to_app(Gamma.get(i)))) {
len = u.str.mk_length(Gamma.get(i));
} else {
len = mk_int(offset - left_length);
rational lenDiff = offset - left_length;
len = mk_int(lenDiff);
}
if (left_sublen == nullptr) {
left_sublen = len;
@ -9084,19 +9087,22 @@ namespace smt {
}
}
if (offset - left_length != 0) {
rational lenDiff = offset - left_length;
if (left_sublen == nullptr) {
left_sublen = mk_int(offset - left_length);
left_sublen = mk_int(lenDiff);
} else {
left_sublen = m_autil.mk_add(left_sublen, mk_int(offset - left_length));
left_sublen = m_autil.mk_add(left_sublen, mk_int(lenDiff));
}
}
expr* extra_left_cond = nullptr;
if (!u.str.is_string(to_app(Gamma.get(left_count)))) {
extra_left_cond = m_autil.mk_ge(u.str.mk_length(Gamma.get(left_count)), mk_int(offset - left_length + 1));
rational offsetLen = offset - left_length + 1;
extra_left_cond = m_autil.mk_ge(u.str.mk_length(Gamma.get(left_count)), mk_int(offsetLen));
}
// find len(Delta[:j])
unsigned right_count = 0, right_length = 0;
unsigned right_count = 0;
rational right_length(0);
last_length = 0;
while(right_count < Delta.size() && right_length <= offset) {
last_length = get_refine_length(Delta.get(right_count), extra_deps);
@ -9113,7 +9119,8 @@ namespace smt {
if (!u.str.is_string(to_app(Delta.get(i)))) {
len = u.str.mk_length(Delta.get(i));
} else {
len = mk_int(offset - right_length);
rational offsetLen = offset - right_length;
len = mk_int(offsetLen);
}
if (right_sublen == nullptr) {
right_sublen = len;
@ -9122,15 +9129,17 @@ namespace smt {
}
}
if (offset - right_length != 0) {
rational offsetLen = offset - right_length;
if (right_sublen == nullptr) {
right_sublen = mk_int(offset - right_length);
right_sublen = mk_int(offsetLen);
} else {
right_sublen = m_autil.mk_add(right_sublen, mk_int(offset - right_length));
right_sublen = m_autil.mk_add(right_sublen, mk_int(offsetLen));
}
}
expr* extra_right_cond = nullptr;
if (!u.str.is_string(to_app(Delta.get(right_count)))) {
extra_right_cond = m_autil.mk_ge(u.str.mk_length(Delta.get(right_count)), mk_int(offset - right_length + 1));
rational offsetLen = offset - right_length + 1;
extra_right_cond = m_autil.mk_ge(u.str.mk_length(Delta.get(right_count)), mk_int(offsetLen));
}
// Offset tells us that Gamma[i+1:]) != Delta[j+1:]

4
src/smt/theory_str.h
View file

@ -543,7 +543,7 @@ protected:
// fixed length model construction
expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver*
expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these
obj_map<expr, unsigned> fixed_length_used_len_terms; // constraints used in generating fixed length model
obj_map<expr, rational> fixed_length_used_len_terms; // constraints used in generating fixed length model
obj_map<expr, ptr_vector<expr> > var_to_char_subterm_map; // maps a var to a list of character terms *in the subsolver*
obj_map<expr, ptr_vector<expr> > uninterpreted_to_char_subterm_map; // maps an "uninterpreted" string term to a list of character terms *in the subsolver*
obj_map<expr, std::tuple<rational, expr*, expr*>> fixed_length_lesson; //keep track of information for the lesson
@ -603,7 +603,7 @@ protected:
expr* refine_dis(expr* lhs, expr* rhs);
expr* refine_function(expr* f);
bool flatten(expr* ex, expr_ref_vector & flat);
unsigned get_refine_length(expr* ex, expr_ref_vector& extra_deps);
rational get_refine_length(expr* ex, expr_ref_vector& extra_deps);
void instantiate_axiom_CharAt(enode * e);
void instantiate_axiom_prefixof(enode * e);

16
src/smt/theory_str_mc.cpp
View file

@ -624,17 +624,16 @@ namespace smt {
cex = expr_ref(m_autil.mk_ge(mk_strlen(term), mk_int(0)), m);
return false;
}
SASSERT(varLen_value.is_unsigned() && "actually arithmetic solver can assign it a very large number");
TRACE("str_fl", tout << "creating character terms for variable " << mk_pp(term, m) << ", length = " << varLen_value << std::endl;);
ptr_vector<expr> new_chars;
for (unsigned i = 0; i < varLen_value.get_unsigned(); ++i) {
for (rational i = rational::zero(); i < varLen_value; ++i) {
// TODO we can probably name these better for the sake of debugging
expr_ref ch(mk_fresh_const("char", bv8_sort), m);
new_chars.push_back(ch);
fixed_length_subterm_trail.push_back(ch);
}
var_to_char_subterm_map.insert(term, new_chars);
fixed_length_used_len_terms.insert(term, varLen_value.get_unsigned());
fixed_length_used_len_terms.insert(term, varLen_value);
}
var_to_char_subterm_map.find(term, eqc_chars);
} else if (u.str.is_concat(term, arg0, arg1)) {
@ -754,13 +753,13 @@ namespace smt {
}
TRACE("str_fl", tout << "creating character terms for uninterpreted function " << mk_pp(term, m) << ", length = " << ufLen_value << std::endl;);
ptr_vector<expr> new_chars;
for (unsigned i = 0; i < ufLen_value.get_unsigned(); ++i) {
for (rational i = rational::zero(); i < ufLen_value; ++i) {
expr_ref ch(mk_fresh_const("char", bv8_sort), m);
new_chars.push_back(ch);
fixed_length_subterm_trail.push_back(ch);
}
uninterpreted_to_char_subterm_map.insert(term, new_chars);
fixed_length_used_len_terms.insert(term, ufLen_value.get_unsigned());
fixed_length_used_len_terms.insert(term, ufLen_value);
}
uninterpreted_to_char_subterm_map.find(term, eqc_chars);
}
@ -794,7 +793,6 @@ namespace smt {
fixed_length_assumptions.push_back(_e);
fixed_length_lesson.insert(_e, std::make_tuple(rational(i), lhs, rhs));
}
// fixed_length_used_len_terms.push_back(get_context().mk_eq_atom(lhs, rhs));
return true;
}
@ -1056,7 +1054,8 @@ namespace smt {
for (auto e : fixed_length_used_len_terms) {
expr * var = &e.get_key();
precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value())));
rational val = e.get_value();
precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(val)));
}
TRACE("str_fl",
@ -1172,7 +1171,8 @@ namespace smt {
TRACE("str_fl", tout << "subsolver found UNSAT; constructing length counterexample" << std::endl;);
for (auto e : fixed_length_used_len_terms) {
expr * var = &e.get_key();
cex.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value())));
rational val = e.get_value();
cex.push_back(m.mk_eq(u.str.mk_length(var), mk_int(val)));
}
return l_false;
} else {