Skip to content

Commit 9409d99

Browse files
thomasspriggsthomasspriggs
committed
Add smt commands
1 parent af27fcc commit 9409d99

File tree

5 files changed

+294
-0
lines changed

5 files changed

+294
-0
lines changed

‎src/solvers/smt2_incremental/smt_commands.cpp

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <solvers/smt2_incremental/smt_commands.h>
4+
5+
#include <util/range.h>
6+
7+
// Define the irep_idts for commands.
8+
#define COMMAND_ID(the_id) \
9+
const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
10+
#include <solvers/smt2_incremental/smt_commands.def>
11+
#undef COMMAND_ID
12+
13+
bool smt_commandt::operator==(const smt_commandt &other) const
14+
{
15+
return irept::operator==(other);
16+
}
17+
18+
bool smt_commandt::operator!=(const smt_commandt &other) const
19+
{
20+
return !(*this == other);
21+
}
22+
23+
smt_assert_commandt::smt_assert_commandt(smt_termt condition)
24+
: smt_commandt{ID_smt_assert_command}
25+
{
26+
set(ID_cond, upcast(std::move(condition)));
27+
}
28+
29+
const smt_termt &smt_assert_commandt::condition() const
30+
{
31+
return downcast(find(ID_cond));
32+
}
33+
34+
smt_check_sat_commandt::smt_check_sat_commandt()
35+
: smt_commandt{ID_smt_check_sat_command}
36+
{
37+
}
38+
39+
smt_declare_function_commandt::smt_declare_function_commandt(
40+
irep_idt identifier,
41+
smt_sortt return_sort,
42+
std::vector<smt_sortt> parameter_sorts)
43+
: smt_commandt{ID_smt_declare_function_command}
44+
{
45+
set(ID_identifier, identifier);
46+
set(ID_type, upcast(std::move(return_sort)));
47+
std::transform(
48+
std::make_move_iterator(parameter_sorts.begin()),
49+
std::make_move_iterator(parameter_sorts.end()),
50+
std::back_inserter(get_sub()),
51+
[](smt_sortt &&parameter_sort) {
52+
return upcast(std::move(parameter_sort));
53+
});
54+
}
55+
56+
irep_idt smt_declare_function_commandt::identifier() const
57+
{
58+
return get(ID_identifier);
59+
}
60+
61+
const smt_sortt &smt_declare_function_commandt::return_sort() const
62+
{
63+
return downcast(find(ID_type));
64+
}
65+
66+
std::vector<std::reference_wrapper<const smt_sortt>>
67+
smt_declare_function_commandt::parameter_sorts() const
68+
{
69+
return make_range(get_sub()).map([](const irept &parameter_sort) {
70+
return std::cref(downcast(parameter_sort));
71+
});
72+
}
73+
74+
smt_exit_commandt::smt_exit_commandt() : smt_commandt{ID_smt_exit_command}
75+
{
76+
}
77+
78+
smt_define_function_commandt::smt_define_function_commandt(
79+
irep_idt identifier,
80+
std::vector<smt_identifier_termt> parameters,
81+
smt_termt definition)
82+
: smt_commandt{ID_smt_define_function_command}
83+
{
84+
set(ID_identifier, identifier);
85+
std::transform(
86+
std::make_move_iterator(parameters.begin()),
87+
std::make_move_iterator(parameters.end()),
88+
std::back_inserter(get_sub()),
89+
[](smt_identifier_termt &&parameter) {
90+
return upcast(std::move(parameter));
91+
});
92+
set(ID_code, upcast(std::move(definition)));
93+
}
94+
95+
const irep_idt &smt_define_function_commandt::identifier() const
96+
{
97+
return get(ID_identifier);
98+
}
99+
100+
std::vector<std::reference_wrapper<const smt_identifier_termt>>
101+
smt_define_function_commandt::parameters() const
102+
{
103+
return make_range(get_sub()).map([](const irept &parameter) {
104+
return std::cref(
105+
static_cast<const smt_identifier_termt &>(downcast((parameter))));
106+
});
107+
}
108+
109+
const smt_termt &smt_define_function_commandt::definition() const
110+
{
111+
return downcast(find(ID_code));
112+
}
113+
114+
smt_get_value_commandt::smt_get_value_commandt(smt_termt descriptor)
115+
: smt_commandt{ID_smt_get_value_command}
116+
{
117+
set(ID_value, upcast(std::move(descriptor)));
118+
}
119+
120+
const smt_termt &smt_get_value_commandt::descriptor() const
121+
{
122+
return downcast(find(ID_value));
123+
}

