Skip to content

Commit 84b7bac

Browse files
thomasspriggsthomasspriggs
committed
Add QF_BF bitwise operators
1 parent 45f3839 commit 84b7bac

File tree

3 files changed

+181
-0
lines changed

3 files changed

+181
-0
lines changed

‎src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,94 @@ void smt_bit_vector_theoryt::ort::validate(
143143
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::ort>
144144
smt_bit_vector_theoryt::make_or{};
145145

146+
const char *smt_bit_vector_theoryt::nandt::identifier()
147+
{
148+
return "bvnand";
149+
}
150+
151+
smt_sortt smt_bit_vector_theoryt::nandt::return_sort(
152+
const smt_termt &lhs,
153+
const smt_termt &rhs)
154+
{
155+
return lhs.get_sort();
156+
}
157+
158+
void smt_bit_vector_theoryt::nandt::validate(
159+
const smt_termt &lhs,
160+
const smt_termt &rhs)
161+
{
162+
validate_bit_vector_operator_arguments(lhs, rhs);
163+
}
164+
165+
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nandt>
166+
smt_bit_vector_theoryt::nand{};
167+
168+
const char *smt_bit_vector_theoryt::nort::identifier()
169+
{
170+
return "bvnor";
171+
}
172+
173+
smt_sortt smt_bit_vector_theoryt::nort::return_sort(
174+
const smt_termt &lhs,
175+
const smt_termt &rhs)
176+
{
177+
return lhs.get_sort();
178+
}
179+
180+
void smt_bit_vector_theoryt::nort::validate(
181+
const smt_termt &lhs,
182+
const smt_termt &rhs)
183+
{
184+
validate_bit_vector_operator_arguments(lhs, rhs);
185+
}
186+
187+
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nort>
188+
smt_bit_vector_theoryt::nor{};
189+
190+
const char *smt_bit_vector_theoryt::xort::identifier()
191+
{
192+
return "bvxor";
193+
}
194+
195+
smt_sortt smt_bit_vector_theoryt::xort::return_sort(
196+
const smt_termt &lhs,
197+
const smt_termt &rhs)
198+
{
199+
return lhs.get_sort();
200+
}
201+
202+
void smt_bit_vector_theoryt::xort::validate(
203+
const smt_termt &lhs,
204+
const smt_termt &rhs)
205+
{
206+
validate_bit_vector_operator_arguments(lhs, rhs);
207+
}
208+
209+
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xort>
210+
smt_bit_vector_theoryt::make_xor{};
211+
212+
const char *smt_bit_vector_theoryt::xnort::identifier()
213+
{
214+
return "bvxnor";
215+
}
216+
217+
smt_sortt smt_bit_vector_theoryt::xnort::return_sort(
218+
const smt_termt &lhs,
219+
const smt_termt &rhs)
220+
{
221+
return lhs.get_sort();
222+
}
223+
224+
void smt_bit_vector_theoryt::xnort::validate(
225+
const smt_termt &lhs,
226+
const smt_termt &rhs)
227+
{
228+
validate_bit_vector_operator_arguments(lhs, rhs);
229+
}
230+
231+
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xnort>
232+
smt_bit_vector_theoryt::xnor{};
233+
146234
// Relational operator definitions
147235

148236
const char *smt_bit_vector_theoryt::unsigned_less_thant::identifier()

‎src/solvers/smt2_incremental/smt_bit_vector_theory.h

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,38 @@ class smt_bit_vector_theoryt
5353
};
5454
static const smt_function_application_termt::factoryt<ort> make_or;
5555

