1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Christopher L. Conway, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <sstream> |
17 |
|
|
18 |
|
#include "api/cpp/cvc5.h" |
19 |
|
#include "base/output.h" |
20 |
|
#include "expr/symbol_manager.h" |
21 |
|
#include "options/base_options.h" |
22 |
|
#include "options/language.h" |
23 |
|
#include "options/options.h" |
24 |
|
#include "parser/parser.h" |
25 |
|
#include "parser/parser_builder.h" |
26 |
|
#include "parser/smt2/smt2.h" |
27 |
|
#include "smt/command.h" |
28 |
|
#include "test.h" |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
|
32 |
|
using namespace parser; |
33 |
|
|
34 |
|
namespace test { |
35 |
|
|
36 |
|
class TestParserBlackParser : public TestInternal |
37 |
|
{ |
38 |
|
protected: |
39 |
8 |
TestParserBlackParser(const std::string& lang) : d_lang(lang) {} |
40 |
|
|
41 |
8 |
virtual ~TestParserBlackParser() {} |
42 |
|
|
43 |
8 |
void SetUp() override |
44 |
|
{ |
45 |
8 |
TestInternal::SetUp(); |
46 |
8 |
d_symman.reset(nullptr); |
47 |
8 |
d_solver.reset(new cvc5::api::Solver()); |
48 |
8 |
d_solver->setOption("parse-only", "true"); |
49 |
8 |
} |
50 |
|
|
51 |
8 |
void TearDown() override |
52 |
|
{ |
53 |
8 |
d_symman.reset(nullptr); |
54 |
8 |
d_solver.reset(nullptr); |
55 |
8 |
} |
56 |
|
|
57 |
|
/* Set up declaration context for expr inputs */ |
58 |
66 |
void setupContext(Parser& parser) |
59 |
|
{ |
60 |
|
/* a, b, c: BOOLEAN */ |
61 |
66 |
parser.bindVar("a", d_solver.get()->getBooleanSort()); |
62 |
66 |
parser.bindVar("b", d_solver.get()->getBooleanSort()); |
63 |
66 |
parser.bindVar("c", d_solver.get()->getBooleanSort()); |
64 |
|
/* t, u, v: TYPE */ |
65 |
132 |
api::Sort t = parser.mkSort("t"); |
66 |
132 |
api::Sort u = parser.mkSort("u"); |
67 |
132 |
api::Sort v = parser.mkSort("v"); |
68 |
|
/* f : t->u; g: u->v; h: v->t; */ |
69 |
66 |
parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u)); |
70 |
66 |
parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v)); |
71 |
66 |
parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t)); |
72 |
|
/* x:t; y:u; z:v; */ |
73 |
66 |
parser.bindVar("x", t); |
74 |
66 |
parser.bindVar("y", u); |
75 |
66 |
parser.bindVar("z", v); |
76 |
66 |
} |
77 |
|
|
78 |
26 |
void tryGoodInput(const std::string goodInput) |
79 |
|
{ |
80 |
26 |
d_symman.reset(new SymbolManager(d_solver.get())); |
81 |
|
std::unique_ptr<Parser> parser( |
82 |
52 |
ParserBuilder(d_solver.get(), d_symman.get(), true) |
83 |
26 |
.withInputLanguage(d_lang) |
84 |
52 |
.build()); |
85 |
26 |
parser->setInput(Input::newStringInput(d_lang, goodInput, "test")); |
86 |
26 |
ASSERT_FALSE(parser->done()); |
87 |
|
Command* cmd; |
88 |
134 |
while ((cmd = parser->nextCommand()) != NULL) |
89 |
|
{ |
90 |
54 |
Debug("parser") << "Parsed command: " << (*cmd) << std::endl; |
91 |
54 |
delete cmd; |
92 |
|
} |
93 |
|
|
94 |
26 |
ASSERT_TRUE(parser->done()); |
95 |
|
} |
96 |
|
|
97 |
16 |
void tryBadInput(const std::string badInput, bool strictMode = false) |
98 |
|
{ |
99 |
16 |
d_symman.reset(new SymbolManager(d_solver.get())); |
100 |
|
std::unique_ptr<Parser> parser( |
101 |
32 |
ParserBuilder(d_solver.get(), d_symman.get(), true) |
102 |
16 |
.withInputLanguage(d_lang) |
103 |
16 |
.withStrictMode(strictMode) |
104 |
32 |
.build()); |
105 |
16 |
parser->setInput(Input::newStringInput(d_lang, badInput, "test")); |
106 |
16 |
ASSERT_THROW( |
107 |
|
{ |
108 |
|
Command* cmd; |
109 |
|
while ((cmd = parser->nextCommand()) != NULL) |
110 |
|
{ |
111 |
|
Debug("parser") << "Parsed command: " << (*cmd) << std::endl; |
112 |
|
delete cmd; |
113 |
|
} |
114 |
|
std::cout << "\nBad input succeeded:\n" << badInput << std::endl; |
115 |
|
}, |
116 |
16 |
ParserException); |
117 |
|
} |
118 |
|
|
119 |
24 |
void tryGoodExpr(const std::string goodExpr) |
120 |
|
{ |
121 |
24 |
d_symman.reset(new SymbolManager(d_solver.get())); |
122 |
|
std::unique_ptr<Parser> parser( |
123 |
48 |
ParserBuilder(d_solver.get(), d_symman.get(), true) |
124 |
24 |
.withInputLanguage(d_lang) |
125 |
48 |
.build()); |
126 |
24 |
parser->setInput(Input::newStringInput(d_lang, goodExpr, "test")); |
127 |
24 |
if (d_lang == "LANG_SMTLIB_V2_6") |
128 |
|
{ |
129 |
|
/* Use QF_LIA to make multiplication ("*") available */ |
130 |
|
std::unique_ptr<Command> cmd( |
131 |
24 |
static_cast<Smt2*>(parser.get())->setLogic("QF_LIA")); |
132 |
|
} |
133 |
|
|
134 |
24 |
ASSERT_FALSE(parser->done()); |
135 |
24 |
setupContext(*parser); |
136 |
24 |
ASSERT_FALSE(parser->done()); |
137 |
48 |
api::Term e = parser->nextExpression(); |
138 |
24 |
ASSERT_FALSE(e.isNull()); |
139 |
24 |
e = parser->nextExpression(); |
140 |
24 |
ASSERT_TRUE(parser->done()); |
141 |
24 |
ASSERT_TRUE(e.isNull()); |
142 |
|
} |
143 |
|
|
144 |
|
/** |
145 |
|
* NOTE: The check implemented here may fail if a bad expression |
146 |
|
* expression string has a prefix that is parseable as a good |
147 |
|
* expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will |
148 |
|
* actually return the bit-vector 10 and ignore the tail of the |
149 |
|
* input. It's more trouble than it's worth to check that the whole |
150 |
|
* input was consumed here, so just be careful to avoid valid |
151 |
|
* prefixes in tests. |
152 |
|
*/ |
153 |
42 |
void tryBadExpr(const std::string badExpr, bool strictMode = false) |
154 |
|
{ |
155 |
42 |
d_symman.reset(new SymbolManager(d_solver.get())); |
156 |
|
std::unique_ptr<Parser> parser( |
157 |
84 |
ParserBuilder(d_solver.get(), d_symman.get(), true) |
158 |
42 |
.withInputLanguage(d_lang) |
159 |
42 |
.withStrictMode(strictMode) |
160 |
84 |
.build()); |
161 |
42 |
parser->setInput(Input::newStringInput(d_lang, badExpr, "test")); |
162 |
42 |
setupContext(*parser); |
163 |
42 |
ASSERT_FALSE(parser->done()); |
164 |
42 |
ASSERT_THROW(api::Term e = parser->nextExpression(); |
165 |
|
std::cout << std::endl |
166 |
|
<< "Bad expr succeeded." << std::endl |
167 |
|
<< "Input: <<" << badExpr << ">>" << std::endl |
168 |
|
<< "Output: <<" << e << ">>" << std::endl; |
169 |
42 |
, ParserException); |
170 |
|
} |
171 |
|
|
172 |
|
std::string d_lang; |
173 |
|
std::unique_ptr<cvc5::api::Solver> d_solver; |
174 |
|
std::unique_ptr<SymbolManager> d_symman; |
175 |
|
}; |
176 |
|
|
177 |
|
/* -------------------------------------------------------------------------- */ |
178 |
|
|
179 |
8 |
class TestParserBlackSmt2Parser : public TestParserBlackParser |
180 |
|
{ |
181 |
|
protected: |
182 |
8 |
TestParserBlackSmt2Parser() : TestParserBlackParser("LANG_SMTLIB_V2_6") {} |
183 |
|
}; |
184 |
|
|
185 |
13 |
TEST_F(TestParserBlackSmt2Parser, good_inputs) |
186 |
|
{ |
187 |
2 |
tryGoodInput(""); // empty string is OK |
188 |
2 |
tryGoodInput("(set-logic QF_UF)"); |
189 |
2 |
tryGoodInput("(set-info :notes |This is a note, take note!|)"); |
190 |
2 |
tryGoodInput("(set-logic QF_UF) (assert true)"); |
191 |
2 |
tryGoodInput("(check-sat)"); |
192 |
2 |
tryGoodInput("(exit)"); |
193 |
2 |
tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)"); |
194 |
2 |
tryGoodInput( |
195 |
|
"(set-logic QF_UF) (declare-fun a () Bool) " |
196 |
|
"(declare-fun b () Bool)"); |
197 |
2 |
tryGoodInput( |
198 |
|
"(set-logic QF_UF) (declare-fun a () Bool) " |
199 |
|
"(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))"); |
200 |
2 |
tryGoodInput( |
201 |
|
"(set-logic QF_UF) (declare-sort a 0) " |
202 |
|
"(declare-fun f (a) a) (declare-fun x () a) " |
203 |
|
"(assert (= (f x) x))"); |
204 |
2 |
tryGoodInput( |
205 |
|
"(set-logic QF_UF) (declare-sort a 0) " |
206 |
|
"(declare-fun x () a) (declare-fun y () a) " |
207 |
|
"(assert (= (ite true x y) x))"); |
208 |
2 |
tryGoodInput(";; nothing but a comment"); |
209 |
2 |
tryGoodInput("; a comment\n(check-sat ; goodbye\n)"); |
210 |
2 |
} |
211 |
|
|
212 |
13 |
TEST_F(TestParserBlackSmt2Parser, bad_inputs) |
213 |
|
{ |
214 |
|
// competition builds don't do any checking |
215 |
|
#ifndef CVC5_COMPETITION_MODE |
216 |
|
// no arguments |
217 |
2 |
tryBadInput("(assert)"); |
218 |
|
// illegal character in symbol |
219 |
2 |
tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); |
220 |
|
// check-sat should not have an argument |
221 |
2 |
tryBadInput("(set-logic QF_UF) (check-sat true)", true); |
222 |
|
// no argument |
223 |
2 |
tryBadInput("(declare-sort a)"); |
224 |
|
// double declaration |
225 |
2 |
tryBadInput("(declare-sort a 0) (declare-sort a 0)"); |
226 |
|
// should be "(declare-fun p () Bool)" |
227 |
2 |
tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); |
228 |
|
// strict mode |
229 |
|
// no set-logic, core theory symbol "true" undefined |
230 |
2 |
tryBadInput("(assert true)", true); |
231 |
|
// core theory symbol "Bool" undefined |
232 |
2 |
tryBadInput("(declare-fun p Bool)", true); |
233 |
|
#endif |
234 |
2 |
} |
235 |
|
|
236 |
13 |
TEST_F(TestParserBlackSmt2Parser, good_exprs) |
237 |
|
{ |
238 |
2 |
tryGoodExpr("(and a b)"); |
239 |
2 |
tryGoodExpr("(or (and a b) c)"); |
240 |
2 |
tryGoodExpr("(=> (and (=> a b) a) b)"); |
241 |
2 |
tryGoodExpr("(and (= a b) (not a))"); |
242 |
2 |
tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))"); |
243 |
2 |
tryGoodExpr("(ite a (f x) y)"); |
244 |
2 |
tryGoodExpr("1"); |
245 |
2 |
tryGoodExpr("0"); |
246 |
2 |
tryGoodExpr("1.5"); |
247 |
2 |
tryGoodExpr("#xfab09c7"); |
248 |
2 |
tryGoodExpr("#b0001011"); |
249 |
2 |
tryGoodExpr("(* 5 1)"); |
250 |
2 |
} |
251 |
|
|
252 |
13 |
TEST_F(TestParserBlackSmt2Parser, bad_exprs) |
253 |
|
{ |
254 |
|
// competition builds don't do any checking |
255 |
|
#ifndef CVC5_COMPETITION_MODE |
256 |
2 |
tryBadExpr("(and)"); // wrong arity |
257 |
2 |
tryBadExpr("(and a b"); // no closing paren |
258 |
2 |
tryBadExpr("(a and b)"); // infix |
259 |
2 |
tryBadExpr("(implies a b)"); // no implies in v2 |
260 |
2 |
tryBadExpr("(iff a b)"); // no iff in v2 |
261 |
2 |
tryBadExpr("(OR (AND a b) c)"); // wrong case |
262 |
2 |
tryBadExpr("(a IMPLIES b)"); // infix AND wrong case |
263 |
2 |
tryBadExpr("(not a b)"); // wrong arity |
264 |
2 |
tryBadExpr("not a"); // needs parens |
265 |
2 |
tryBadExpr("(ite a x)"); // wrong arity |
266 |
2 |
tryBadExpr("(if_then_else a (f x) y)"); // no if_then_else in v2 |
267 |
2 |
tryBadExpr("(a b)"); // using non-function as function |
268 |
2 |
tryBadExpr(".5"); // rational constants must have integer prefix |
269 |
2 |
tryBadExpr("1."); // rational constants must have fractional suffix |
270 |
2 |
tryBadExpr("#x"); // hex constants must have at least one digit |
271 |
2 |
tryBadExpr("#b"); // ditto binary constants |
272 |
2 |
tryBadExpr("#xg0f"); |
273 |
2 |
tryBadExpr("#b9"); |
274 |
|
// Bad strict exprs |
275 |
2 |
tryBadExpr("(and a)", true); // no unary and's |
276 |
2 |
tryBadExpr("(or a)", true); // no unary or's |
277 |
2 |
tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant |
278 |
|
#endif |
279 |
2 |
} |
280 |
|
} // namespace test |
281 |
15 |
} // namespace cvc5 |