summaryrefslogtreecommitdiff
path: root/src/parser/cvc/cvc_parser.g
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-02-02 20:04:18 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-02-02 20:04:18 +0000
commit86716e3782aae62a38987f7f89bdf5498eca534a (patch)
treeac2d524141bfc486351dcd5b092e3ebcbc3a0b3a /src/parser/cvc/cvc_parser.g
parenta1ee56b7d09b4f6430a048c53a3b5bd0a194357f (diff)
Minor changes to parser
Diffstat (limited to 'src/parser/cvc/cvc_parser.g')
-rw-r--r--src/parser/cvc/cvc_parser.g7
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
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback