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 |
|
using namespace language::input; |
34 |
|
|
35 |
|
namespace test { |
36 |
|
|
37 |
|
class TestParserBlackParser : public TestInternal |
38 |
|
{ |
39 |
|
protected: |
40 |
16 |
TestParserBlackParser(InputLanguage lang) : d_lang(lang) {} |
41 |
|
|
42 |
16 |
virtual ~TestParserBlackParser() {} |
43 |
|
|
44 |
16 |
void SetUp() override |
45 |
|
{ |
46 |
16 |
TestInternal::SetUp(); |
47 |
32 |
d_options.set(options::parseOnly, true); |
48 |
16 |
d_symman.reset(nullptr); |
49 |
16 |
d_solver.reset(new cvc5::api::Solver(&d_options)); |
50 |
16 |
} |
51 |
|
|
52 |
16 |
void TearDown() override |
53 |
|
{ |
54 |
16 |
d_symman.reset(nullptr); |
55 |
16 |
d_solver.reset(nullptr); |
56 |
16 |
} |
57 |
|
|
58 |
|
void setUp() |
59 |
|
{ |
60 |
|
/* ensure the old symbol manager is deleted */ |
61 |
|
d_symman.reset(nullptr); |
62 |
|
d_solver.reset(new api::Solver(&d_options)); |
63 |
|
} |
64 |
|
|
65 |
|
/* Set up declaration context for expr inputs */ |
66 |
76 |
void setupContext(Parser& parser) |
67 |
|
{ |
68 |
|
/* a, b, c: BOOLEAN */ |
69 |
76 |
parser.bindVar("a", d_solver.get()->getBooleanSort()); |
70 |
76 |
parser.bindVar("b", d_solver.get()->getBooleanSort()); |
71 |
76 |
parser.bindVar("c", d_solver.get()->getBooleanSort()); |
72 |
|
/* t, u, v: TYPE */ |
73 |
152 |
api::Sort t = parser.mkSort("t"); |
74 |
152 |
api::Sort u = parser.mkSort("u"); |
75 |
152 |
api::Sort v = parser.mkSort("v"); |
76 |
|
/* f : t->u; g: u->v; h: v->t; */ |
77 |
76 |
parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u)); |
78 |
76 |
parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v)); |
79 |
76 |
parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t)); |
80 |
|
/* x:t; y:u; z:v; */ |
81 |
76 |
parser.bindVar("x", t); |
82 |
76 |
parser.bindVar("y", u); |
83 |
76 |
parser.bindVar("z", v); |
84 |
76 |
} |
85 |
|
|
86 |
72 |
void tryGoodInput(const std::string goodInput) |
87 |
|
{ |
88 |
72 |
d_symman.reset(new SymbolManager(d_solver.get())); |
89 |
144 |
std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) |
90 |
72 |
.withOptions(d_options) |
91 |
72 |
.withInputLanguage(d_lang) |
92 |
144 |
.build()); |
93 |
72 |
parser->setInput(Input::newStringInput(d_lang, goodInput, "test")); |
94 |
72 |
ASSERT_FALSE(parser->done()); |
95 |
|
Command* cmd; |
96 |
356 |
while ((cmd = parser->nextCommand()) != NULL) |
97 |
|
{ |
98 |
142 |
Debug("parser") << "Parsed command: " << (*cmd) << std::endl; |
99 |
142 |
delete cmd; |
100 |
|
} |
101 |
|
|
102 |
72 |
ASSERT_TRUE(parser->done()); |
103 |
|
} |
104 |
|
|
105 |
60 |
void tryBadInput(const std::string badInput, bool strictMode = false) |
106 |
|
{ |
107 |
60 |
d_symman.reset(new SymbolManager(d_solver.get())); |
108 |
120 |
std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) |
109 |
60 |
.withOptions(d_options) |
110 |
60 |
.withInputLanguage(d_lang) |
111 |
60 |
.withStrictMode(strictMode) |
112 |
120 |
.build()); |
113 |
60 |
parser->setInput(Input::newStringInput(d_lang, badInput, "test")); |
114 |
60 |
ASSERT_THROW( |
115 |
|
{ |
116 |
|
Command* cmd; |
117 |
|
while ((cmd = parser->nextCommand()) != NULL) |
118 |
|
{ |
119 |
|
Debug("parser") << "Parsed command: " << (*cmd) << std::endl; |
120 |
|
delete cmd; |
121 |
|
} |
122 |
|
std::cout << "\nBad input succeeded:\n" << badInput << std::endl; |
123 |
|
}, |
124 |
60 |
ParserException); |
125 |
|
} |
126 |
|
|
127 |
34 |
void tryGoodExpr(const std::string goodExpr) |
128 |
|
{ |
129 |
34 |
d_symman.reset(new SymbolManager(d_solver.get())); |
130 |
68 |
std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) |
131 |
34 |
.withOptions(d_options) |
132 |
34 |
.withInputLanguage(d_lang) |
133 |
68 |
.build()); |
134 |
34 |
parser->setInput(Input::newStringInput(d_lang, goodExpr, "test")); |
135 |
34 |
if (d_lang == LANG_SMTLIB_V2) |
136 |
|
{ |
137 |
|
/* Use QF_LIA to make multiplication ("*") available */ |
138 |
|
std::unique_ptr<Command> cmd( |
139 |
24 |
static_cast<Smt2*>(parser.get())->setLogic("QF_LIA")); |
140 |
|
} |
141 |
|
|
142 |
34 |
ASSERT_FALSE(parser->done()); |
143 |
34 |
setupContext(*parser); |
144 |
34 |
ASSERT_FALSE(parser->done()); |
145 |
68 |
api::Term e = parser->nextExpression(); |
146 |
34 |
ASSERT_FALSE(e.isNull()); |
147 |
34 |
e = parser->nextExpression(); |
148 |
34 |
ASSERT_TRUE(parser->done()); |
149 |
34 |
ASSERT_TRUE(e.isNull()); |
150 |
|
} |
151 |
|
|
152 |
|
/** |
153 |
|
* NOTE: The check implemented here may fail if a bad expression |
154 |
|
* expression string has a prefix that is parseable as a good |
155 |
|
* expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will |
156 |
|
* actually return the bit-vector 10 and ignore the tail of the |
157 |
|
* input. It's more trouble than it's worth to check that the whole |
158 |
|
* input was consumed here, so just be careful to avoid valid |
159 |
|
* prefixes in tests. |
160 |
|
*/ |
161 |
42 |
void tryBadExpr(const std::string badExpr, bool strictMode = false) |
162 |
|
{ |
163 |
42 |
d_symman.reset(new SymbolManager(d_solver.get())); |
164 |
84 |
std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) |
165 |
42 |
.withOptions(d_options) |
166 |
42 |
.withInputLanguage(d_lang) |
167 |
42 |
.withStrictMode(strictMode) |
168 |
84 |
.build()); |
169 |
42 |
parser->setInput(Input::newStringInput(d_lang, badExpr, "test")); |
170 |
42 |
setupContext(*parser); |
171 |
42 |
ASSERT_FALSE(parser->done()); |
172 |
42 |
ASSERT_THROW(api::Term e = parser->nextExpression(); |
173 |
|
std::cout << std::endl |
174 |
|
<< "Bad expr succeeded." << std::endl |
175 |
|
<< "Input: <<" << badExpr << ">>" << std::endl |
176 |
|
<< "Output: <<" << e << ">>" << std::endl; |
177 |
42 |
, ParserException); |
178 |
|
} |
179 |
|
|
180 |
|
Options d_options; |
181 |
|
InputLanguage d_lang; |
182 |
|
std::unique_ptr<cvc5::api::Solver> d_solver; |
183 |
|
std::unique_ptr<SymbolManager> d_symman; |
184 |
|
}; |
185 |
|
|
186 |
|
/* -------------------------------------------------------------------------- */ |
187 |
|
|
188 |
8 |
class TestParserBlackCvCParser : public TestParserBlackParser |
189 |
|
{ |
190 |
|
protected: |
191 |
8 |
TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC) {} |
192 |
|
}; |
193 |
|
|
194 |
17 |
TEST_F(TestParserBlackCvCParser, good_inputs) |
195 |
|
{ |
196 |
2 |
tryGoodInput(""); // empty string is OK |
197 |
2 |
tryGoodInput(";"); // no command is OK |
198 |
2 |
tryGoodInput("ASSERT TRUE;"); |
199 |
2 |
tryGoodInput("QUERY TRUE;"); |
200 |
2 |
tryGoodInput("CHECKSAT FALSE;"); |
201 |
2 |
tryGoodInput("a, b : BOOLEAN;"); |
202 |
2 |
tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); |
203 |
2 |
tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;"); |
204 |
2 |
tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); |
205 |
2 |
tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];"); |
206 |
2 |
tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;"); |
207 |
2 |
tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); |
208 |
2 |
tryGoodInput( |
209 |
|
"T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); |
210 |
2 |
tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); |
211 |
2 |
tryGoodInput("%% nothing but a comment"); |
212 |
2 |
tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); |
213 |
2 |
tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible |
214 |
2 |
tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible |
215 |
2 |
tryGoodInput( |
216 |
|
"a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct |
217 |
2 |
tryGoodInput( |
218 |
|
"a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a' |
219 |
2 |
tryGoodInput( |
220 |
|
"DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null " |
221 |
|
"END;"); |
222 |
2 |
tryGoodInput( |
223 |
|
"DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil " |
224 |
|
"END;"); |
225 |
2 |
tryGoodInput( |
226 |
|
"DATATYPE trex = Foo | Bar END; DATATYPE tree = " |
227 |
|
"node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list " |
228 |
|
"OF tree,cdr:BITVECTOR(32)) END;"); |
229 |
2 |
} |
230 |
|
|
231 |
17 |
TEST_F(TestParserBlackCvCParser, bad_inputs) |
232 |
|
{ |
233 |
|
// competition builds don't do any checking |
234 |
|
#ifndef CVC5_COMPETITION_MODE |
235 |
2 |
tryBadInput("ASSERT;"); // no args |
236 |
2 |
tryBadInput("QUERY"); |
237 |
2 |
tryBadInput("CHECKSAT"); |
238 |
2 |
tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type |
239 |
2 |
tryBadInput("0x : INT;"); // 0x isn't an identifier |
240 |
2 |
tryBadInput( |
241 |
|
"a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl |
242 |
2 |
tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal |
243 |
2 |
tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function |
244 |
2 |
tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible |
245 |
2 |
tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared |
246 |
2 |
tryBadInput("a : INT; a: INT = 5;"); // can't define after decl |
247 |
2 |
tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type |
248 |
2 |
tryBadInput( |
249 |
|
"a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a' |
250 |
2 |
tryBadInput( |
251 |
|
"DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | " |
252 |
|
"cons(car:INT,cdr:list) END;"); |
253 |
2 |
tryBadInput( |
254 |
|
"DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil " |
255 |
|
"END;"); |
256 |
2 |
tryBadInput( |
257 |
|
"DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = " |
258 |
|
"cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); |
259 |
|
#endif |
260 |
2 |
} |
261 |
|
|
262 |
17 |
TEST_F(TestParserBlackCvCParser, good_exprs) |
263 |
|
{ |
264 |
2 |
tryGoodExpr("a AND b"); |
265 |
2 |
tryGoodExpr("a AND b OR c"); |
266 |
2 |
tryGoodExpr("(a => b) AND a => b"); |
267 |
2 |
tryGoodExpr("(a <=> b) AND (NOT a)"); |
268 |
2 |
tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))"); |
269 |
2 |
} |
270 |
|
|
271 |
17 |
TEST_F(TestParserBlackCvCParser, bad_exprs) |
272 |
|
{ |
273 |
|
// competition builds don't do any checking |
274 |
|
#ifndef CVC5_COMPETITION_MODE |
275 |
2 |
tryBadInput("a AND"); // wrong arity |
276 |
2 |
tryBadInput("AND(a,b)"); // not infix |
277 |
2 |
tryBadInput("(OR (AND a b) c)"); // not infix |
278 |
2 |
tryBadInput("a IMPLIES b"); // should be => |
279 |
2 |
tryBadInput("a NOT b"); // wrong arity, not infix |
280 |
2 |
tryBadInput("a and b"); // wrong case |
281 |
|
#endif |
282 |
2 |
} |
283 |
|
|
284 |
|
/* -------------------------------------------------------------------------- */ |
285 |
|
|
286 |
8 |
class TestParserBlackSmt2Parser : public TestParserBlackParser |
287 |
|
{ |
288 |
|
protected: |
289 |
8 |
TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {} |
290 |
|
}; |
291 |
|
|
292 |
17 |
TEST_F(TestParserBlackSmt2Parser, good_inputs) |
293 |
|
{ |
294 |
2 |
tryGoodInput(""); // empty string is OK |
295 |
2 |
tryGoodInput("(set-logic QF_UF)"); |
296 |
2 |
tryGoodInput("(set-info :notes |This is a note, take note!|)"); |
297 |
2 |
tryGoodInput("(set-logic QF_UF) (assert true)"); |
298 |
2 |
tryGoodInput("(check-sat)"); |
299 |
2 |
tryGoodInput("(exit)"); |
300 |
2 |
tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)"); |
301 |
2 |
tryGoodInput( |
302 |
|
"(set-logic QF_UF) (declare-fun a () Bool) " |
303 |
|
"(declare-fun b () Bool)"); |
304 |
2 |
tryGoodInput( |
305 |
|
"(set-logic QF_UF) (declare-fun a () Bool) " |
306 |
|
"(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))"); |
307 |
2 |
tryGoodInput( |
308 |
|
"(set-logic QF_UF) (declare-sort a 0) " |
309 |
|
"(declare-fun f (a) a) (declare-fun x () a) " |
310 |
|
"(assert (= (f x) x))"); |
311 |
2 |
tryGoodInput( |
312 |
|
"(set-logic QF_UF) (declare-sort a 0) " |
313 |
|
"(declare-fun x () a) (declare-fun y () a) " |
314 |
|
"(assert (= (ite true x y) x))"); |
315 |
2 |
tryGoodInput(";; nothing but a comment"); |
316 |
2 |
tryGoodInput("; a comment\n(check-sat ; goodbye\n)"); |
317 |
2 |
} |
318 |
|
|
319 |
17 |
TEST_F(TestParserBlackSmt2Parser, bad_inputs) |
320 |
|
{ |
321 |
|
// competition builds don't do any checking |
322 |
|
#ifndef CVC5_COMPETITION_MODE |
323 |
|
// no arguments |
324 |
2 |
tryBadInput("(assert)"); |
325 |
|
// illegal character in symbol |
326 |
2 |
tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); |
327 |
|
// check-sat should not have an argument |
328 |
2 |
tryBadInput("(set-logic QF_UF) (check-sat true)", true); |
329 |
|
// no argument |
330 |
2 |
tryBadInput("(declare-sort a)"); |
331 |
|
// double declaration |
332 |
2 |
tryBadInput("(declare-sort a 0) (declare-sort a 0)"); |
333 |
|
// should be "(declare-fun p () Bool)" |
334 |
2 |
tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); |
335 |
|
// strict mode |
336 |
|
// no set-logic, core theory symbol "true" undefined |
337 |
2 |
tryBadInput("(assert true)", true); |
338 |
|
// core theory symbol "Bool" undefined |
339 |
2 |
tryBadInput("(declare-fun p Bool)", true); |
340 |
|
#endif |
341 |
2 |
} |
342 |
|
|
343 |
17 |
TEST_F(TestParserBlackSmt2Parser, good_exprs) |
344 |
|
{ |
345 |
2 |
tryGoodExpr("(and a b)"); |
346 |
2 |
tryGoodExpr("(or (and a b) c)"); |
347 |
2 |
tryGoodExpr("(=> (and (=> a b) a) b)"); |
348 |
2 |
tryGoodExpr("(and (= a b) (not a))"); |
349 |
2 |
tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))"); |
350 |
2 |
tryGoodExpr("(ite a (f x) y)"); |
351 |
2 |
tryGoodExpr("1"); |
352 |
2 |
tryGoodExpr("0"); |
353 |
2 |
tryGoodExpr("1.5"); |
354 |
2 |
tryGoodExpr("#xfab09c7"); |
355 |
2 |
tryGoodExpr("#b0001011"); |
356 |
2 |
tryGoodExpr("(* 5 1)"); |
357 |
2 |
} |
358 |
|
|
359 |
17 |
TEST_F(TestParserBlackSmt2Parser, bad_exprs) |
360 |
|
{ |
361 |
|
// competition builds don't do any checking |
362 |
|
#ifndef CVC5_COMPETITION_MODE |
363 |
2 |
tryBadExpr("(and)"); // wrong arity |
364 |
2 |
tryBadExpr("(and a b"); // no closing paren |
365 |
2 |
tryBadExpr("(a and b)"); // infix |
366 |
2 |
tryBadExpr("(implies a b)"); // no implies in v2 |
367 |
2 |
tryBadExpr("(iff a b)"); // no iff in v2 |
368 |
2 |
tryBadExpr("(OR (AND a b) c)"); // wrong case |
369 |
2 |
tryBadExpr("(a IMPLIES b)"); // infix AND wrong case |
370 |
2 |
tryBadExpr("(not a b)"); // wrong arity |
371 |
2 |
tryBadExpr("not a"); // needs parens |
372 |
2 |
tryBadExpr("(ite a x)"); // wrong arity |
373 |
2 |
tryBadExpr("(if_then_else a (f x) y)"); // no if_then_else in v2 |
374 |
2 |
tryBadExpr("(a b)"); // using non-function as function |
375 |
2 |
tryBadExpr(".5"); // rational constants must have integer prefix |
376 |
2 |
tryBadExpr("1."); // rational constants must have fractional suffix |
377 |
2 |
tryBadExpr("#x"); // hex constants must have at least one digit |
378 |
2 |
tryBadExpr("#b"); // ditto binary constants |
379 |
2 |
tryBadExpr("#xg0f"); |
380 |
2 |
tryBadExpr("#b9"); |
381 |
|
// Bad strict exprs |
382 |
2 |
tryBadExpr("(and a)", true); // no unary and's |
383 |
2 |
tryBadExpr("(or a)", true); // no unary or's |
384 |
2 |
tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant |
385 |
|
#endif |
386 |
2 |
} |
387 |
|
} // namespace test |
388 |
43 |
} // namespace cvc5 |