Skip to content

Commit cd8e888

Browse files
thomasspriggsthomasspriggs
committed
Add smt_terms data structures
1 parent d5c12a3 commit cd8e888

File tree

7 files changed

+366
-0
lines changed

7 files changed

+366
-0
lines changed

‎src/solvers/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,7 @@ SRC = $(BOOLEFORCE_SRC) \
193193
smt2/smt2_tokenizer.cpp \
194194
smt2/smt2irep.cpp \
195195
smt2_incremental/smt_sorts.cpp \
196+
smt2_incremental/smt_terms.cpp \
196197
smt2_incremental/smt_to_string.cpp \
197198
smt2_incremental/smt2_incremental_decision_procedure.cpp \
198199
# Empty last line

‎src/solvers/smt2_incremental/smt_terms.cpp

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,166 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <solvers/smt2_incremental/smt_terms.h>
4+
5+
#include <solvers/smt2_incremental/smt_sorts.h>
6+
7+
#include <util/arith_tools.h>
8+
#include <util/mp_arith.h>
9+
#include <util/range.h>
10+
11+
#include <algorithm>
12+
#include <regex>
13+
14+
// Define the irep_idts for terms.
15+
#define TERM_ID(the_id) \
16+
const irep_idt ID_smt_##the_id##_term{"smt_" #the_id "_term"};
17+
#include <solvers/smt2_incremental/smt_terms.def>
18+
#undef TERM_ID
19+
20+
smt_termt::smt_termt(irep_idt id, smt_sortt sort)
21+
: irept{id, {{ID_type, upcast(std::move(sort))}}, {}}
22+
{
23+
}
24+
25+
bool smt_termt::operator==(const smt_termt &other) const
26+
{
27+
return irept::operator==(other);
28+
}
29+
30+
bool smt_termt::operator!=(const smt_termt &other) const
31+
{
32+
return !(*this == other);
33+
}
34+
35+
const smt_sortt &smt_termt::get_sort() const
36+
{
37+
return downcast(find(ID_type));
38+
}
39+
40+
smt_bool_literal_termt::smt_bool_literal_termt(bool value)
41+
: smt_termt{ID_smt_bool_literal_term, smt_bool_sortt{}}
42+
{
43+
set(ID_value, value);
44+
}
45+
46+
bool smt_bool_literal_termt::value() const
47+
{
48+
return get_bool(ID_value);
49+
}
50+
51+
smt_not_termt::smt_not_termt(smt_termt operand)
52+
: smt_termt{ID_not, smt_bool_sortt{}}
53+
{
54+
INVARIANT(
55+
operand.get_sort() == smt_bool_sortt{},
56+
"smt_not_termt may only be applied to terms which have bool sort.");
57+
get_sub().push_back(std::move(operand));
58+
}
59+
60+
const smt_termt &smt_not_termt::operand() const
61+
{
62+
return static_cast<const smt_termt &>(get_sub().at(0));
63+
}
64+
65+
static bool is_valid_smt_identifier(irep_idt identifier)
66+
{
67+
static const std::regex valid{R"(^[^\|\\]*$)"};
68+
return std::regex_match(id2string(identifier), valid);
69+
}
70+
71+
smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
72+
: smt_termt(ID_smt_identifier_term, std::move(sort))
73+
{
74+
INVARIANT(
75+
is_valid_smt_identifier(identifier),
76+
R"(Identifiers may not contain | or \ characters.)");
77+
set(ID_identifier, identifier);
78+
}
79+
80+
irep_idt smt_identifier_termt::identifier() const
81+
{
82+
return get(ID_identifier);
83+
}
84+
85+
smt_bit_vector_constant_termt::smt_bit_vector_constant_termt(
86+
const mp_integer &value,
87+
smt_bit_vector_sortt sort)
88+
: smt_termt{ID_smt_bit_vector_constant_term, std::move(sort)}
89+
{
90+
INVARIANT(
91+
value < power(mp_integer{2}, get_sort().bit_width()),
92+
"value must fit in number of bits available.");
93+
INVARIANT(
94+
!value.is_negative(),
95+
"Negative numbers are not supported by bit vector constants.");
96+
set(ID_value, integer2bvrep(value, get_sort().bit_width()));
97+
}
98+
99+
smt_bit_vector_constant_termt::smt_bit_vector_constant_termt(
100+
const mp_integer &value,
101+
std::size_t bit_width)
102+
: smt_bit_vector_constant_termt{value, smt_bit_vector_sortt{bit_width}}
103+
{
104+
}
105+
106+
mp_integer smt_bit_vector_constant_termt::value() const
107+
{
108+
return bvrep2integer(get(ID_value), get_sort().bit_width(), false);
109+
}
110+
111+
const smt_bit_vector_sortt &smt_bit_vector_constant_termt::get_sort() const
112+
{
113+
// The below cast is sound because the constructor only allows bit_vector
114+
// sorts to be set.
115+
return static_cast<const smt_bit_vector_sortt &>(smt_termt::get_sort());
116+
}
117+
118+
smt_function_application_termt::smt_function_application_termt(
119+
smt_sortt return_sort,
120+
irep_idt function_identifier,
121+
std::vector<smt_termt> arguments)
122+
: smt_termt(ID_smt_function_application_term, std::move(return_sort))
123+
{
124+
set(ID_identifier, function_identifier);
125+
std::transform(
126+
std::make_move_iterator(arguments.begin()),
127+
std::make_move_iterator(arguments.end()),
128+
std::back_inserter(get_sub()),
129+
[](smt_termt &&argument) { return static_cast<irept &&>(argument); });
130+
}
131+
132+
irep_idt smt_function_application_termt::function_identifier() const
133+
{
134+
return get(ID_identifier);
135+
}
136+
137+
std::vector<std::reference_wrapper<const smt_termt>>
138+
smt_function_application_termt::arguments()
139+
{
140+
return make_range(get_sub()).map([](const irept &argument) {
141+
return std::cref(static_cast<const smt_termt &>(argument));
142+
});
143+
}
144+
145+
template <typename visitort>
146+
void accept(const smt_termt &term, const irep_idt &id, visitort &&visitor)
147+
{
148+
#define TERM_ID(the_id) \
149+
if(id == ID_smt_##the_id##_term) \
150+
return visitor.visit(static_cast<const smt_##the_id##_termt &>(term));
151+
// The include below is marked as nolint because including the same file
152+
// multiple times is required as part of the x macro pattern.
153+
#include <solvers/smt2_incremental/smt_terms.def> // NOLINT(build/include)
154+
#undef TERM_ID
155+
UNREACHABLE;
156+
}
157+
158+
void smt_termt::accept(smt_term_const_downcast_visitort &visitor) const
159+
{
160+
::accept(*this, id(), visitor);
161+
}
162+
163+
void smt_termt::accept(smt_term_const_downcast_visitort &&visitor) const
164+
{
165+
::accept(*this, id(), std::move(visitor));
166+
}

‎src/solvers/smt2_incremental/smt_terms.def

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
TERM_ID(bool_literal)
2+
TERM_ID(not)
3+
TERM_ID(identifier)
4+
TERM_ID(bit_vector_constant)
5+
TERM_ID(function_application)

‎src/solvers/smt2_incremental/smt_terms.h

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
// Author: Diffblue Ltd.
2+
3+
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
4+
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
5+
6+
#include <solvers/smt2_incremental/smt_sorts.h>
7+
#include <util/irep.h>
8+
9+
#include <functional>
10+
11+
class BigInt;
12+
using mp_integer = BigInt;
13+
14+
class smt_sortt;
15+
class smt_term_const_downcast_visitort;
16+
17+
class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
18+
{
19+
public:
20+
// smt_termt does not support the notion of an empty / null state. Use
21+
// optionalt<smt_termt> instead if an empty sort is required.
22+
smt_termt() = delete;
23+
24+
using irept::pretty;
25+
26+
bool operator==(const smt_termt &) const;
27+
bool operator!=(const smt_termt &) const;
28+
29+
const smt_sortt &get_sort() const;
30+
31+
void accept(smt_term_const_downcast_visitort &) const;
32+
void accept(smt_term_const_downcast_visitort &&) const;
33+
34+
protected:
35+
smt_termt(irep_idt id, smt_sortt sort);
36+
};
37+
38+
class smt_bool_literal_termt : public smt_termt
39+
{
40+
public:
41+
explicit smt_bool_literal_termt(bool value);
42+
bool value() const;
43+
};
44+
45+
class smt_not_termt : public smt_termt
46+
{
47+
public:
48+
explicit smt_not_termt(smt_termt operand);
49+
const smt_termt &operand() const;
50+
};
51+
52+
/// Stores identifiers in unescaped and unquoted form. Any escaping or quoting
53+
/// required should be performed during printing.
54+
class smt_identifier_termt : public smt_termt
55+
{
56+
public:
57+
explicit smt_identifier_termt(irep_idt identifier, smt_sortt sort);
58+
irep_idt identifier() const;
59+
};
60+
61+
class smt_bit_vector_constant_termt : public smt_termt
62+
{
63+
public:
64+
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt);
65+
smt_bit_vector_constant_termt(const mp_integer &value, std::size_t bit_width);
66+
mp_integer value() const;
67+
68+
// This deliberately hides smt_termt::get_sort, because bit_vector terms
69+
// always have bit_vector sorts.
70+
const smt_bit_vector_sortt &get_sort() const;
71+
};
72+
73+
class smt_function_application_termt : public smt_termt
74+
{
75+
smt_function_application_termt(
76+
smt_sortt return_sort,
77+
irep_idt function_identifier,
78+
std::vector<smt_termt> arguments);
79+
irep_idt function_identifier() const;
80+
std::vector<std::reference_wrapper<const smt_termt>> arguments();
81+
};
82+
83+
class smt_term_const_downcast_visitort
84+
{
85+
public:
86+
#define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
87+
#include "smt_terms.def"
88+
#undef TERM_ID
89+
};
90+
91+
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ SRC += analyses/ai/ai.cpp \
7777
solvers/sat/satcheck_cadical.cpp \
7878
solvers/sat/satcheck_minisat2.cpp \
7979
solvers/smt2_incremental/smt_sorts.cpp \
80+
solvers/smt2_incremental/smt_terms.cpp \
8081
solvers/smt2_incremental/smt_to_string.cpp \
8182
solvers/strings/array_pool/array_pool.cpp \
8283
solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \

‎unit/solvers/smt2_incremental/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
11
solvers/smt2_incremental
22
testing-utils
3+
util

‎unit/solvers/smt2_incremental/smt_terms.cpp

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <testing-utils/use_catch.h>
4+
5+
#include <solvers/smt2_incremental/smt_terms.h>
6+
7+
#include <util/mp_arith.h>
8+
9+
TEST_CASE("smt_bool_literal_termt upcasts.", "[core][smt2_incremental]")
10+
{
11+
smt_termt term{smt_bool_literal_termt{true}};
12+
term = smt_bool_literal_termt{false};
13+
}
14+
15+
TEST_CASE("Test smt_termt.pretty is accessible.", "[core][smt2_incremental]")
16+
{
17+
const smt_termt bool_term{smt_bool_literal_termt{true}};
18+
REQUIRE(
19+
bool_term.pretty(0, 0) ==
20+
"smt_bool_literal_term\n"
21+
" * type: smt_bool_sort\n"
22+
" * value: 1");
23+
}
24+
25+
TEST_CASE(
26+
"Test smt_bool_literal_termt has bool sort.",
27+
"[core][smt2_incremental]")
28+
{
29+
REQUIRE(smt_bool_literal_termt{true}.get_sort() == smt_bool_sortt{});
30+
}
31+
32+
TEST_CASE(
33+
"Test smt_bool_literal_termt value getter.",
34+
"[core][smt2_incremental]")
35+
{
36+
REQUIRE(smt_bool_literal_termt{true}.value());
37+
REQUIRE_FALSE(smt_bool_literal_termt{false}.value());
38+
}
39+
40+
TEST_CASE("smt_not_termt upcasts.", "[core][smt2_incremental]")
41+
{
42+
smt_termt not_term{smt_not_termt{smt_bool_literal_termt{false}}};
43+
not_term = smt_not_termt{smt_bool_literal_termt{true}};
44+
}
45+
46+
TEST_CASE("smt_not_termt sort.", "[core][smt2_incremental]")
47+
{
48+
REQUIRE(
49+
smt_not_termt{smt_bool_literal_termt{true}}.get_sort() == smt_bool_sortt{});
50+
}
51+
52+
TEST_CASE("smt_not_termt operand getter.", "[core][smt2_incremental]")
53+
{
54+
const smt_bool_literal_termt bool_term{true};
55+
const smt_not_termt not_term{bool_term};
56+
REQUIRE(not_term.operand() == bool_term);
57+
}
58+
59+
TEST_CASE("smt_identifier_termt construction", "[core][smt2_incremental]")
60+
{
61+
cbmc_invariants_should_throwt invariants_throw;
62+
CHECK_NOTHROW(smt_identifier_termt{"foo bar", smt_bool_sortt{}});
63+
CHECK_THROWS(smt_identifier_termt{"|foo bar|", smt_bool_sortt{}});
64+
}
65+
66+
TEST_CASE("smt_identifier_termt upcasts.", "[core][smt2_incremental]")
67+
{
68+
smt_termt term{smt_identifier_termt{"foo", smt_bool_sortt{}}};
69+
term = smt_identifier_termt{"bar", smt_bool_sortt{}};
70+
}
71+
72+
TEST_CASE("smt_identifier_termt getters.", "[core][smt2_incremental]")
73+
{
74+
const smt_identifier_termt identifier{"foo", smt_bool_sortt{}};
75+
CHECK(identifier.identifier() == "foo");
76+
CHECK(identifier.get_sort() == smt_bool_sortt{});
77+
}
78+
79+
TEST_CASE("smt_bit_vector_constant_termt getters.", "[core][smt2_incremental]")
80+
{
81+
const smt_bit_vector_constant_termt bit_vector{32, 8};
82+
CHECK(bit_vector.value() == 32);
83+
CHECK(bit_vector.get_sort() == smt_bit_vector_sortt{8});
84+
}
85+
86+
TEST_CASE("smt_termt equality.", "[core][smt2_incremental]")
87+
{
88+
smt_termt false_term = smt_bool_literal_termt{false};
89+
CHECK(false_term == false_term);
90+
CHECK(false_term == smt_bool_literal_termt{false});
91+
smt_termt true_term = smt_bool_literal_termt{true};
92+
CHECK_FALSE(false_term == true_term);
93+
CHECK(
94+
smt_bit_vector_constant_termt{42, 8} !=
95+
smt_bit_vector_constant_termt{12, 8});
96+
smt_termt not_false = smt_not_termt{smt_bool_literal_termt{false}};
97+
smt_termt not_true = smt_not_termt{smt_bool_literal_termt{true}};
98+
CHECK_FALSE(not_false == true_term);
99+
CHECK_FALSE(not_false == not_true);
100+
CHECK(not_false == smt_not_termt{smt_bool_literal_termt{false}});
101+
}

0 commit comments

Comments
 (0)