Skip to content

Commit a1cf6f2

Browse files
Add a class for SMT2 commands
This reflects the structure of SMT2 commands, making commands constructed using this framework will be syntatically correct by construction.
1 parent 531c2af commit a1cf6f2

File tree

2 files changed

+199
-0
lines changed

2 files changed

+199
-0
lines changed

src/solvers/smt2/smt2_command.h

Lines changed: 198 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,198 @@
1+
/*******************************************************************\
2+
3+
Module: SMT2 solver
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// SMT2 commands
11+
12+
#ifndef CPROVER_SOLVERS_SMT2_SMT2_COMMAND_H
13+
#define CPROVER_SOLVERS_SMT2_SMT2_COMMAND_H
14+
15+
#include "smt2_ast.h"
16+
17+
class smt2_command_or_commentt
18+
{
19+
public:
20+
virtual void print(std::ostream &stream) const = 0;
21+
};
22+
23+
inline std::ostream &
24+
operator<<(std::ostream &stream, const smt2_command_or_commentt &command)
25+
{
26+
command.print(stream);
27+
return stream;
28+
}
29+
30+
class smt2_commandt : public smt2_command_or_commentt
31+
{
32+
public:
33+
void print(std::ostream &stream) const override;
34+
35+
static smt2_commandt set_logic(smt2_symbolt symbol)
36+
{
37+
return smt2_commandt{"set-logic", {std::move(symbol)}};
38+
}
39+
40+
static smt2_commandt declare_fun(
41+
smt2_symbolt symbol,
42+
smt2_listt<smt2_sortt> arguments,
43+
smt2_sortt result)
44+
{
45+
return smt2_commandt{
46+
"declare-fun",
47+
{std::move(symbol), std::move(arguments), std::move(result)}};
48+
}
49+
50+
static smt2_commandt define_fun(
51+
smt2_symbolt symbol,
52+
smt2_listt<smt2_pairt<smt2_symbolt, smt2_sortt>> arguments,
53+
smt2_sortt result_sort,
54+
smt2_astt result_expr)
55+
{
56+
return smt2_commandt{"define-fun",
57+
{std::move(symbol),
58+
std::move(arguments),
59+
std::move(result_sort),
60+
std::move(result_expr)}};
61+
}
62+
63+
static smt2_commandt declare_sort(smt2_symbolt symbol, smt2_constantt numeral)
64+
{
65+
return smt2_commandt{"declare-sort",
66+
{std::move(symbol), std::move(numeral)}};
67+
}
68+
69+
static smt2_commandt define_sort(
70+
smt2_symbolt symbol,
71+
smt2_listt<smt2_symbolt> arguments,
72+
smt2_astt expr)
73+
{
74+
return smt2_commandt{
75+
"define-sort",
76+
{std::move(symbol), std::move(arguments), std::move(expr)}};
77+
}
78+
79+
static smt2_commandt _assert(smt2_astt expr)
80+
{
81+
return smt2_commandt{"assert", {std::move(expr)}};
82+
}
83+
84+
static smt2_commandt get_assertions()
85+
{
86+
return smt2_commandt{"get-assertions", {}};
87+
}
88+
89+
static smt2_commandt check_sat()
90+
{
91+
return smt2_commandt{"check-sat", {}};
92+
}
93+
94+
static smt2_commandt get_proof()
95+
{
96+
return smt2_commandt{"get-proof", {}};
97+
}
98+
99+
static smt2_commandt get_unsat_core()
100+
{
101+
return smt2_commandt{"get-unsat-core", {}};
102+
}
103+
104+
static smt2_commandt get_value(smt2_listt<smt2_astt> terms)
105+
{
106+
return smt2_commandt{"get-value", {std::move(terms)}};
107+
}
108+
109+
static smt2_commandt get_assignment()
110+
{
111+
return smt2_commandt{"get-assignment", {}};
112+
}
113+
114+
static smt2_commandt push(smt2_constantt numeral)
115+
{
116+
return smt2_commandt{"push", {std::move(numeral)}};
117+
}
118+
119+
static smt2_commandt pop(smt2_constantt numeral)
120+
{
121+
return smt2_commandt{"pop", {std::move(numeral)}};
122+
}
123+
124+
static smt2_commandt get_option(smt2_symbolt keyword)
125+
{
126+
return smt2_commandt{"get-option", {std::move(keyword)}};
127+
}
128+
129+
static smt2_commandt set_option(smt2_symbolt keyword, smt2_astt value)
130+
{
131+
return smt2_commandt{"set-option", {std::move(keyword), std::move(value)}};
132+
}
133+
134+
static smt2_commandt get_info(smt2_symbolt keyword)
135+
{
136+
return smt2_commandt{"get-info", {std::move(keyword)}};
137+
}
138+
139+
static smt2_commandt set_info(smt2_symbolt keyword, smt2_astt value)
140+
{
141+
return smt2_commandt{"set-info", {std::move(keyword), std::move(value)}};
142+
}
143+
144+
static smt2_commandt exit()
145+
{
146+
return smt2_commandt{"exit", {}};
147+
}
148+
149+
static smt2_commandt declare_datatypes(
150+
smt2_listt<smt2_sort_declarationt> sort_decs,
151+
smt2_listt<smt2_datatype_declarationt> datatype_decs)
152+
{
153+
return smt2_commandt{"declare-datatypes",
154+
{std::move(sort_decs), std::move(datatype_decs)}};
155+
}
156+
157+
static smt2_commandt
158+
declare_datatypes(smt2_listt<smt2_datatype_declarationt> datatype_decs)
159+
{
160+
return declare_datatypes(
161+
smt2_listt<smt2_sort_declarationt>{{}}, std::move(datatype_decs));
162+
}
163+
164+
private:
165+
irep_idt name;
166+
std::vector<smt2_astt> arguments;
167+
168+
smt2_commandt(irep_idt name, std::vector<smt2_astt> arguments)
169+
: name(std::move(name)), arguments(std::move(arguments))
170+
{
171+
}
172+
};
173+
174+
void smt2_commandt::print(std::ostream &stream) const
175+
{
176+
stream << '(' << name;
177+
for(const auto &arg : arguments)
178+
stream << ' ' << arg;
179+
stream << ")\n";
180+
}
181+
182+
class smt2_commentt : public smt2_command_or_commentt
183+
{
184+
public:
185+
void print(std::ostream &stream) const override
186+
{
187+
stream << "; " << content << '\n';
188+
}
189+
190+
explicit smt2_commentt(std::string content) : content(std::move(content))
191+
{
192+
}
193+
194+
private:
195+
std::string content;
196+
};
197+
198+
#endif // CPROVER_SOLVERS_SMT2_SMT2_COMMAND_H

src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -723,6 +723,7 @@ IREP_ID_ONE(to_member)
723723
IREP_ID_ONE(pointer_to_member)
724724
IREP_ID_ONE(tuple)
725725
IREP_ID_ONE(function_body)
726+
IREP_ID_ONE(par)
726727

727728
// Projects depending on this code base that wish to extend the list of
728729
// available ids should provide a file local_irep_ids.def in their source tree

0 commit comments

Comments
 (0)