Skip to content
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

Drop inheritance of string_constraints from exprt #1967

Merged
merged 2 commits into from
Jun 1, 2018
Merged

Drop inheritance of string_constraints from exprt #1967

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0ffd0ae
Replace negation of constraint by a method
romainbrenguier Mar 22, 2018
c6c2928
Drop inheritance from constraint on exprt
romainbrenguier Mar 22, 2018
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
6 changes: 2 additions & 4 deletions jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,10 +206,8 @@ SCENARIO("instantiate_not_contains",
constraints.end(),
axioms,
[&](const std::string &accu, string_constraintt sc) {
simplify(sc, ns);
std::string s;
java_lang->from_expr(sc, s, ns);
return accu + s + "\n\n";
simplify(sc.body, ns);
return accu + to_string(sc) + "\n\n";
});

const auto nc_contraints = generator.get_not_contains_constraints();
Expand Down
97 changes: 37 additions & 60 deletions src/solvers/refinement/string_constraint.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ Author: Romain Brenguier, [email protected]
#include <util/format_type.h>
#include <util/refined_string_type.h>
#include <util/string_expr.h>
#include <util/union_find_replace.h>

/// ### Universally quantified string constraint
///
Expand Down Expand Up @@ -54,84 +55,60 @@ Author: Romain Brenguier, [email protected]
/// \f$f\f$ [explicitly stated, implied].
///
/// \todo The fact that we follow this grammar is not enforced at the moment.
class string_constraintt : public exprt
class string_constraintt final
{
public:
// String constraints are of the form
// forall univ_var in [lower_bound,upper_bound[. premise => body
// forall univ_var in [lower_bound,upper_bound[. body
symbol_exprt univ_var;
exprt lower_bound;
exprt upper_bound;
exprt body;

const exprt &premise() const
{
return op0();
}
string_constraintt() = delete;

const exprt &body() const
string_constraintt(
symbol_exprt _univ_var,
exprt lower_bound,
exprt upper_bound,
exprt body)
: univ_var(_univ_var),
lower_bound(lower_bound),
upper_bound(upper_bound),
body(body)
{
return op1();
}

const symbol_exprt &univ_var() const
// Default bound inferior is 0
string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
: string_constraintt(
univ_var,
from_integer(0, univ_var.type()),
upper_bound,
body)
{
return to_symbol_expr(op2());
}

const exprt &upper_bound() const
exprt univ_within_bounds() const
{
return op3();
return and_exprt(
binary_relation_exprt(lower_bound, ID_le, univ_var),
binary_relation_exprt(upper_bound, ID_gt, univ_var));
}

const exprt &lower_bound() const
void replace_expr(union_find_replacet &replace_map)
{
return operands()[4];
replace_map.replace_expr(lower_bound);
replace_map.replace_expr(upper_bound);
replace_map.replace_expr(body);
}

private:
string_constraintt();

public:
string_constraintt(
const symbol_exprt &_univ_var,
const exprt &bound_inf,
const exprt &bound_sup,
const exprt &body):
exprt(ID_string_constraint)
exprt negation() const
{
copy_to_operands(true_exprt(), body);
copy_to_operands(_univ_var, bound_sup, bound_inf);
}

// Default bound inferior is 0
string_constraintt(
const symbol_exprt &_univ_var,
const exprt &bound_sup,
const exprt &body):
string_constraintt(
_univ_var,
from_integer(0, _univ_var.type()),
bound_sup,
body)
{}

exprt univ_within_bounds() const
{
return and_exprt(
binary_relation_exprt(lower_bound(), ID_le, univ_var()),
binary_relation_exprt(upper_bound(), ID_gt, univ_var()));
return and_exprt(univ_within_bounds(), not_exprt(body));
}
};

extern inline const string_constraintt &to_string_constraint(const exprt &expr)
{
PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
return static_cast<const string_constraintt &>(expr);
}

extern inline string_constraintt &to_string_constraint(exprt &expr)
{
PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
return static_cast<string_constraintt &>(expr);
}

/// Used for debug printing.
/// \param [in] ns: namespace for `from_expr`
/// \param [in] identifier: identifier for `from_expr`
Expand All @@ -140,9 +117,9 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
inline std::string to_string(const string_constraintt &expr)
{
std::ostringstream out;
out << "forall " << format(expr.univ_var()) << " in ["
<< format(expr.lower_bound()) << ", " << format(expr.upper_bound())
<< "). " << format(expr.premise()) << " => " << format(expr.body());
out << "forall " << format(expr.univ_var) << " in ["
<< format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
<< format(expr.body);
return out.str();
}

Expand Down
Loading