Skip to content

Always pass namespace to from_expr #1051

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 23, 2017
Merged

Always pass namespace to from_expr #1051

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 31 additions & 30 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ void string_refinementt::display_index_set()
for(const auto &i : index_set)
{
const exprt &s=i.first;
debug() << "IS(" << from_expr(s) << ")=={" << eom;
debug() << "IS(" << from_expr(ns, "", s) << ")=={" << eom;

for(auto j : i.second)
{
Expand All @@ -81,7 +81,7 @@ void string_refinementt::display_index_set()
count_current++;
debug() << "**";
}
debug() << " " << from_expr(j) << ";" << eom;
debug() << " " << from_expr(ns, "", j) << ";" << eom;
count++;
}
debug() << "}" << eom;
Expand All @@ -99,10 +99,10 @@ void string_refinementt::add_instantiations()
for(const auto &i : current_index_set)
{
const exprt &s=i.first;
debug() << "IS(" << from_expr(s) << ")=={";
debug() << "IS(" << from_expr(ns, "", s) << ")=={";

for(const auto &j : i.second)
debug() << from_expr(j) << "; ";
debug() << from_expr(ns, "", j) << "; ";
debug() << "}" << eom;

for(const auto &j : i.second)
Expand Down Expand Up @@ -227,7 +227,7 @@ bool string_refinementt::add_axioms_for_string_assigns(
else
{
debug() << "string_refinement warning: not handling char_array: "
<< from_expr(rhs) << eom;
<< from_expr(ns, "", rhs) << eom;
return true;
}
}
Expand Down Expand Up @@ -291,7 +291,7 @@ void string_refinementt::concretize_string(const exprt &expr)
mp_index>=concretize_limit)
{
debug() << "concretize_string: ignoring out of bound index: "
<< from_expr(simple_i) << eom;
<< from_expr(ns, "", simple_i) << eom;
}
else
{
Expand All @@ -311,8 +311,8 @@ void string_refinementt::concretize_string(const exprt &expr)

array_exprt arr(to_array_type(content.type()));
arr.operands()=result;
debug() << "Concretized " << from_expr(content_expr)
<< " = " << from_expr(arr) << eom;
debug() << "Concretized " << from_expr(ns, "", content_expr)
<< " = " << from_expr(ns, "", arr) << eom;
found_content[content]=arr;
}
}
Expand Down Expand Up @@ -371,7 +371,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
if(eq_expr.lhs().type()!=eq_expr.rhs().type())
{
debug() << "(sr::set_to) WARNING: ignoring "
<< from_expr(expr) << " [inconsistent types]" << eom;
<< from_expr(ns, "", expr) << " [inconsistent types]" << eom;
debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom;
debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom;
return;
Expand All @@ -393,7 +393,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
if(lhs.id()!=ID_symbol)
{
debug() << "(sr::set_to) WARNING: ignoring "
<< from_expr(expr) << eom;
<< from_expr(ns, "", expr) << eom;
return;
}

Expand All @@ -405,7 +405,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
eq_expr.lhs().type().subtype() != subst_rhs.type().subtype())
{
debug() << "(sr::set_to) WARNING: ignoring "
<< from_expr(expr) << " [inconsistent types after substitution]"
<< from_expr(ns, "", expr) << " [inconsistent types after substitution]"
<< eom;
return;
}
Expand Down Expand Up @@ -602,7 +602,7 @@ void string_refinementt::add_lemma(
return;
}

debug() << "adding lemma " << from_expr(simple_lemma) << eom;
debug() << "adding lemma " << from_expr(ns, "", simple_lemma) << eom;

