Skip to content

Commit 7eef276

Browse files
kroeningkroening
authored
Merge pull request #8524 from diffblue/smt2-onehot
SMT2: support `onehot` and `onehot0`
2 parents c902db3 + 7e39d04 commit 7eef276

File tree

6 files changed

+196
-2
lines changed

6 files changed

+196
-2
lines changed

‎src/solvers/flattening/boolbv.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -412,8 +412,10 @@ literalt boolbvt::convert_rest(const exprt &expr)
412412
expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
413413
expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
414414
return convert_reduction(to_unary_expr(expr));
415-
else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
416-
return convert_onehot(to_unary_expr(expr));
415+
else if(expr.id() == ID_onehot)
416+
return convert_onehot(to_onehot_expr(expr));
417+
else if(expr.id() == ID_onehot0)
418+
return convert_onehot(to_onehot0_expr(expr));
417419
else if(
418420
const auto binary_overflow =
419421
expr_try_dynamic_cast<binary_overflow_exprt>(expr))

‎src/solvers/smt2/smt2_conv.cpp

+8
Original file line numberDiff line numberDiff line change
@@ -1831,6 +1831,14 @@ void smt2_convt::convert_expr(const exprt &expr)
18311831
out << ")) #b1)"; // bvlshr, extract, =
18321832
}
18331833
}
1834+
else if(expr.id() == ID_onehot)
1835+
{
1836+
convert_expr(to_onehot_expr(expr).lower());
1837+
}
1838+
else if(expr.id() == ID_onehot0)
1839+
{
1840+
convert_expr(to_onehot0_expr(expr).lower());
1841+
}
18341842
else if(expr.id()==ID_extractbits)
18351843
{
18361844
const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr);

‎src/util/bitvector_expr.cpp

+34
Original file line numberDiff line numberDiff line change
@@ -306,3 +306,37 @@ exprt zero_extend_exprt::lower() const
306306
return extractbits_exprt{op(), 0, type()};
307307
}
308308
}
309+
310+
static exprt onehot_lowering(const exprt &expr)
311+
{
312+
exprt one_seen = false_exprt{};
313+
const auto width = to_bitvector_type(expr.type()).get_width();
314+
exprt::operandst more_than_one_seen_disjuncts;
315+
more_than_one_seen_disjuncts.reserve(width);
316+
317+
for(std::size_t i = 0; i < width; i++)
318+
{
319+
auto bit = extractbit_exprt{expr, i};
320+
more_than_one_seen_disjuncts.push_back(and_exprt{bit, one_seen});
321+
one_seen = or_exprt{one_seen, bit};
322+
}
323+
324+
auto more_than_one_seen = disjunction(more_than_one_seen_disjuncts);
325+
326+
return and_exprt{one_seen, not_exprt{more_than_one_seen}};
327+
}
328+
329+
exprt onehot_exprt::lower() const
330+
{
331+
auto symbol = symbol_exprt{"onehot-op", op().type()};
332+
333+
return let_exprt{symbol, op(), onehot_lowering(symbol)};
334+
}
335+
336+
exprt onehot0_exprt::lower() const
337+
{
338+
auto symbol = symbol_exprt{"onehot-op", op().type()};
339+
340+
// same as onehot, but on flipped operand bits
341+
return let_exprt{symbol, bitnot_exprt{op()}, onehot_lowering(symbol)};
342+
}

‎src/util/bitvector_expr.h

+70
Original file line numberDiff line numberDiff line change
@@ -1742,4 +1742,74 @@ inline zero_extend_exprt &to_zero_extend_expr(exprt &expr)
17421742
return static_cast<zero_extend_exprt &>(expr);
17431743
}
17441744

