Skip to content

Commit 686ba37

Browse files
thomasspriggsthomasspriggs
committed
Add SMT2 incremental core theory logical operators
1 parent 2f09110 commit 686ba37

File tree

3 files changed

+154
-0
lines changed

3 files changed

+154
-0
lines changed

‎src/solvers/smt2_incremental/smt_core_theory.cpp

+76
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,82 @@ void smt_core_theoryt::impliest::validate(
4848
const smt_function_application_termt::factoryt<smt_core_theoryt::impliest>
4949
smt_core_theoryt::implies{};
5050

51+
const char *smt_core_theoryt::andt::identifier()
52+
{
53+
return "and";
54+
}
55+
56+
smt_sortt
57+
smt_core_theoryt::andt::return_sort(const smt_termt &, const smt_termt &)
58+
{
59+
return smt_bool_sortt{};
60+
}
61+
62+
void smt_core_theoryt::andt::validate(
63+
const smt_termt &lhs,
64+
const smt_termt &rhs)
65+
{
66+
INVARIANT(
67+
lhs.get_sort() == smt_bool_sortt{},
68+
"Left hand side of \"and\" must have bool sort.");
69+
INVARIANT(
70+
rhs.get_sort() == smt_bool_sortt{},
71+
"Right hand side of \"and\" must have bool sort.");
72+
}
73+
74+
const smt_function_application_termt::factoryt<smt_core_theoryt::andt>
75+
smt_core_theoryt::make_and{};
76+
77+
const char *smt_core_theoryt::ort::identifier()
78+
{
79+
return "or";
80+
}
81+
82+
smt_sortt
83+
smt_core_theoryt::ort::return_sort(const smt_termt &, const smt_termt &)
84+
{
85+
return smt_bool_sortt{};
86+
}
87+
88+
void smt_core_theoryt::ort::validate(const smt_termt &lhs, const smt_termt &rhs)
89+
{
90+
INVARIANT(
91+
lhs.get_sort() == smt_bool_sortt{},
92+
"Left hand side of \"or\" must have bool sort.");
93+
INVARIANT(
94+
rhs.get_sort() == smt_bool_sortt{},
95+
"Right hand side of \"or\" must have bool sort.");
96+
}
97+
98+
const smt_function_application_termt::factoryt<smt_core_theoryt::ort>
99+
smt_core_theoryt::make_or{};
100+
101+
const char *smt_core_theoryt::xort::identifier()
102+
{
103+
return "xor";
104+
}
105+
106+
smt_sortt
107+
smt_core_theoryt::xort::return_sort(const smt_termt &, const smt_termt &)
108+
{
109+
return smt_bool_sortt{};
110+
}
111+
112+
void smt_core_theoryt::xort::validate(
113+
const smt_termt &lhs,
114+
const smt_termt &rhs)
115+
{
116+
INVARIANT(
117+
lhs.get_sort() == smt_bool_sortt{},
118+
"Left hand side of \"xor\" must have bool sort.");
119+
INVARIANT(
120+
rhs.get_sort() == smt_bool_sortt{},
121+
"Right hand side of \"xor\" must have bool sort.");
122+
}
123+
124+
const smt_function_application_termt::factoryt<smt_core_theoryt::xort>
125+
smt_core_theoryt::make_xor{};
126+
51127
const char *smt_core_theoryt::equalt::identifier()
52128
{
53129
return "=";

‎src/solvers/smt2_incremental/smt_core_theory.h

+24
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,30 @@ class smt_core_theoryt
2424
};
2525
static const smt_function_application_termt::factoryt<impliest> implies;
2626

27+
struct andt final
28+
{
29+
static const char *identifier();
30+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
31+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
32+
};
33+
static const smt_function_application_termt::factoryt<andt> make_and;
34+
35+
struct ort final
36+
{
37+
static const char *identifier();
38+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
39+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
40+
};
41+
static const smt_function_application_termt::factoryt<ort> make_or;
42+
43+
struct xort final
44+
{
45+
static const char *identifier();
46+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
47+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
48+
};
49+
static const smt_function_application_termt::factoryt<xort> make_xor;
50+
2751
struct equalt final
2852
{
2953
static const char *identifier();

‎unit/solvers/smt2_incremental/smt_core_theory.cpp

+54
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,60 @@ TEST_CASE("SMT core theory implies.", "[core][smt2_incremental]")
4040
CHECK_THROWS(smt_core_theoryt::implies(true_term, two));
4141
}
4242

43+
TEST_CASE("SMT core theory \"and\".", "[core][smt2_incremental]")
44+
{
45+
const smt_bool_literal_termt true_term{true};
46+
const smt_bool_literal_termt false_term{false};
47+
const auto implies = smt_core_theoryt::make_and(true_term, false_term);
48+
CHECK(implies.get_sort() == smt_bool_sortt{});
49+
CHECK(
50+
implies.function_identifier() ==
51+
smt_identifier_termt{"and", smt_bool_sortt{}});
52+
REQUIRE(implies.arguments().size() == 2);
53+
CHECK(implies.arguments()[0].get() == true_term);
54+
CHECK(implies.arguments()[1].get() == false_term);
55+
cbmc_invariants_should_throwt invariants_throw;
56+
const smt_bit_vector_constant_termt two{2, 8};
57+
CHECK_THROWS(smt_core_theoryt::make_and(two, false_term));
58+
CHECK_THROWS(smt_core_theoryt::make_and(true_term, two));
59+
}
60+
61+
TEST_CASE("SMT core theory \"or\".", "[core][smt2_incremental]")
62+
{
63+
const smt_bool_literal_termt true_term{true};
64+
const smt_bool_literal_termt false_term{false};
65+
const auto implies = smt_core_theoryt::make_or(true_term, false_term);
66+
CHECK(implies.get_sort() == smt_bool_sortt{});
67+
CHECK(
68+
implies.function_identifier() ==
69+
smt_identifier_termt{"or", smt_bool_sortt{}});
70+
REQUIRE(implies.arguments().size() == 2);
71+
CHECK(implies.arguments()[0].get() == true_term);
72+
CHECK(implies.arguments()[1].get() == false_term);
73+
cbmc_invariants_should_throwt invariants_throw;
74+
const smt_bit_vector_constant_termt two{2, 8};
75+
CHECK_THROWS(smt_core_theoryt::make_or(two, false_term));
76+
CHECK_THROWS(smt_core_theoryt::make_or(true_term, two));
77+
}
78+
79+
TEST_CASE("SMT core theory \"xor\".", "[core][smt2_incremental]")
80+
{
81+
const smt_bool_literal_termt true_term{true};
82+
const smt_bool_literal_termt false_term{false};
83+
const auto implies = smt_core_theoryt::make_xor(true_term, false_term);
84+
CHECK(implies.get_sort() == smt_bool_sortt{});
85+
CHECK(
86+
implies.function_identifier() ==
87+
smt_identifier_termt{"xor", smt_bool_sortt{}});
88+
REQUIRE(implies.arguments().size() == 2);
89+
CHECK(implies.arguments()[0].get() == true_term);
90+
CHECK(implies.arguments()[1].get() == false_term);
91+
cbmc_invariants_should_throwt invariants_throw;
92+
const smt_bit_vector_constant_termt two{2, 8};
93+
CHECK_THROWS(smt_core_theoryt::make_xor(two, false_term));
94+
CHECK_THROWS(smt_core_theoryt::make_xor(true_term, two));
95+
}
96+
4397
TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]")
4498
{
4599
SECTION("Bool sorted term comparison")

0 commit comments

Comments
 (0)