Skip to content

Commit 3394320

Browse files
committed
Add equal to smt core theory
1 parent 4050a5e commit 3394320

File tree

3 files changed

+72
-0
lines changed

3 files changed

+72
-0
lines changed

src/solvers/smt2_incremental/smt_core_theory.cpp

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,26 @@ void smt_core_theoryt::nott::validate(const smt_termt &operand)
2121

2222
const smt_function_application_termt::factoryt<smt_core_theoryt::nott>
2323
smt_core_theoryt::make_not{};
24+
25+
const char *smt_core_theoryt::equalt::identifier()
26+
{
27+
return "=";
28+
}
29+
30+
smt_sortt
31+
smt_core_theoryt::equalt::return_sort(const smt_termt &, const smt_termt &)
32+
{
33+
return smt_bool_sortt{};
34+
}
35+
36+
void smt_core_theoryt::equalt::validate(
37+
const smt_termt &lhs,
38+
const smt_termt &rhs)
39+
{
40+
INVARIANT(
41+
lhs.get_sort() == rhs.get_sort(),
42+
"\"=\" may only be applied to terms which have the same sort.");
43+
}
44+
45+
const smt_function_application_termt::factoryt<smt_core_theoryt::equalt>
46+
smt_core_theoryt::equal{};

src/solvers/smt2_incremental/smt_core_theory.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,14 @@ class smt_core_theoryt
1515
static void validate(const smt_termt &operand);
1616
};
1717
static const smt_function_application_termt::factoryt<nott> make_not;
18+
19+
struct equalt final
20+
{
21+
static const char *identifier();
22+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
23+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
24+
};
25+
static const smt_function_application_termt::factoryt<equalt> equal;
1826
};
1927

2028
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H

unit/solvers/smt2_incremental/smt_core_theory.cpp

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,44 @@ TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]")
2121
cbmc_invariants_should_throwt invariants_throw;
2222
CHECK_THROWS(smt_core_theoryt::make_not(smt_bit_vector_constant_termt{0, 1}));
2323
}
24+
25+
TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]")
26+
{
27+
SECTION("Bool sorted term comparison")
28+
{
29+
const smt_bool_literal_termt true_term{true};
30+
const smt_bool_literal_termt false_term{false};
31+
const auto bool_comparison = smt_core_theoryt::equal(true_term, false_term);
32+
CHECK(bool_comparison.get_sort() == smt_bool_sortt{});
33+
CHECK(
34+
bool_comparison.function_identifier() ==
35+
smt_identifier_termt{"=", smt_bool_sortt{}});
36+
REQUIRE(bool_comparison.arguments().size() == 2);
37+
REQUIRE(bool_comparison.arguments()[0].get() == true_term);
38+
REQUIRE(bool_comparison.arguments()[1].get() == false_term);
39+
}
40+
41+
SECTION("Bit vector sorted term comparison")
42+
{
43+
const smt_bit_vector_constant_termt two{2, 8};
44+
const smt_bit_vector_constant_termt three{3, 8};
45+
const auto bit_vector_comparison = smt_core_theoryt::equal(two, three);
46+
CHECK(bit_vector_comparison.get_sort() == smt_bool_sortt{});
47+
CHECK(
48+
bit_vector_comparison.function_identifier() ==
49+
smt_identifier_termt{"=", smt_bool_sortt{}});
50+
REQUIRE(bit_vector_comparison.arguments().size() == 2);
51+
REQUIRE(bit_vector_comparison.arguments()[0].get() == two);
52+
REQUIRE(bit_vector_comparison.arguments()[1].get() == three);
53+
}
54+
55+
SECTION("Mismatch sort invariant")
56+
{
57+
cbmc_invariants_should_throwt invariants_throw;
58+
CHECK_THROWS(smt_core_theoryt::equal(
59+
smt_bit_vector_constant_termt{2, 8},
60+
smt_bit_vector_constant_termt{2, 16}));
61+
CHECK_THROWS(smt_core_theoryt::equal(
62+
smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true}));
63+
}
64+
}

0 commit comments

Comments
 (0)