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