prop.l_set_to_true(convert(simple_lemma));
}
Expand All @@ -626,7 +626,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
{
#if 0
debug() << "(sr::get_array) string of unknown size: "
<< from_expr(size_val) << eom;
<< from_expr(ns, "", size_val) << eom;
#endif
return empty_ret;
}
Expand Down Expand Up @@ -699,7 +699,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
else
{
#if 0
debug() << "unable to get array-list value of " << from_expr(arr)
debug() << "unable to get array-list value of " << from_expr(ns, "", arr)
<< " of size " << n << eom;
#endif
return array_of_exprt(from_integer(0, char_type), ret_type);
Expand Down Expand Up @@ -787,14 +787,14 @@ void string_refinementt::fill_model()

current_model[elength]=len;
current_model[econtent]=arr;
debug() << from_expr(to_symbol_expr(it.first)) << "="
<< from_expr(refined);
debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
<< from_expr(ns, "", refined);

if(arr.id()==ID_array)
debug() << " = \"" << string_of_array(to_array_expr(arr))
<< "\" (size:" << from_expr(len) << ")"<< eom;
<< "\" (size:" << from_expr(ns, "", len) << ")"<< eom;
else
debug() << " = " << from_expr(arr) << " (size:" << from_expr(len)
debug() << " = " << from_expr(ns, "", arr) << " (size:" << from_expr(ns, "", len)
<< ")" << eom;
}
else
Expand All @@ -806,22 +806,22 @@ void string_refinementt::fill_model()
exprt arr_model=get_array(arr);
current_model[it.first]=arr_model;

debug() << from_expr(to_symbol_expr(it.first)) << "="
<< from_expr(arr) << " = " << from_expr(arr_model) << "" << eom;
debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
<< from_expr(ns, "", arr) << " = " << from_expr(ns, "", arr_model) << "" << eom;
}
}

for(auto it : generator.boolean_symbols)
{
debug() << "" << it.get_identifier() << " := "
<< from_expr(supert::get(it)) << eom;
<< from_expr(ns, "", supert::get(it)) << eom;
current_model[it]=supert::get(it);
}

for(auto it : generator.index_symbols)
{
debug() << "" << it.get_identifier() << " := "
<< from_expr(supert::get(it)) << eom;
<< from_expr(ns, "", supert::get(it)) << eom;
current_model[it]=supert::get(it);
}
}
Expand Down Expand Up @@ -956,7 +956,7 @@ void string_refinementt::add_negation_of_constraint_to_solver(
and_exprt premise(axiom.premise(), axiom.univ_within_bounds());
and_exprt negaxiom(premise, not_exprt(axiom.body()));

debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;
debug() << "(sr::check_axioms) negated axiom: " << from_expr(ns, "", negaxiom) << eom;
substitute_array_access(negaxiom);
solver << negaxiom;
}
Expand Down Expand Up @@ -1000,7 +1000,7 @@ bool string_refinementt::check_axioms()
exprt val=solver.get(axiom_in_model.univ_var());
debug() << "string constraint can be violated for "
<< axiom_in_model.univ_var().get_identifier()
<< " = " << from_expr(val) << eom;
<< " = " << from_expr(ns, "", val) << eom;
violated[i]=val;
}
break;
Expand Down Expand Up @@ -1047,7 +1047,7 @@ bool string_refinementt::check_axioms()
implies_exprt instance(premise, body);
replace_expr(symbol_resolve, instance);
replace_expr(axiom.univ_var(), val, instance);
debug() << "adding counter example " << from_expr(instance) << eom;
debug() << "adding counter example " << from_expr(ns, "", instance) << eom;
add_lemma(instance);
}
}
Expand Down Expand Up @@ -1282,8 +1282,8 @@ void string_refinementt::add_to_index_set(const exprt &s, exprt i)
}
if(index_set[s].insert(i).second)
{
debug() << "adding to index set of " << from_expr(s)
<< ": " << from_expr(i) << eom;
debug() << "adding to index set of " << from_expr(ns, "", s)
<< ": " << from_expr(ns, "", i) << eom;
current_index_set[s].insert(i);
}
}
Expand Down Expand Up @@ -1429,15 +1429,16 @@ void string_refinementt::instantiate_not_contains(
exprt s0=axiom.s0();
exprt s1=axiom.s1();

debug() << "instantiate not contains " << from_expr(s0) << " : "
<< from_expr(s1) << eom;
debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "
<< from_expr(ns, "", s1) << eom;
expr_sett index_set0=index_set[to_string_expr(s0).content()];
expr_sett index_set1=index_set[to_string_expr(s1).content()];

for(auto it0 : index_set0)
for(auto it1 : index_set1)
{
debug() << from_expr(it0) << " : " << from_expr(it1) << eom;
debug() << from_expr(ns, "", it0) << " : " << from_expr(ns, "", it1)
<< eom;
exprt val=minus_exprt(it0, it1);
exprt witness=generator.get_witness_of(axiom, val);
and_exprt prem_and_is_witness(
Expand Down