1745+
/// \brief A Boolean expression returning true iff the given
1746+
/// operand consists of exactly one '1' and '0' otherwise.
1747+
class onehot_exprt : public unary_predicate_exprt
1748+
{
1749+
public:
1750+
explicit onehot_exprt(exprt _op)
1751+
: unary_predicate_exprt(ID_onehot, std::move(_op))
1752+
{
1753+
}
1754+
1755+
/// lowering to extractbit
1756+
exprt lower() const;
1757+
};
1758+
1759+
/// \brief Cast an exprt to a \ref onehot_exprt
1760+
///
1761+
/// \a expr must be known to be \ref onehot_exprt.
1762+
///
1763+
/// \param expr: Source expression
1764+
/// \return Object of type \ref onehot_exprt
1765+
inline const onehot_exprt &to_onehot_expr(const exprt &expr)
1766+
{
1767+
PRECONDITION(expr.id() == ID_onehot);
1768+
onehot_exprt::check(expr);
1769+
return static_cast<const onehot_exprt &>(expr);
1770+
}
1771+
1772+
/// \copydoc to_onehot_expr(const exprt &)
1773+
inline onehot_exprt &to_onehot_expr(exprt &expr)
1774+
{
1775+
PRECONDITION(expr.id() == ID_onehot);
1776+
onehot_exprt::check(expr);
1777+
return static_cast<onehot_exprt &>(expr);
1778+
}
1779+
1780+
/// \brief A Boolean expression returning true iff the given
1781+
/// operand consists of exactly one '0' and '1' otherwise.
1782+
class onehot0_exprt : public unary_predicate_exprt
1783+
{
1784+
public:
1785+
explicit onehot0_exprt(exprt _op)
1786+
: unary_predicate_exprt(ID_onehot0, std::move(_op))
1787+
{
1788+
}
1789+
1790+
/// lowering to extractbit
1791+
exprt lower() const;
1792+
};
1793+
1794+
/// \brief Cast an exprt to a \ref onehot0_exprt
1795+
///
1796+
/// \a expr must be known to be \ref onehot0_exprt.
1797+
///
1798+
/// \param expr: Source expression
1799+
/// \return Object of type \ref onehot0_exprt
1800+
inline const onehot0_exprt &to_onehot0_expr(const exprt &expr)
1801+
{
1802+
PRECONDITION(expr.id() == ID_onehot0);
1803+
onehot0_exprt::check(expr);
1804+
return static_cast<const onehot0_exprt &>(expr);
1805+
}
1806+
1807+
/// \copydoc to_onehot0_expr(const exprt &)
1808+
inline onehot0_exprt &to_onehot0_expr(exprt &expr)
1809+
{
1810+
PRECONDITION(expr.id() == ID_onehot0);
1811+
onehot0_exprt::check(expr);
1812+
return static_cast<onehot0_exprt &>(expr);
1813+
}
1814+
17451815
#endif // CPROVER_UTIL_BITVECTOR_EXPR_H

‎unit/util/bitvector_expr.cpp

+78
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,15 @@
11
// Author: Diffblue Ltd.
22

3+
#include <util/arith_tools.h>
34
#include <util/bitvector_expr.h>
45
#include <util/bitvector_types.h>
6+
#include <util/cout_message.h>
7+
#include <util/namespace.h>
8+
#include <util/std_expr.h>
9+
#include <util/symbol_table.h>
510

11+
#include <solvers/flattening/boolbv.h>
12+
#include <solvers/sat/satcheck.h>
613
#include <testing-utils/use_catch.h>
714

815
TEST_CASE(
@@ -64,3 +71,74 @@ TEMPLATE_TEST_CASE(
6471
}
6572
}
6673
}
74+
75+
TEST_CASE("onehot expression lowering", "[core][util][expr]")
76+
{
77+
console_message_handlert message_handler;
78+
message_handler.set_verbosity(0);
79+
satcheckt satcheck{message_handler};
80+
symbol_tablet symbol_table;
81+
namespacet ns{symbol_table};
82+
boolbvt boolbv{ns, satcheck, message_handler};
83+
unsignedbv_typet u8{8};
84+
85+
GIVEN("A bit-vector that is one-hot")
86+
{
87+
boolbv << onehot_exprt{from_integer(64, u8)}.lower();
88+
89+
THEN("the lowering of onehot is true")
90+
{
91+
REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
92+
}
93+
}
94+
95+
GIVEN("A bit-vector that is not one-hot")
96+
{
97+
boolbv << onehot_exprt{from_integer(5, u8)}.lower();
98+
99+
THEN("the lowering of onehot is false")
100+
{
101+
REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
102+
}
103+
}
104+
105+
GIVEN("A bit-vector that is not one-hot")
106+
{
107+
boolbv << onehot_exprt{from_integer(0, u8)}.lower();
108+
109+
THEN("the lowering of onehot is false")
110+
{
111+
REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
112+
}
113+
}
114+
115+
GIVEN("A bit-vector that is one-hot 0")
116+
{
117+
boolbv << onehot0_exprt{from_integer(0xfe, u8)}.lower();
118+
119+
THEN("the lowering of onehot0 is true")
120+
{
121+
REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
122+
}
123+
}
124+
125+
GIVEN("A bit-vector that is not one-hot 0")
126+
{
127+
boolbv << onehot0_exprt{from_integer(0x7e, u8)}.lower();
128+
129+
THEN("the lowering of onehot0 is false")
130+
{
131+
REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
132+
}
133+
}
134+
135+
GIVEN("A bit-vector that is not one-hot 0")
136+
{
137+
boolbv << onehot0_exprt{from_integer(0xff, u8)}.lower();
138+
139+
THEN("the lowering of onehot0 is false")
140+
{
141+
REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
142+
}
143+
}
144+
}

‎unit/util/module_dependencies.txt

+2
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,4 @@
11
testing-utils
22
util
3+
solvers/flattening
4+
solvers/sat

0 commit comments

Comments
 (0)