mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

z3str3: ensure top-level free variables always participate in model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-01-22 15:13:56 -05:00 • committed by Nikolaj Bjorner
parent 812049ca4a
commit 237adbf40c
3 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -9175,7 +9175,7 @@ namespace smt {
} // RegexAutomata } // RegexAutomata
bool needToAssignFreeVars = false; bool needToAssignFreeVars = false;
std::set<expr*> free_variables; expr_ref_vector free_variables(m);
std::set<expr*> unused_internal_variables; std::set<expr*> unused_internal_variables;
{ // Z3str2 free variables check { // Z3str2 free variables check
std::map<expr*, int>::iterator itor = varAppearInAssign.begin(); std::map<expr*, int>::iterator itor = varAppearInAssign.begin();
@ -9196,7 +9196,7 @@ namespace smt {
if (!hasEqcValue) { if (!hasEqcValue) {
TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;); TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;);
needToAssignFreeVars = true; needToAssignFreeVars = true;
free_variables.insert(itor->first); free_variables.push_back(itor->first);
// break; // break;
} else { } else {
// debug // debug
@ -9413,7 +9413,7 @@ namespace smt {
expr_ref_vector precondition(m); expr_ref_vector precondition(m);
expr_ref_vector cex(m); expr_ref_vector cex(m);
lbool model_status = fixed_length_model_construction(assignments, precondition, candidate_model, cex); lbool model_status = fixed_length_model_construction(assignments, precondition, free_variables, candidate_model, cex);
if (model_status == l_true) { if (model_status == l_true) {
m_stats.m_solved_by = 2; m_stats.m_solved_by = 2;

1
src/smt/theory_str.h
View file

@ -842,6 +842,7 @@ protected:
bool finalcheck_int2str(app * a); bool finalcheck_int2str(app * a);
lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition, lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
expr_ref_vector& free_variables,
obj_map<expr, zstring> &model, expr_ref_vector &cex); obj_map<expr, zstring> &model, expr_ref_vector &cex);
ptr_vector<expr> fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term); ptr_vector<expr> fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term);
bool fixed_length_get_len_value(expr * e, rational & val); bool fixed_length_get_len_value(expr * e, rational & val);

10
src/smt/theory_str_mc.cpp
View file

@ -614,6 +614,7 @@ namespace smt {
} }
lbool theory_str::fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition, lbool theory_str::fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
expr_ref_vector& free_variables,
obj_map<expr, zstring> &model, expr_ref_vector &cex) { obj_map<expr, zstring> &model, expr_ref_vector &cex) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -658,6 +659,15 @@ namespace smt {
sort * str_sort = u.str.mk_string_sort(); sort * str_sort = u.str.mk_string_sort();
sort * bool_sort = m.mk_bool_sort(); sort * bool_sort = m.mk_bool_sort();
for (expr * var : free_variables) {
TRACE("str_fl", tout << "initialize free variable " << mk_pp(var, m) << std::endl;);
rational var_lenVal;
if (!fixed_length_get_len_value(var, var_lenVal)) {
NOT_IMPLEMENTED_YET();
}
fixed_length_reduce_string_term(subsolver, var);
}
for (expr * f : formulas) { for (expr * f : formulas) {
if (!get_context().is_relevant(f)) { if (!get_context().is_relevant(f)) {
TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;); TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;);