1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
|
/********************* */
/*! \file parser_black.h
** \verbatim
** Top contributors (to current version):
** Christopher L. Conway, Morgan Deters, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Black box testing of CVC4::parser::Parser, including CVC, SMT and
** SMT v2 inputs.
**
** Black box testing of CVC4::parser::Parser, including CVC, SMT, and
** SMT v2 inputs.
**/
#include <cxxtest/TestSuite.h>
#include <sstream>
#include "api/cvc4cpp.h"
#include "base/output.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/smt2/smt2.h"
#include "smt/command.h"
using namespace CVC4;
using namespace CVC4::parser;
using namespace CVC4::language::input;
using namespace std;
class ParserBlack
{
protected:
Options d_options;
/* Set up declaration context for expr inputs */
virtual void setupContext(Parser& parser) {
/* a, b, c: BOOLEAN */
parser.mkVar("a", d_solver->getExprManager()->booleanType());
parser.mkVar("b", d_solver->getExprManager()->booleanType());
parser.mkVar("c", d_solver->getExprManager()->booleanType());
/* t, u, v: TYPE */
Type t = parser.mkSort("t");
Type u = parser.mkSort("u");
Type v = parser.mkSort("v");
/* f : t->u; g: u->v; h: v->t; */
parser.mkVar("f", d_solver->getExprManager()->mkFunctionType(t, u));
parser.mkVar("g", d_solver->getExprManager()->mkFunctionType(u, v));
parser.mkVar("h", d_solver->getExprManager()->mkFunctionType(v, t));
/* x:t; y:u; z:v; */
parser.mkVar("x",t);
parser.mkVar("y",u);
parser.mkVar("z",v);
}
void tryGoodInput(const string goodInput)
{
try
{
// Debug.on("parser");
// Debug.on("parser-extra");
// cerr << "Testing good input: <<" << goodInput << ">>" << endl;
// istringstream stream(goodInputs[i]);
Parser* parser = ParserBuilder(d_solver.get(), "test")
.withStringInput(goodInput)
.withOptions(d_options)
.withInputLanguage(d_lang)
.build();
TS_ASSERT(!parser->done());
Command* cmd;
while ((cmd = parser->nextCommand()) != NULL)
{
Debug("parser") << "Parsed command: " << (*cmd) << endl;
delete cmd;
}
TS_ASSERT(parser->done());
delete parser;
// Debug.off("parser");
// Debug.off("parser-extra");
}
catch (Exception& e)
{
cout << "\nGood input failed:\n" << goodInput << endl << e << endl;
// Debug.off("parser");
throw;
}
}
void tryBadInput(const string badInput, bool strictMode = false)
{
// cerr << "Testing bad input: '" << badInput << "'\n";
// Debug.on("parser");
Parser* parser = ParserBuilder(d_solver.get(), "test")
.withStringInput(badInput)
.withOptions(d_options)
.withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build();
TS_ASSERT_THROWS(
{
Command* cmd;
while ((cmd = parser->nextCommand()) != NULL)
{
Debug("parser") << "Parsed command: " << (*cmd) << endl;
delete cmd;
}
cout << "\nBad input succeeded:\n" << badInput << endl;
},
const ParserException&);
// Debug.off("parser");
delete parser;
}
void tryGoodExpr(const string goodExpr)
{
// Debug.on("parser");
// Debug.on("parser-extra");
try
{
// cerr << "Testing good expr: '" << goodExpr << "'\n";
// Debug.on("parser");
// istringstream stream(context + goodBooleanExprs[i]);
Parser* parser = ParserBuilder(d_solver.get(), "test")
.withStringInput(goodExpr)
.withOptions(d_options)
.withInputLanguage(d_lang)
.build();
TS_ASSERT(!parser->done());
setupContext(*parser);
TS_ASSERT(!parser->done());
Expr e = parser->nextExpression();
TS_ASSERT(!e.isNull());
e = parser->nextExpression();
TS_ASSERT(parser->done());
TS_ASSERT(e.isNull());
delete parser;
}
catch (Exception& e)
{
cout << endl
<< "Good expr failed." << endl
<< "Input: <<" << goodExpr << ">>" << endl
<< "Output: <<" << e << ">>" << endl;
throw;
}
}
/* NOTE: The check implemented here may fail if a bad expression
* expression string has a prefix that is parseable as a good
* expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will
* actually return the bit-vector 10 and ignore the tail of the
* input. It's more trouble than it's worth to check that the whole
* input was consumed here, so just be careful to avoid valid
* prefixes in tests.
*/
void tryBadExpr(const string badExpr, bool strictMode = false)
{
// Debug.on("parser");
// Debug.on("parser-extra");
// cout << "Testing bad expr: '" << badExpr << "'\n";
Parser* parser = ParserBuilder(d_solver.get(), "test")
.withStringInput(badExpr)
.withOptions(d_options)
.withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build();
setupContext(*parser);
TS_ASSERT(!parser->done());
TS_ASSERT_THROWS(Expr e = parser->nextExpression();
cout << endl
<< "Bad expr succeeded." << endl
<< "Input: <<" << badExpr << ">>" << endl
<< "Output: <<" << e << ">>" << endl;
, const ParserException&);
delete parser;
// Debug.off("parser");
}
ParserBlack(InputLanguage lang) :
d_lang(lang) {
}
virtual ~ParserBlack() {}
void setUp()
{
d_options.set(options::parseOnly, true);
d_solver.reset(new api::Solver(&d_options));
}
void tearDown() {
}
private:
InputLanguage d_lang;
std::unique_ptr<api::Solver> d_solver;
}; /* class ParserBlack */
class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
public:
Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
void setUp() override { super::setUp(); }
void tearDown() override { super::tearDown(); }
void testGoodCvc4Inputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput(";"); // no command is OK
tryGoodInput("ASSERT TRUE;");
tryGoodInput("QUERY TRUE;");
tryGoodInput("CHECKSAT FALSE;");
tryGoodInput("a, b : BOOLEAN;");
tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];");
tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;");
tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;");
tryGoodInput("%% nothing but a comment");
tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible
tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible
tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct
tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a'
//tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges
tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];");
tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;");
//tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
}
void testBadCvc4Inputs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadInput("ASSERT;"); // no args
tryBadInput("QUERY");
tryBadInput("CHECKSAT");
tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type
tryBadInput("0x : INT;"); // 0x isn't an identifier
tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl
tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal
tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function
tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible
tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared
tryBadInput("a : INT; a: INT = 5;"); // can't define after decl
tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type
tryBadInput("a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a'
//tryBadInput("a : [1..-1];"); // bad subrange
//tryBadInput("a : [0. .0];"); // bad subrange
//tryBadInput("a : [..0];"); // bad subrange
//tryBadInput("a : [0.0];"); // bad subrange
tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;");
tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;");
tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
#endif /* ! CVC4_COMPETITION_MODE */
}
void testGoodCvc4Exprs() {
tryGoodExpr("a AND b");
tryGoodExpr("a AND b OR c");
tryGoodExpr("(a => b) AND a => b");
tryGoodExpr("(a <=> b) AND (NOT a)");
tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))");
}
void testBadCvc4Exprs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadInput("a AND"); // wrong arity
tryBadInput("AND(a,b)"); // not infix
tryBadInput("(OR (AND a b) c)"); // not infix
tryBadInput("a IMPLIES b"); // should be =>
tryBadInput("a NOT b"); // wrong arity, not infix
tryBadInput("a and b"); // wrong case
#endif /* ! CVC4_COMPETITION_MODE */
}
};/* class Cvc4ParserTest */
class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
public:
Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { }
void setUp() override { super::setUp(); }
void tearDown() override { super::tearDown(); }
void testGoodSmt1Inputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("(benchmark foo :assumption true)");
tryGoodInput("(benchmark bar :formula true)");
tryGoodInput("(benchmark qux :formula false)");
tryGoodInput("(benchmark baz :extrapreds ( (a) (b) ) )");
tryGoodInput("(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))");
tryGoodInput("(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))");
tryGoodInput("(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))");
tryGoodInput(";; nothing but a comment");
tryGoodInput("; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)");
}
void testBadSmt1Inputs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadInput("(benchmark foo)"); // empty benchmark is not OK
tryBadInput("(benchmark bar :assumption)"); // no args
tryBadInput("(benchmark bar :formula)");
tryBadInput("(benchmark baz :extrapreds ( (a) (a) ) )"); // double decl
tryBadInput("(benchmark zub :extrasorts (a) :extrapreds (p a))"); // (p a) needs parens
#endif /* ! CVC4_COMPETITION_MODE */
}
void testGoodSmt1Exprs() {
tryGoodExpr("(and a b)");
tryGoodExpr("(or (and a b) c)");
tryGoodExpr("(implies (and (implies a b) a) b)");
tryGoodExpr("(and (iff a b) (not a))");
tryGoodExpr("(iff (xor a b) (and (or a b) (not (and a b))))");
tryGoodExpr("(ite a (f x) y)");
tryGoodExpr("(if_then_else a (f x) y)");
tryGoodExpr("1");
tryGoodExpr("0");
tryGoodExpr("1.5");
}
void testBadSmt1Exprs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadExpr("(and)"); // wrong arity
tryBadExpr("(and a b"); // no closing paren
tryBadExpr("(a and b)"); // infix
tryBadExpr("(OR (AND a b) c)"); // wrong case
tryBadExpr("(a IMPLIES b)"); // infix AND wrong case
tryBadExpr("(not a b)"); // wrong arity
tryBadExpr("not a"); // needs parens
tryBadExpr("(ite a x)"); // wrong arity
tryBadExpr("(a b)"); // using non-function as function
tryBadExpr(".5"); // rational constants must have integer prefix
tryBadExpr("1."); // rational constants must have fractional suffix
#endif /* ! CVC4_COMPETITION_MODE */
}
};/* class Smt1ParserTest */
class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
public:
Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
void setUp() override { super::setUp(); }
void tearDown() override { super::tearDown(); }
void setupContext(Parser& parser) override
{
if(dynamic_cast<Smt2*>(&parser) != NULL){
dynamic_cast<Smt2*>(&parser)->addTheory(Smt2::THEORY_CORE);
}
super::setupContext(parser);
}
void testGoodSmt2Inputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("(set-logic QF_UF)");
tryGoodInput("(set-info :notes |This is a note, take note!|)");
tryGoodInput("(set-logic QF_UF) (assert true)");
tryGoodInput("(check-sat)");
tryGoodInput("(exit)");
tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)");
tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) "
"(declare-fun b () Bool)");
tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) "
"(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))");
tryGoodInput("(set-logic QF_UF) (declare-sort a 0) "
"(declare-fun f (a) a) (declare-fun x () a) "
"(assert (= (f x) x))");
tryGoodInput("(set-logic QF_UF) (declare-sort a 0) "
"(declare-fun x () a) (declare-fun y () a) "
"(assert (= (ite true x y) x))");
tryGoodInput(";; nothing but a comment");
tryGoodInput("; a comment\n(check-sat ; goodbye\n)");
}
void testBadSmt2Inputs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadInput("(assert)"); // no args
tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
tryBadInput("(set-logic QF_UF) (check-sat true)", true); // check-sat shouldn't have an arg
tryBadInput("(declare-sort a)"); // no arg
tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl
tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool"
// strict mode
tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined
tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined
#endif /* ! CVC4_COMPETITION_MODE */
}
void testGoodSmt2Exprs() {
tryGoodExpr("(and a b)");
tryGoodExpr("(or (and a b) c)");
tryGoodExpr("(=> (and (=> a b) a) b)");
tryGoodExpr("(and (= a b) (not a))");
tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))");
tryGoodExpr("(ite a (f x) y)");
tryGoodExpr("1");
tryGoodExpr("0");
tryGoodExpr("1.5");
tryGoodExpr("#xfab09c7");
tryGoodExpr("#b0001011");
tryGoodExpr("(* 5 01)"); // '01' is OK in non-strict mode
}
void testBadSmt2Exprs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadExpr("(and)"); // wrong arity
tryBadExpr("(and a b"); // no closing paren
tryBadExpr("(a and b)"); // infix
tryBadExpr("(implies a b)"); // no implies in v2
tryBadExpr("(iff a b)"); // no iff in v2
tryBadExpr("(OR (AND a b) c)"); // wrong case
tryBadExpr("(a IMPLIES b)"); // infix AND wrong case
tryBadExpr("(not a b)"); // wrong arity
tryBadExpr("not a"); // needs parens
tryBadExpr("(ite a x)"); // wrong arity
tryBadExpr("(if_then_else a (f x) y)"); // no if_then_else in v2
tryBadExpr("(a b)"); // using non-function as function
tryBadExpr(".5"); // rational constants must have integer prefix
tryBadExpr("1."); // rational constants must have fractional suffix
tryBadExpr("#x"); // hex constants must have at least one digit
tryBadExpr("#b"); // ditto binary constants
tryBadExpr("#xg0f");
tryBadExpr("#b9");
// Bad strict exprs
tryBadExpr("(and a)", true); // no unary and's
tryBadExpr("(or a)", true); // no unary or's
tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant
#endif /* ! CVC4_COMPETITION_MODE */
}
};/* class Smt2ParserTest */
|