Skip to content

Commit 2061d96

Browse files
thomasspriggsthomasspriggs
committed
Add SMT2 incremental core theory operators
1 parent 47a8082 commit 2061d96

File tree

3 files changed

+154
-0
lines changed

3 files changed

+154
-0
lines changed

‎src/solvers/smt2_incremental/smt_core_theory.cpp

Lines changed: 76 additions & 0 deletions
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

Lines changed: 24 additions & 0 deletions
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

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,60 @@ TEST_CASE("SMT core theory implies.", "[core][smt2_incremental]")
3737
CHECK_THROWS(smt_core_theoryt::implies(true_term, two));
3838
}
3939

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

0 commit comments

Comments
 (0)