56+
struct nandt final
57+
{
58+
static const char *identifier();
59+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
60+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
61+
};
62+
static const smt_function_application_termt::factoryt<nandt> nand;
63+
64+
struct nort final
65+
{
66+
static const char *identifier();
67+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
68+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
69+
};
70+
static const smt_function_application_termt::factoryt<nort> nor;
71+
72+
struct xort final
73+
{
74+
static const char *identifier();
75+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
76+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
77+
};
78+
static const smt_function_application_termt::factoryt<xort> make_xor;
79+
80+
struct xnort final
81+
{
82+
static const char *identifier();
83+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
84+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
85+
};
86+
static const smt_function_application_termt::factoryt<xnort> xnor;
87+
5688
// Relational operator class declarations
5789
struct unsigned_less_thant final
5890
{

‎unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,67 @@ TEST_CASE("SMT bit vector bitwise operators", "[core][smt2_incremental]")
111111
REQUIRE_THROWS(smt_bit_vector_theoryt::make_and(three, wider));
112112
REQUIRE_THROWS(smt_bit_vector_theoryt::make_and(true_val, three));
113113
}
114+
SECTION("nand")
115+
{
116+
const auto function_application = smt_bit_vector_theoryt::nand(two, three);
117+
REQUIRE(
118+
function_application.function_identifier() ==
119+
smt_identifier_termt("bvnand", smt_bit_vector_sortt{8}));
120+
REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
121+
REQUIRE(function_application.arguments().size() == 2);
122+
REQUIRE(function_application.arguments()[0].get() == two);
123+
REQUIRE(function_application.arguments()[1].get() == three);
124+
125+
cbmc_invariants_should_throwt invariants_throw;
126+
REQUIRE_THROWS(smt_bit_vector_theoryt::nand(three, wider));
127+
REQUIRE_THROWS(smt_bit_vector_theoryt::nand(true_val, three));
128+
}
129+
SECTION("nor")
130+
{
131+
const auto function_application = smt_bit_vector_theoryt::nor(two, three);
132+
REQUIRE(
133+
function_application.function_identifier() ==
134+
smt_identifier_termt("bvnor", smt_bit_vector_sortt{8}));
135+
REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
136+
REQUIRE(function_application.arguments().size() == 2);
137+
REQUIRE(function_application.arguments()[0].get() == two);
138+
REQUIRE(function_application.arguments()[1].get() == three);
139+
140+
cbmc_invariants_should_throwt invariants_throw;
141+
REQUIRE_THROWS(smt_bit_vector_theoryt::nor(three, wider));
142+
REQUIRE_THROWS(smt_bit_vector_theoryt::nor(true_val, three));
143+
}
144+
SECTION("xor")
145+
{
146+
const auto function_application =
147+
smt_bit_vector_theoryt::make_xor(two, three);
148+
REQUIRE(
149+
function_application.function_identifier() ==
150+
smt_identifier_termt("bvxor", smt_bit_vector_sortt{8}));
151+
REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
152+
REQUIRE(function_application.arguments().size() == 2);
153+
REQUIRE(function_application.arguments()[0].get() == two);
154+
REQUIRE(function_application.arguments()[1].get() == three);
155+
156+
cbmc_invariants_should_throwt invariants_throw;
157+
REQUIRE_THROWS(smt_bit_vector_theoryt::make_xor(three, wider));
158+
REQUIRE_THROWS(smt_bit_vector_theoryt::make_xor(true_val, three));
159+
}
160+
SECTION("xnor")
161+
{
162+
const auto function_application = smt_bit_vector_theoryt::xnor(two, three);
163+
REQUIRE(
164+
function_application.function_identifier() ==
165+
smt_identifier_termt("bvxnor", smt_bit_vector_sortt{8}));
166+
REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
167+
REQUIRE(function_application.arguments().size() == 2);
168+
REQUIRE(function_application.arguments()[0].get() == two);
169+
REQUIRE(function_application.arguments()[1].get() == three);
170+
171+
cbmc_invariants_should_throwt invariants_throw;
172+
REQUIRE_THROWS(smt_bit_vector_theoryt::xnor(three, wider));
173+
REQUIRE_THROWS(smt_bit_vector_theoryt::xnor(true_val, three));
174+
}
114175
}
115176

116177
TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")

0 commit comments

Comments
 (0)