Skip to content

Commit ce3fcaa

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #6425 from thomasspriggs/tas/smt_response_classes
Add smt response storage classes
2 parents 00c76c9 + e5db980 commit ce3fcaa

File tree

7 files changed

+457
-6
lines changed

7 files changed

+457
-6
lines changed

‎src/solvers/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -199,6 +199,7 @@ SRC = $(BOOLEFORCE_SRC) \
199199
smt2_incremental/smt_core_theory.cpp \
200200
smt2_incremental/smt_logics.cpp \
201201
smt2_incremental/smt_options.cpp \
202+
smt2_incremental/smt_responses.cpp \
202203
smt2_incremental/smt_solver_process.cpp \
203204
smt2_incremental/smt_sorts.cpp \
204205
smt2_incremental/smt_terms.cpp \

‎src/solvers/smt2_incremental/smt_responses.cpp

+175
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <solvers/smt2_incremental/smt_responses.h>
4+
5+
#include <util/range.h>
6+
7+
// Define the irep_idts for responses.
8+
#define RESPONSE_ID(the_id, the_base) \
9+
const irep_idt ID_smt_##the_id##_response{"smt_" #the_id "_response"};
10+
#include <solvers/smt2_incremental/smt_responses.def>
11+
#undef RESPONSE_ID
12+
13+
bool smt_responset::operator==(const smt_responset &other) const
14+
{
15+
return irept::operator==(other);
16+
}
17+
18+
bool smt_responset::operator!=(const smt_responset &other) const
19+
{
20+
return !(*this == other);
21+
}
22+
23+
#define RESPONSE_ID(the_id, the_base) \
24+
template <> \
25+
const smt_##the_id##_responset *the_base::cast<smt_##the_id##_responset>() \
26+
const & \
27+
{ \
28+
return id() == ID_smt_##the_id##_response \
29+
? static_cast<const smt_##the_id##_responset *>(this) \
30+
: nullptr; \
31+
}
32+
#include <solvers/smt2_incremental/smt_responses.def> // NOLINT(build/include)
33+
#undef RESPONSE_ID
34+
35+
template <typename sub_classt>
36+
const sub_classt *smt_responset::cast() const &
37+
{
38+
return nullptr;
39+
}
40+
41+
bool smt_check_sat_response_kindt::
42+
operator==(const smt_check_sat_response_kindt &other) const
43+
{
44+
return irept::operator==(other);
45+
}
46+
47+
bool smt_check_sat_response_kindt::
48+
operator!=(const smt_check_sat_response_kindt &other) const
49+
{
50+
return !(*this == other);
51+
}
52+
53+
smt_success_responset::smt_success_responset()
54+
: smt_responset{ID_smt_success_response}
55+
{
56+
}
57+
58+
smt_sat_responset::smt_sat_responset()
59+
: smt_check_sat_response_kindt{ID_smt_sat_response}
60+
{
61+
}
62+
63+
smt_unsat_responset::smt_unsat_responset()
64+
: smt_check_sat_response_kindt{ID_smt_unsat_response}
65+
{
66+
}
67+
68+
smt_unknown_responset::smt_unknown_responset()
69+
: smt_check_sat_response_kindt{ID_smt_unknown_response}
70+
{
71+
}
72+
73+
template <typename derivedt>
74+
smt_check_sat_response_kindt::storert<derivedt>::storert()
75+
{
76+
static_assert(
77+
std::is_base_of<irept, derivedt>::value &&
78+
std::is_base_of<storert<derivedt>, derivedt>::value,
79+
"Only irept based classes need to upcast smt_termt to store it.");
80+
}
81+
82+
template <typename derivedt>
83+
irept smt_check_sat_response_kindt::storert<derivedt>::upcast(
84+
smt_check_sat_response_kindt check_sat_response_kind)
85+
{
86+
return static_cast<irept &&>(std::move(check_sat_response_kind));
87+
}
88+
89+
template <typename derivedt>
90+
const smt_check_sat_response_kindt &
91+
smt_check_sat_response_kindt::storert<derivedt>::downcast(const irept &irep)
92+
{
93+
return static_cast<const smt_check_sat_response_kindt &>(irep);
94+
}
95+
96+
smt_check_sat_responset::smt_check_sat_responset(
97+
smt_check_sat_response_kindt kind)
98+
: smt_responset{ID_smt_check_sat_response}
99+
{
100+
set(ID_value, upcast(std::move(kind)));
101+
}
102+
103+
const smt_check_sat_response_kindt &smt_check_sat_responset::kind() const
104+
{
105+
return downcast(find(ID_value));
106+
}
107+
108+
smt_get_value_responset::valuation_pairt::valuation_pairt(
109+
smt_termt descriptor,
110+
smt_termt value)
111+
{
112+
get_sub().push_back(upcast(std::move(descriptor)));
113+
get_sub().push_back(upcast(std::move(value)));
114+
}
115+
116+
const smt_termt &smt_get_value_responset::valuation_pairt::descriptor() const
117+
{
118+
return downcast(get_sub().at(0));
119+
}
120+
121+
const smt_termt &smt_get_value_responset::valuation_pairt::value() const
122+
{
123+
return downcast(get_sub().at(1));
124+
}
125+
126+
bool smt_get_value_responset::valuation_pairt::
127+
operator==(const smt_get_value_responset::valuation_pairt &other) const
128+
{
129+
return irept::operator==(other);
130+
}
131+
132+
bool smt_get_value_responset::valuation_pairt::
133+
operator!=(const smt_get_value_responset::valuation_pairt &other) const
134+
{
135+
return !(*this == other);
136+
}
137+
138+
smt_get_value_responset::smt_get_value_responset(
139+
std::vector<valuation_pairt> pairs)
140+
: smt_responset(ID_smt_get_value_response)
141+
{
142+
// SMT-LIB standard version 2.6 requires one or more pairs.
143+
// See page 47, figure 3.9: Command responses.
144+
INVARIANT(
145+
!pairs.empty(), "Get value response must contain one or more pairs.");
146+
for(auto &pair : pairs)
147+
{
148+
get_sub().push_back(std::move(pair));
149+
}
150+
}
151+
152+
std::vector<
153+
std::reference_wrapper<const smt_get_value_responset::valuation_pairt>>
154+
smt_get_value_responset::pairs() const
155+
{
156+
return make_range(get_sub()).map([](const irept &pair) {
157+
return std::cref(static_cast<const valuation_pairt &>(pair));
158+
});
159+
}
160+
161+
smt_unsupported_responset::smt_unsupported_responset()
162+
: smt_responset{ID_smt_unsupported_response}
163+
{
164+
}
165+
166+
smt_error_responset::smt_error_responset(irep_idt message)
167+
: smt_responset{ID_smt_error_response}
168+
{
169+
set(ID_value, message);
170+
}
171+
172+
const irep_idt &smt_error_responset::message() const
173+
{
174+
return get(ID_value);
175+
}

