summaryrefslogtreecommitdiff
path: root/src/parser/cvc/Cvc.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r--src/parser/cvc/Cvc.g4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index cd4c66664..75a59c6e0 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -53,6 +53,7 @@ tokens {
CHECK_TYPE_TOK = 'CHECK_TYPE';
GET_CHILD_TOK = 'GET_CHILD';
GET_OP_TOK = 'GET_OP';
+ GET_VALUE_TOK = 'GET_VALUE';
SUBSTITUTE_TOK = 'SUBSTITUTE';
DBG_TOK = 'DBG';
TRACE_TOK = 'TRACE';
@@ -646,6 +647,9 @@ mainCommand[CVC4::Command*& cmd]
| GET_OP_TOK formula[f]
{ UNSUPPORTED("GET_OP command"); }
+ | GET_VALUE_TOK formula[f]
+ { cmd = new GetValueCommand(f); }
+
| SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK
formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET
{ UNSUPPORTED("SUBSTITUTE command"); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback