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