‎src/solvers/smt2_incremental/smt_responses.def

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
/// \file
2+
/// This set of definitions is used as part of the
3+
/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
4+
/// set of responses which are implemented and it is used to automate repetitive
5+
/// parts of the implementation. These include -
6+
/// * The constant `irep_idt`s used to identify each of the response classes.
7+
/// * The public base classes used for implementing down casting.
8+
RESPONSE_ID(success, smt_responset)
9+
RESPONSE_ID(sat, smt_check_sat_response_kindt)
10+
RESPONSE_ID(unsat, smt_check_sat_response_kindt)
11+
RESPONSE_ID(unknown, smt_check_sat_response_kindt)
12+
RESPONSE_ID(check_sat, smt_responset)
13+
RESPONSE_ID(get_value, smt_responset)
14+
RESPONSE_ID(unsupported, smt_responset)
15+
RESPONSE_ID(error, smt_responset)

‎src/solvers/smt2_incremental/smt_responses.h

+114
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
44
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
55

6+
#include "smt_terms.h"
67
#include <util/irep.h>
78

89
class smt_responset : protected irept
@@ -14,8 +15,121 @@ class smt_responset : protected irept
1415

1516
using irept::pretty;
1617

18+
bool operator==(const smt_responset &) const;
19+
bool operator!=(const smt_responset &) const;
20+
21+
template <typename sub_classt>
22+
const sub_classt *cast() const &;
23+
1724
protected:
1825
using irept::irept;
1926
};
2027

