mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

z3str3: use rational in place of unsigned during model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-05-13 14:32:44 -04:00
parent 127ef59ce4
commit 5e7806c4a4
3 changed files with 36 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/smt/theory_str.cpp
View file

@ -8833,7 +8833,7 @@ namespace smt {
out << "TODO: theory_str display" << std::endl; 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(); ast_manager & m = get_manager();
TRACE("str_fl", tout << "finding length for " << mk_ismt2_pp(ex, m) << std::endl;); TRACE("str_fl", tout << "finding length for " << mk_ismt2_pp(ex, m) << std::endl;);
@ -8843,7 +8843,7 @@ namespace smt {
SASSERT(str_exists); SASSERT(str_exists);
zstring str_const; zstring str_const;
u.str.is_string(str, 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)) { } else if (u.str.is_itos(ex)) {
expr* fromInt = nullptr; expr* fromInt = nullptr;
u.str.is_itos(ex, fromInt); u.str.is_itos(ex, fromInt);
@ -8855,7 +8855,7 @@ namespace smt {
std::string s = std::to_string(val.get_int32()); std::string s = std::to_string(val.get_int32());
extra_deps.push_back(ctx.mk_eq_atom(fromInt, mk_int(val))); 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)) { } else if (u.str.is_at(ex)) {
expr* substrBase = nullptr; expr* substrBase = nullptr;
@ -8867,7 +8867,7 @@ namespace smt {
VERIFY(v.get_value(substrPos, pos)); VERIFY(v.get_value(substrPos, pos));
extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(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)) { } else if (u.str.is_extract(ex)) {
expr* substrBase = nullptr; expr* substrBase = nullptr;
@ -8881,7 +8881,7 @@ namespace smt {
VERIFY(v.get_value(substrPos, pos)); VERIFY(v.get_value(substrPos, pos));
extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(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)) { } else if (u.str.is_replace(ex)) {
TRACE("str_fl", tout << "replace is like contains---not in conjunctive fragment!" << std::endl;); TRACE("str_fl", tout << "replace is like contains---not in conjunctive fragment!" << std::endl;);
@ -8917,8 +8917,8 @@ namespace smt {
return nullptr; return nullptr;
} }
expr* theory_str::refine_eq(expr* lhs, expr* rhs, unsigned offset) { expr* theory_str::refine_eq(expr* lhs, expr* rhs, unsigned _offset) {
TRACE("str_fl", tout << "refine eq " << offset << std::endl;); TRACE("str_fl", tout << "refine eq " << _offset << std::endl;);
ast_manager & m = get_manager(); ast_manager & m = get_manager();
expr_ref_vector Gamma(m); expr_ref_vector Gamma(m);
@ -8929,9 +8929,11 @@ namespace smt {
} }
expr_ref_vector extra_deps(m); expr_ref_vector extra_deps(m);
rational offset(_offset);
// find len(Gamma[:i]) // 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) { while(left_count < Gamma.size() && left_length <= offset) {
last_length = get_refine_length(Gamma.get(left_count), extra_deps); last_length = get_refine_length(Gamma.get(left_count), extra_deps);
left_length += last_length; left_length += last_length;
@ -8947,7 +8949,8 @@ namespace smt {
if (!u.str.is_string(to_app(Gamma.get(i)))) { if (!u.str.is_string(to_app(Gamma.get(i)))) {
len = u.str.mk_length(Gamma.get(i)); len = u.str.mk_length(Gamma.get(i));
} else { } else {
len = mk_int(offset - left_length); rational lenDiff = offset - left_length;
len = mk_int(lenDiff);
} }
if (left_sublen == nullptr) { if (left_sublen == nullptr) {
left_sublen = len; left_sublen = len;
@ -8956,19 +8959,22 @@ namespace smt {
} }
} }
if (offset - left_length != 0) { if (offset - left_length != 0) {
rational lenDiff = offset - left_length;
if (left_sublen == nullptr) { if (left_sublen == nullptr) {
left_sublen = mk_int(offset - left_length); left_sublen = mk_int(lenDiff);
} else { } 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; expr* extra_left_cond = nullptr;
if (!u.str.is_string(to_app(Gamma.get(left_count)))) { 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]) // find len(Delta[:j])
unsigned right_count = 0, right_length = 0; unsigned right_count = 0;
rational right_length(0);
last_length = 0; last_length = 0;
while(right_count < Delta.size() && right_length <= offset) { while(right_count < Delta.size() && right_length <= offset) {
last_length = get_refine_length(Delta.get(right_count), extra_deps); last_length = get_refine_length(Delta.get(right_count), extra_deps);
@ -8985,7 +8991,8 @@ namespace smt {
if (!u.str.is_string(to_app(Delta.get(i)))) { if (!u.str.is_string(to_app(Delta.get(i)))) {
len = u.str.mk_length(Delta.get(i)); len = u.str.mk_length(Delta.get(i));
} else { } else {
len = mk_int(offset - right_length); rational offsetLen = offset - right_length;
len = mk_int(offsetLen);
} }
if (right_sublen == nullptr) { if (right_sublen == nullptr) {
right_sublen = len; right_sublen = len;
@ -8994,15 +9001,17 @@ namespace smt {
} }
} }
if (offset - right_length != 0) { if (offset - right_length != 0) {
rational offsetLen = offset - right_length;
if (right_sublen == nullptr) { if (right_sublen == nullptr) {
right_sublen = mk_int(offset - right_length); right_sublen = mk_int(offsetLen);
} else { } 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; expr* extra_right_cond = nullptr;
if (!u.str.is_string(to_app(Delta.get(right_count)))) { 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:] // 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 // fixed length model construction
expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver* 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 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> > 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, 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 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_dis(expr* lhs, expr* rhs);
expr* refine_function(expr* f); expr* refine_function(expr* f);
bool flatten(expr* ex, expr_ref_vector & flat); 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_CharAt(enode * e);
void instantiate_axiom_prefixof(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); cex = expr_ref(m_autil.mk_ge(mk_strlen(term), mk_int(0)), m);
return false; 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;); TRACE("str_fl", tout << "creating character terms for variable " << mk_pp(term, m) << ", length = " << varLen_value << std::endl;);
ptr_vector<expr> new_chars; 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 // TODO we can probably name these better for the sake of debugging
expr_ref ch(mk_fresh_const("char", bv8_sort), m); expr_ref ch(mk_fresh_const("char", bv8_sort), m);
new_chars.push_back(ch); new_chars.push_back(ch);
fixed_length_subterm_trail.push_back(ch); fixed_length_subterm_trail.push_back(ch);
} }
var_to_char_subterm_map.insert(term, new_chars); 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); var_to_char_subterm_map.find(term, eqc_chars);
} else if (u.str.is_concat(term, arg0, arg1)) { } 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;); TRACE("str_fl", tout << "creating character terms for uninterpreted function " << mk_pp(term, m) << ", length = " << ufLen_value << std::endl;);
ptr_vector<expr> new_chars; 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); expr_ref ch(mk_fresh_const("char", bv8_sort), m);
new_chars.push_back(ch); new_chars.push_back(ch);
fixed_length_subterm_trail.push_back(ch); fixed_length_subterm_trail.push_back(ch);
} }
uninterpreted_to_char_subterm_map.insert(term, new_chars); 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); uninterpreted_to_char_subterm_map.find(term, eqc_chars);
} }
@ -794,7 +793,6 @@ namespace smt {
fixed_length_assumptions.push_back(_e); fixed_length_assumptions.push_back(_e);
fixed_length_lesson.insert(_e, std::make_tuple(rational(i), lhs, rhs)); 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; return true;
} }
@ -1056,7 +1054,8 @@ namespace smt {
for (auto e : fixed_length_used_len_terms) { for (auto e : fixed_length_used_len_terms) {
expr * var = &e.get_key(); 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", TRACE("str_fl",
@ -1172,7 +1171,8 @@ namespace smt {
TRACE("str_fl", tout << "subsolver found UNSAT; constructing length counterexample" << std::endl;); TRACE("str_fl", tout << "subsolver found UNSAT; constructing length counterexample" << std::endl;);
for (auto e : fixed_length_used_len_terms) { for (auto e : fixed_length_used_len_terms) {
expr * var = &e.get_key(); 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; return l_false;
} else { } else {