‎src/solvers/smt2_incremental/smt_commands.def

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
COMMAND_ID(assert)
2+
COMMAND_ID(check_sat)
3+
COMMAND_ID(declare_function)
4+
COMMAND_ID(define_function)
5+
COMMAND_ID(exit)
6+
COMMAND_ID(get_value)
7+
COMMAND_ID(set_logic)
8+
COMMAND_ID(set_option)

‎src/solvers/smt2_incremental/smt_commands.h

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
// Author: Diffblue Ltd.
2+
3+
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
4+
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
5+
6+
#include <solvers/smt2_incremental/smt_terms.h>
7+
#include <util/irep.h>
8+
9+
class smt_commandt : protected irept
10+
{
11+
public:
12+
// smt_commandt does not support the notion of an empty / null state. Use
13+
// optionalt<smt_commandt> instead if an empty command is required.
14+
smt_commandt() = delete;
15+
16+
using irept::pretty;
17+
18+
bool operator==(const smt_commandt &) const;
19+
bool operator!=(const smt_commandt &) const;
20+
21+
protected:
22+
using irept::irept;
23+
};
24+
25+
class smt_assert_commandt : public smt_commandt,
26+
private smt_termt::storert<smt_assert_commandt>
27+
{
28+
public:
29+
explicit smt_assert_commandt(smt_termt condition);
30+
const smt_termt &condition() const;
31+
};
32+
33+
class smt_check_sat_commandt : public smt_commandt
34+
{
35+
public:
36+
smt_check_sat_commandt();
37+
};
38+
39+
class smt_declare_function_commandt
40+
: public smt_commandt,
41+
private smt_sortt::storert<smt_declare_function_commandt>
42+
{
43+
public:
44+
smt_declare_function_commandt(
45+
irep_idt identifier,
46+
smt_sortt return_sort,
47+
std::vector<smt_sortt> parameter_sorts);
48+
irep_idt identifier() const;
49+
const smt_sortt &return_sort() const;
50+
std::vector<std::reference_wrapper<const smt_sortt>> parameter_sorts() const;
51+
};
52+
53+
class smt_define_function_commandt
54+
: public smt_commandt,
55+
private smt_termt::storert<smt_define_function_commandt>
56+
{
57+
public:
58+
smt_define_function_commandt(
59+
irep_idt identifier,
60+
std::vector<smt_identifier_termt> parameters,
61+
smt_termt definition);
62+
const irep_idt &identifier() const;
63+
std::vector<std::reference_wrapper<const smt_identifier_termt>>
64+
parameters() const;
65+
const smt_termt &definition() const;
66+
};
67+
68+
class smt_exit_commandt : public smt_commandt
69+
{
70+
public:
71+
smt_exit_commandt();
72+
};
73+
74+
class smt_get_value_commandt : public smt_commandt,
75+
protected smt_termt::storert<smt_assert_commandt>
76+
{
77+
public:
78+
explicit smt_get_value_commandt(smt_termt descriptor);
79+
const smt_termt &descriptor() const;
80+
};
81+
82+
class smt_set_logic_commandt : public smt_commandt
83+
{
84+
public:
85+
};
86+
87+
class smt_set_option_commandt : public smt_commandt
88+
{
89+
public:
90+
};
91+
92+
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,7 @@ SRC += analyses/ai/ai.cpp \
7676
solvers/sat/external_sat.cpp \
7777
solvers/sat/satcheck_cadical.cpp \
7878
solvers/sat/satcheck_minisat2.cpp \
79+
solvers/smt2_incremental/smt_commands.cpp \
7980
solvers/smt2_incremental/smt_sorts.cpp \
8081
solvers/smt2_incremental/smt_terms.cpp \
8182
solvers/smt2_incremental/smt_to_string.cpp \

