diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
commit | 57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a (patch) | |
tree | 1c1781cc83118e4bbd2ad6939b16734c30a69f1a /test/unit/parser | |
parent | 673d0e86b91094a58433c3ca71591fb0a0c60f84 (diff) |
* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
Diffstat (limited to 'test/unit/parser')
-rw-r--r-- | test/unit/parser/parser_black.h | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 632db2b91..53050eece 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -27,6 +27,7 @@ #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" #include "expr/command.h" +#include "util/options.h" #include "util/output.h" #include "util/language.h" @@ -40,6 +41,8 @@ class ParserBlack { ExprManager *d_exprManager; protected: + Options d_options; + /* Set up declaration context for expr inputs */ virtual void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ @@ -69,6 +72,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(goodInput) + .withOptions(d_options) .withInputLanguage(d_lang) .build(); TS_ASSERT( !parser->done() ); @@ -96,6 +100,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(badInput) + .withOptions(d_options) .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); @@ -118,6 +123,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(goodExpr) + .withOptions(d_options) .withInputLanguage(d_lang) .build(); @@ -155,6 +161,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(badExpr) + .withOptions(d_options) .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); @@ -177,6 +184,7 @@ protected: void setUp() { d_exprManager = new ExprManager; + d_options.parseOnly = true; } void tearDown() { @@ -217,6 +225,14 @@ public: 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) 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() { @@ -232,6 +248,14 @@ public: 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;"); } void testGoodCvc4Exprs() { |