Skip to content

SMT2: range_type fixes #8537

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.

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 3 commits into from
Feb 4, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
67 changes: 60 additions & 7 deletions src/solvers/smt2/smt2_conv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -517,11 +517,14 @@
std::size_t width=boolbv_width(type);
return constant_exprt(integer2bvrep(value, width), type);
}
else if(type.id()==ID_integer ||
type.id()==ID_range)
else if(type.id() == ID_integer)

Check warning on line 520 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L520

Added line #L520 was not covered by tests
{
return from_integer(value, type);
}
else if(type.id() == ID_range)

Check warning on line 524 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L524

Added line #L524 was not covered by tests
{
return from_integer(value + to_range_type(type).get_from(), type);

Check warning on line 526 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L526

Added line #L526 was not covered by tests
}
else
UNREACHABLE_BECAUSE(
"smt2_convt::parse_literal should not be of unsupported type " +
Expand Down Expand Up @@ -1317,17 +1320,26 @@
else if(expr.id()==ID_unary_minus)
{
const unary_minus_exprt &unary_minus_expr = to_unary_minus_expr(expr);
const auto &type = expr.type();

if(
unary_minus_expr.type().id() == ID_rational ||
unary_minus_expr.type().id() == ID_integer ||
unary_minus_expr.type().id() == ID_real)
type.id() == ID_rational || type.id() == ID_integer ||
type.id() == ID_real)
{
out << "(- ";
convert_expr(unary_minus_expr.op());
out << ")";
}
else if(unary_minus_expr.type().id() == ID_floatbv)
else if(type.id() == ID_range)
{
auto &range_type = to_range_type(type);
PRECONDITION(type == unary_minus_expr.op().type());

Check warning on line 1336 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1335-L1336

Added lines #L1335 - L1336 were not covered by tests
// turn -x into 0-x
auto minus_expr =
minus_exprt{range_type.zero_expr(), unary_minus_expr.op()};
convert_expr(minus_expr);

Check warning on line 1340 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1338-L1340

Added lines #L1338 - L1340 were not covered by tests
}
else if(type.id() == ID_floatbv)
{
// this has no rounding mode
if(use_FPA_theory)
Expand Down Expand Up @@ -3783,7 +3795,7 @@
}
else if(
expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
expr.type().id() == ID_fixedbv || expr.type().id() == ID_range)
expr.type().id() == ID_fixedbv)
{
// These could be chained, i.e., need not be binary,
// but at least MathSat doesn't like that.
Expand All @@ -3800,6 +3812,31 @@
convert_plus(to_plus_expr(make_binary(expr)));
}
}
else if(expr.type().id() == ID_range)
{
auto &range_type = to_range_type(expr.type());

Check warning on line 3817 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L3817

Added line #L3817 was not covered by tests

// These could be chained, i.e., need not be binary,
// but at least MathSat doesn't like that.
if(expr.operands().size() == 2)
{
// add: lhs + from + rhs + from - from = lhs + rhs + from
mp_integer from = range_type.get_from();
const auto size = range_type.get_to() - range_type.get_from() + 1;
const auto width = address_bits(size);

Check warning on line 3826 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L3824-L3826

Added lines #L3824 - L3826 were not covered by tests

out << "(bvadd ";
convert_expr(expr.op0());
out << " (bvadd ";
convert_expr(expr.op1());
out << " (_ bv" << range_type.get_from() << ' ' << width
<< ")))"; // bv, bvadd, bvadd

Check warning on line 3833 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L3828-L3833

Added lines #L3828 - L3833 were not covered by tests
}
else
{
convert_plus(to_plus_expr(make_binary(expr)));

Check warning on line 3837 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L3837

Added line #L3837 was not covered by tests
}
}
else if(expr.type().id() == ID_floatbv)
{
// Floating-point additions should have be been converted
Expand Down Expand Up @@ -4037,6 +4074,22 @@
"unsupported operand types for -: " + expr.op0().type().id_string() +
" and " + expr.op1().type().id_string());
}
else if(expr.type().id() == ID_range)

Check warning on line 4077 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L4077

Added line #L4077 was not covered by tests
{
auto &range_type = to_range_type(expr.type());

Check warning on line 4079 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L4079

Added line #L4079 was not covered by tests

// sub: lhs + from - (rhs + from) - from = lhs - rhs - from
mp_integer from = range_type.get_from();
const auto size = range_type.get_to() - range_type.get_from() + 1;
const auto width = address_bits(size);

Check warning on line 4084 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L4082-L4084

Added lines #L4082 - L4084 were not covered by tests

out << "(bvsub (bvsub ";
convert_expr(expr.op0());
out << ' ';
convert_expr(expr.op1());
out << ") (_ bv" << range_type.get_from() << ' ' << width
<< "))"; // bv, bvsub

Check warning on line 4091 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L4086-L4091

Added lines #L4086 - L4091 were not covered by tests
}
else
UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
}
Expand Down
17 changes: 17 additions & 0 deletions src/util/std_types.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -165,6 +165,23 @@
set_width(numeric_cast_v<std::size_t>(width));
}

bool range_typet::includes(const mp_integer &singleton) const

Check warning on line 168 in src/util/std_types.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_types.cpp#L168

Added line #L168 was not covered by tests
{
return get_from() <= singleton && singleton <= get_to();

Check warning on line 170 in src/util/std_types.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_types.cpp#L170

Added line #L170 was not covered by tests
}

constant_exprt range_typet::one_expr() const

Check warning on line 173 in src/util/std_types.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_types.cpp#L173

Added line #L173 was not covered by tests
{
PRECONDITION(includes(1));
return constant_exprt{ID_1, *this};

Check warning on line 176 in src/util/std_types.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_types.cpp#L175-L176

Added lines #L175 - L176 were not covered by tests
}

constant_exprt range_typet::zero_expr() const

Check warning on line 179 in src/util/std_types.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_types.cpp#L179

Added line #L179 was not covered by tests
{
PRECONDITION(includes(0));
return constant_exprt{ID_0, *this};

Check warning on line 182 in src/util/std_types.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_types.cpp#L181-L182

Added lines #L181 - L182 were not covered by tests
}

void range_typet::set_from(const mp_integer &from)
{
set(ID_from, integer2string(from));
Expand Down
3 changes: 3 additions & 0 deletions src/util/std_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -1012,6 +1012,9 @@ class range_typet:public typet

mp_integer get_from() const;
mp_integer get_to() const;
bool includes(const mp_integer &) const;
constant_exprt zero_expr() const;
constant_exprt one_expr() const;

void set_from(const mp_integer &_from);
void set_to(const mp_integer &to);
Expand Down
Loading