‎unit/solvers/smt2_incremental/smt_commands.cpp

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <testing-utils/use_catch.h>
4+
5+
#include <solvers/smt2_incremental/smt_commands.h>
6+
7+
TEST_CASE("smt_commandt upcasts.", "[core][smt2_incremental]")
8+
{
9+
smt_commandt command{smt_exit_commandt{}};
10+
command = smt_exit_commandt{};
11+
}
12+
13+
TEST_CASE("Test smt_commandt.pretty is accessible.", "[core][smt2_incremental]")
14+
{
15+
const smt_commandt check_sat_command{smt_check_sat_commandt{}};
16+
REQUIRE(check_sat_command.pretty(0, 0) == "smt_check_sat_command");
17+
}
18+
19+
TEST_CASE("smt_assert_commandt condition getter", "[core][smt2_incremental]")
20+
{
21+
const smt_assert_commandt assert_command{smt_bool_literal_termt{true}};
22+
REQUIRE(assert_command.condition() == smt_bool_literal_termt{true});
23+
}
24+
25+
TEST_CASE("smt_declare_function_commandt getters", "[core][smt2_incremental]")
26+
{
27+
const smt_declare_function_commandt function_declaration{"+", smt_bit_vector_sortt{9},
28+
std::vector<smt_sortt>{smt_bit_vector_sortt{8}, smt_bit_vector_sortt{7}}};
29+
CHECK(function_declaration.identifier() == "+");
30+
CHECK(function_declaration.return_sort() == smt_bit_vector_sortt{9});
31+
CHECK(function_declaration.parameter_sorts()[0].get() == smt_bit_vector_sortt{8});
32+
CHECK(function_declaration.parameter_sorts()[1].get() == smt_bit_vector_sortt{7});
33+
}
34+
35+
TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]")
36+
{
37+
const smt_define_function_commandt function_definition
38+
{
39+
"not first",
40+
{smt_identifier_termt{"x", smt_bool_sortt{}},
41+
smt_identifier_termt{"y", smt_bool_sortt{}}},
42+
smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}}
43+
};
44+
CHECK(function_definition.identifier() == "not first");
45+
CHECK(function_definition.parameters()[0].get() ==
46+
smt_identifier_termt{"x", smt_bool_sortt{}});
47+
CHECK(function_definition.parameters()[1].get() ==
48+
smt_identifier_termt{"y", smt_bool_sortt{}});
49+
CHECK(function_definition.definition() ==
50+
smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}});
51+
}
52+
53+
TEST_CASE("smt_get_value_commandt getter", "[core][smt2_incremental]")
54+
{
55+
const smt_get_value_commandt get_value_command{smt_identifier_termt{"x", smt_bool_sortt{}}};
56+
REQUIRE(get_value_command.descriptor() == smt_identifier_termt{"x", smt_bool_sortt{}});
57+
}
58+
59+
TEST_CASE("smt_commandt equality", "[core][smt2_incremental]")
60+
{
61+
const smt_exit_commandt exit_command{};
62+
CHECK(exit_command == smt_exit_commandt{});
63+
const smt_check_sat_commandt check_sat_command{};
64+
CHECK(check_sat_command == smt_check_sat_commandt{});
65+
CHECK_FALSE(exit_command == check_sat_command);
66+
const smt_assert_commandt assert_true{smt_bool_literal_termt{true}};
67+
CHECK(assert_true == smt_assert_commandt{smt_bool_literal_termt{true}});
68+
const smt_assert_commandt assert_false{smt_bool_literal_termt{false}};
69+
CHECK_FALSE(assert_true == assert_false);
70+
}

0 commit comments

Comments
 (0)