mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

successful run of model generation test case, after assigning all internal variables a bogus value if they are unused

Browse source
This commit is contained in:
Murphy Berzish 2015-12-03 20:58:54 -05:00
parent e010e7c0d6
commit cf5eacbf33
1 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/theory_str.cpp
View file

@ -3428,20 +3428,37 @@ final_check_status theory_str::final_check_eh() {
// If not, mark it as free. // If not, mark it as free.
bool needToAssignFreeVars = false; bool needToAssignFreeVars = false;
std::set<expr*> free_variables; std::set<expr*> free_variables;
std::set<expr*> unused_internal_variables;
TRACE("t_str_detail", tout << variable_set.size() << " variables in variable_set" << std::endl;); TRACE("t_str_detail", tout << variable_set.size() << " variables in variable_set" << std::endl;);
for (std::set<expr*>::iterator it = variable_set.begin(); it != variable_set.end(); ++it) { for (std::set<expr*>::iterator it = variable_set.begin(); it != variable_set.end(); ++it) {
TRACE("t_str_detail", tout << "checking eqc of variable " << mk_ismt2_pp(*it, m) << std::endl;); TRACE("t_str_detail", tout << "checking eqc of variable " << mk_ismt2_pp(*it, m) << std::endl;);
bool has_eqc_value = false; bool has_eqc_value = false;
get_eqc_value(*it, has_eqc_value); get_eqc_value(*it, has_eqc_value);
if (!has_eqc_value) { if (!has_eqc_value) {
needToAssignFreeVars = true; // if this is an internal variable, it can be ignored...I think
free_variables.insert(*it); if (internal_variable_set.find(*it) != internal_variable_set.end()) {
TRACE("t_str_detail", tout << "WARNING: free internal variable " << mk_ismt2_pp(*it, m) << std::endl;);
unused_internal_variables.insert(*it);
} else {
needToAssignFreeVars = true;
free_variables.insert(*it);
}
} }
} }
if (!needToAssignFreeVars) { if (!needToAssignFreeVars) {
TRACE("t_str", tout << "All variables are assigned. Done!" << std::endl;); if (unused_internal_variables.empty()) {
return FC_DONE; TRACE("t_str", tout << "All variables are assigned. Done!" << std::endl;);
return FC_DONE;
} else {
TRACE("t_str", tout << "Assigning decoy values to free internal variables." << std::endl;);
for (std::set<expr*>::iterator it = unused_internal_variables.begin(); it != unused_internal_variables.end(); ++it) {
expr * var = *it;
expr_ref assignment(m.mk_eq(var, m_strutil.mk_string("**unused**")), m);
assert_axiom(assignment);
}
return FC_CONTINUE;
}
} }
CTRACE("t_str", needToAssignFreeVars, CTRACE("t_str", needToAssignFreeVars,
@ -4218,7 +4235,7 @@ void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> &
} }
void theory_str::init_model(model_generator & mg) { void theory_str::init_model(model_generator & mg) {
TRACE("t_str", tout << "initializing model" << std::endl; display(tout);); //TRACE("t_str", tout << "initializing model" << std::endl; display(tout););
m_factory = alloc(str_value_factory, get_manager(), get_family_id()); m_factory = alloc(str_value_factory, get_manager(), get_family_id());
mg.register_factory(m_factory); mg.register_factory(m_factory);
} }
@ -4287,7 +4304,7 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
TRACE("t_str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;); TRACE("t_str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
// TODO make absolutely sure the reason we can't find a concrete value is because of an unassigned temporary // TODO make absolutely sure the reason we can't find a concrete value is because of an unassigned temporary
// e.g. for an expression like (Concat X $$_str0) // e.g. for an expression like (Concat X $$_str0)
//return alloc(expr_wrapper_proc, m_strutil.mk_string("")); //return alloc(expr_wrapper_proc, m_strutil.mk_string("**UNUSED**"));
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
} }