28+
class smt_success_responset : public smt_responset
29+
{
30+
public:
31+
smt_success_responset();
32+
};
33+
34+
class smt_check_sat_response_kindt : protected irept
35+
{
36+
public:
37+
// smt_responset does not support the notion of an empty / null state. Use
38+
// optionalt<smt_responset> instead if an empty response is required.
39+
smt_check_sat_response_kindt() = delete;
40+
41+
using irept::pretty;
42+
43+
bool operator==(const smt_check_sat_response_kindt &) const;
44+
bool operator!=(const smt_check_sat_response_kindt &) const;
45+
46+
template <typename sub_classt>
47+
const sub_classt *cast() const &;
48+
49+
/// \brief Class for adding the ability to up and down cast
50+
/// smt_check_sat_response_kindt to and from irept. These casts are required
51+
/// by other irept derived classes in order to store instances of smt_termt
52+
/// inside them.
53+
/// \tparam derivedt The type of class which derives from this class and from
54+
/// irept.
55+
template <typename derivedt>
56+
class storert
57+
{
58+
protected:
59+
storert();
60+
static irept upcast(smt_check_sat_response_kindt check_sat_response_kind);
61+
static const smt_check_sat_response_kindt &downcast(const irept &);
62+
};
63+
64+
protected:
65+
using irept::irept;
66+
};
67+
68+
class smt_sat_responset : public smt_check_sat_response_kindt
69+
{
70+
public:
71+
smt_sat_responset();
72+
};
73+
74+
class smt_unsat_responset : public smt_check_sat_response_kindt
75+
{
76+
public:
77+
smt_unsat_responset();
78+
};
79+
80+
class smt_unknown_responset : public smt_check_sat_response_kindt
81+
{
82+
public:
83+
smt_unknown_responset();
84+
};
85+
86+
class smt_check_sat_responset
87+
: public smt_responset,
88+
private smt_check_sat_response_kindt::storert<smt_check_sat_responset>
89+
{
90+
public:
91+
explicit smt_check_sat_responset(smt_check_sat_response_kindt kind);
92+
const smt_check_sat_response_kindt &kind() const;
93+
};
94+
95+
class smt_get_value_responset
96+
: public smt_responset,
97+
private smt_termt::storert<smt_get_value_responset>
98+
{
99+
public:
100+
class valuation_pairt : private irept,
101+
private smt_termt::storert<valuation_pairt>
102+
{
103+
public:
104+
valuation_pairt() = delete;
105+
valuation_pairt(smt_termt descriptor, smt_termt value);
106+
107+
using irept::pretty;
108+
109+
bool operator==(const valuation_pairt &) const;
110+
bool operator!=(const valuation_pairt &) const;
111+
112+
const smt_termt &descriptor() const;
113+
const smt_termt &value() const;
114+
115+
friend smt_get_value_responset;
116+
};
117+
118+
explicit smt_get_value_responset(std::vector<valuation_pairt> pairs);
119+
std::vector<std::reference_wrapper<const valuation_pairt>> pairs() const;
120+
};
121+
122+
class smt_unsupported_responset : public smt_responset
123+
{
124+
public:
125+
smt_unsupported_responset();
126+
};
127+
128+
class smt_error_responset : public smt_responset
129+
{
130+
public:
131+
explicit smt_error_responset(irep_idt message);
132+
const irep_idt &message() const;
133+
};
134+
21135
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H

‎unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,7 @@ SRC += analyses/ai/ai.cpp \
105105
solvers/smt2_incremental/smt_bit_vector_theory.cpp \
106106
solvers/smt2_incremental/smt_commands.cpp \
107107
solvers/smt2_incremental/smt_core_theory.cpp \
108+
solvers/smt2_incremental/smt_responses.cpp \
108109
solvers/smt2_incremental/smt_sorts.cpp \
109110
solvers/smt2_incremental/smt_terms.cpp \
110111
solvers/smt2_incremental/smt_to_smt2_string.cpp \

‎unit/count_tests.py

+15-6
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,22 @@ def __init__(self):
1414
self.separators = 0
1515

1616
def read_text(self, text):
17+
previous_character = None
18+
in_quotes = False
1719
for character in text:
18-
if character == '(' or character == '<':
19-
self.bracket_depth += 1
20-
elif character == ')' or character == '(':
21-
self.bracket_depth -= 1
22-
elif character == ',' and self.bracket_depth == 1:
23-
self.separators += 1
20+
if in_quotes:
21+
if character == '"' and previous_character != "\\":
22+
in_quotes = False
23+
else:
24+
if character == '"':
25+
in_quotes = True
26+
elif character == '(' or character == '<':
27+
self.bracket_depth += 1
28+
elif character == ')' or character == '(':
29+
self.bracket_depth -= 1
30+
elif character == ',' and self.bracket_depth == 1:
31+
self.separators += 1
32+
previous_character = character
2433

2534

2635
def tests_in_file(file_path):

0 commit comments

Comments
 (0)