diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-02 20:04:18 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-02 20:04:18 +0000 |
commit | 86716e3782aae62a38987f7f89bdf5498eca534a (patch) | |
tree | ac2d524141bfc486351dcd5b092e3ebcbc3a0b3a /src/parser/cvc | |
parent | a1ee56b7d09b4f6430a048c53a3b5bd0a194357f (diff) |
Minor changes to parser
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 51473312e..cb9c9b160 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -59,8 +59,9 @@ command returns [CVC4::Command* cmd = 0] | CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); } | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(); } | identifierList[ids, CHECK_UNDECLARED] COLON type { - // [chris 12/15/2009] FIXME: decls may not be BOOLEAN - newPredicates(ids); + // FIXME: switch on type (may not be predicates) + vector<string> sorts; + newPredicates(ids,sorts); cmd = new DeclarationCommand(ids); } SEMICOLON @@ -239,4 +240,4 @@ boolAtom returns [CVC4::Expr atom] predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol] : pSymbol = identifier[check] ; -
\ No newline at end of file + |