1 %{
2 /*****************************************************************************/
3 /*!
4 * \file smtlib2.y
5 *
6 * Author: Clark Barrett
7 *
8 * Created: Apr 30 2005
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 *
19 */
20 /*****************************************************************************/
21 /*
22 This file contains the bison code for the parser that reads in CVC
23 commands in SMT-LIB language.
24 */
25
26 #include "vc.h"
27 #include "parser_exception.h"
28 #include "parser_temp.h"
29 #include "translator.h"
30 #include "kinds.h"
31 #include "command_line_flags.h"
32 #include "theory_arith.h"
33
34 // Exported shared data
35 namespace CVC3 {
36 extern ParserTemp* parserTemp;
37 }
38 // Define shortcuts for various things
39 #define TMP CVC3::parserTemp
40 #define EXPR CVC3::parserTemp->expr
41 #define VC (CVC3::parserTemp->vc)
42 #define ARRAYSENABLED (CVC3::parserTemp->arrFlag)
43 #define BVENABLED (CVC3::parserTemp->bvFlag)
44 #define BVSIZE (CVC3::parserTemp->bvSize)
45 #define RAT(args) CVC3::newRational args
46 #define QUERYPARSED CVC3::parserTemp->queryParsed
47 #define TRANSLATOR CVC3::parserTemp->translator
48
49 // Suppress the bogus warning suppression in bison (it generates
50 // compile error)
51 #undef __GNUC_MINOR__
52
53 /* stuff that lives in smtlib2.lex */
54 extern int smtlib2lex(void);
55
smtlib2error(const char * s)56 int smtlib2error(const char *s)
57 {
58 std::ostringstream ss;
59 ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
60 << ": " << s;
61 return CVC3::parserTemp->error(ss.str());
62 }
63
64 #define YYLTYPE_IS_TRIVIAL 1
65 #define YYMAXDEPTH 10485760
66
67 // static hash_map<std::string,std::string> *operators;
68
69 %}
70
71 %union {
72 std::string *str;
73 std::vector<std::string> *strvec;
74 CVC3::Expr *node;
75 std::vector<CVC3::Expr> *vec;
76 std::pair<std::vector<CVC3::Expr>, std::vector<CVC3::Expr> > *pat_ann;
77 };
78
79
80 %start command
81
82 /* strings are for better error messages.
83 "_TOK" is so macros don't conflict with kind names */
84
85 %type <node> command command_aux non_keyword_sexpr sexpr term sort_symbol identifier binding sorted_var attribute
86 %type <vec> sexprs sort_symbols sort_symbols_nonempty terms bindings sorted_vars attributes numerals
87 %type <str> quantifier
88
89 %token <str> DECIMAL_TOK
90 %token <str> INTEGER_TOK
91 %token <str> HEX_TOK
92 %token <str> BINARY_TOK
93 %token <str> SYM_TOK
94 %token <str> KEYWORD_TOK
95 %token <str> STRING_TOK
96
97 %token ASSERT_TOK
98 %token CHECKSAT_TOK
99 %token PUSH_TOK
100 %token POP_TOK
101 %token DECLARE_FUN_TOK
102 %token DECLARE_SORT_TOK
103 %token GET_PROOF_TOK
104 %token GET_ASSIGNMENT_TOK
105 %token GET_VALUE_TOK
106 %token GET_MODEL_TOK
107 %token EXCLAMATION_TOK
108 %token EXIT_TOK
109 %token ITE_TOK
110 %token LET_TOK
111 %token LPAREN_TOK
112 %token RPAREN_TOK
113 %token SET_LOGIC_TOK
114 %token SET_INFO_TOK
115 %token UNDERSCORE_TOK
116 %token EOF_TOK
117
118 // Logic symbols
119 /* %token AND_TOK */
120 /* %token AT_TOK */
121 /* %token DISTINCT_TOK */
122 /* %token DIV_TOK */
123 /* %token EQUAL_TOK */
124 %token EXISTS_TOK
125 /* %token FALSE_TOK */
126 %token FORALL_TOK
127 /* %token GREATER_THAN_TOK */
128 /* %token GREATER_THAN_EQ_TOK */
129 /* %token IFF_TOK */
130 /* %token IMPLIES_TOK */
131 /* %token LESS_THAN_TOK */
132 /* %token LESS_THAN_EQ_TOK */
133 /* %token MINUS_TOK */
134 /* %token NOT_TOK */
135 /* %token OR_TOK */
136 /* %token PERCENT_TOK */
137 /* %token PLUS_TOK */
138 /* %token POUND_TOK */
139 /* %token STAR_TOK */
140 /* %token TRUE_TOK */
141 /* %token XOR_TOK */
142
143 %%
144
145 command:
146 LPAREN_TOK command_aux RPAREN_TOK
147 {
148 EXPR = *$2;
149 delete $2;
150 YYACCEPT;
151 }
152 | EOF_TOK
153 {
154 TMP->done = true;
155 EXPR = CVC3::Expr();
156 YYACCEPT;
157 }
158 ;
159
160 command_aux:
161 SET_LOGIC_TOK SYM_TOK
162 {
163 ARRAYSENABLED = false;
164 BVENABLED = false;
165 std::vector<CVC3::Expr> subCommands;
166
167 /* Add the symbols of the core theory */
168 subCommands.push_back( VC->listExpr("_TYPEDEF", VC->idExpr("Bool"),
169 VC->idExpr("_BOOLEAN")) );
170 subCommands.push_back( VC->listExpr("_CONST", VC->idExpr("true"),
171 VC->idExpr("Bool"),
172 VC->idExpr("_TRUE_EXPR")) );
173 subCommands.push_back( VC->listExpr("_CONST", VC->idExpr("false"),
174 VC->idExpr("Bool"),
175 VC->idExpr("_FALSE_EXPR")) );
176
177 if (*$2 == "QF_AX" ||
178 *$2 == "QF_AUFLIA" ||
179 *$2 == "AUFLIA" ||
180 *$2 == "QF_AUFLIRA" ||
181 *$2 == "AUFLIRA" ||
182 *$2 == "QF_AUFNIRA" ||
183 *$2 == "AUFNIRA" ||
184 *$2 == "QF_AUFBV" ||
185 *$2 == "QF_ABV") {
186 ARRAYSENABLED = true;
187 }
188
189 if (*$2 == "QF_AUFBV" ||
190 *$2 == "QF_ABV" ||
191 *$2 == "QF_BV" ||
192 *$2 == "QF_UFBV") {
193 BVENABLED = true;
194 }
195
196 /* Add the Int type for logics that include it */
197 if (*$2 == "AUFLIA" ||
198 *$2 == "AUFLIRA" ||
199 *$2 == "AUFNIRA" ||
200 *$2 == "QF_AUFLIA" ||
201 *$2 == "QF_IDL" ||
202 *$2 == "QF_LIA" ||
203 *$2 == "QF_NIA" ||
204 *$2 == "QF_UFIDL" ||
205 *$2 == "QF_UFLIA" ||
206 *$2 == "UFNIA" ) {
207 subCommands.push_back( VC->listExpr("_TYPEDEF", VC->idExpr("Int"),
208 VC->idExpr("_INT")) );
209 }
210
211 /* Add the Real type for logics that include it */
212 if (*$2 == "AUFLIRA" ||
213 *$2 == "AUFNIRA" ||
214 *$2 == "LRA" ||
215 *$2 == "QF_RDL" ||
216 *$2 == "QF_LRA" ||
217 *$2 == "QF_NRA" ||
218 *$2 == "QF_UFLRA" ||
219 *$2 == "QF_UFNRA" ||
220 *$2 == "UFLRA" ||
221 *$2 == "QF_UFRDL" ) {
222 subCommands.push_back( VC->listExpr("_TYPEDEF", VC->idExpr("Real"),
223 VC->idExpr("_REAL")) );
224 }
225
226 /* Enable complete instantiation heuristics */
227 if (*$2 == "AUFLIA" ||
228 *$2 == "AUFLIRA" ||
229 *$2 == "AUFNIRA" ||
230 *$2 == "LRA" ||
231 *$2 == "UFLRA" ||
232 *$2 == "UFNIA") {
233 subCommands.push_back( VC->listExpr("_OPTION",
234 VC->stringExpr("quant-complete-inst"),
235 VC->ratExpr(1)) );
236 }
237
238 $$ = new CVC3::Expr(VC->listExpr("_SEQ", subCommands));
239 delete $2;
240 }
241
242 | SET_INFO_TOK KEYWORD_TOK sexpr
243 {
244 $$ = NULL;
245 if(*$2 == ":status") {
246 TRANSLATOR->setStatus((*$3)[0].getString());
247 } else if(*$2 == ":source") {
248 if($3->getKind() == CVC3::STRING_EXPR) {
249 TRANSLATOR->setSource($3->getString());
250 } else if($3->getKind() == CVC3::ID) {
251 TRANSLATOR->setSource((*$3)[0].getString());
252 } else {
253 smtlib2error("bad type for set-info :source");
254 }
255 } else if(*$2 == ":category") {
256 TRANSLATOR->setCategory($3->getString());
257 } else if(*$2 == ":notes") {
258 std::string notes;
259 if($3->getKind() == CVC3::STRING_EXPR) {
260 notes = $3->getString();
261 } else if($3->getKind() == CVC3::ID) {
262 notes = (*$3)[0].getString();
263 } else {
264 smtlib2error("bad type for set-info :notes");
265 }
266 $$ = new CVC3::Expr(VC->listExpr("_ANNOTATION", VC->listExpr(VC->stringExpr("notes"), VC->stringExpr(notes))));
267 }
268 delete $2;
269 delete $3;
270 if($$ == NULL) {
271 $$ = new CVC3::Expr();
272 }
273 }
274
275 | DECLARE_SORT_TOK SYM_TOK INTEGER_TOK
276 {
277 $$ = new CVC3::Expr(VC->listExpr("_TYPE", VC->idExpr(*$2)));
278 delete $2;
279 }
280
281 | DECLARE_FUN_TOK SYM_TOK LPAREN_TOK sort_symbols RPAREN_TOK sort_symbol
282 {
283 if ($4->size() == 0) {
284 $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->idExpr(*$2), (*$6)));
285 }
286 else {
287 $4->push_back( *$6 );
288 CVC3::Expr tmp(VC->listExpr("_ARROW", *$4));
289 $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->idExpr(*$2), tmp));
290 }
291 delete $2;
292 delete $4;
293 delete $6;
294 }
295
296 | ASSERT_TOK term
297 {
298 $$ = new CVC3::Expr(VC->listExpr("_ASSERT", *$2));
299 delete $2;
300 }
301
302 | CHECKSAT_TOK
303 {
304 $$ = new CVC3::Expr(VC->listExpr("_CHECKSAT",
305 CVC3::Expr(VC->idExpr("_TRUE_EXPR"))));
306 }
307
308 | PUSH_TOK INTEGER_TOK
309 {
310 $$ = new CVC3::Expr(VC->listExpr("_PUSH", CVC3::Expr(VC->ratExpr((*$2)))));
311 }
312
313 | POP_TOK INTEGER_TOK
314 {
315 $$ = new CVC3::Expr(VC->listExpr("_POP", CVC3::Expr(VC->ratExpr((*$2)))));
316 }
317
318 | GET_PROOF_TOK
319 {
320 $$ = new CVC3::Expr(VC->listExpr(VC->idExpr("_DUMP_PROOF")));
321 }
322
323 | GET_ASSIGNMENT_TOK
324 {
325 $$ = new CVC3::Expr(VC->listExpr(VC->idExpr("_GET_ASSIGNMENT")));
326 }
327
328 | GET_VALUE_TOK LPAREN_TOK terms RPAREN_TOK
329 {
330 $$ = new CVC3::Expr(VC->listExpr(VC->idExpr("_GET_VALUE"), VC->listExpr(*$3)));
331 delete $3;
332 }
333
334 | GET_MODEL_TOK
335 {
336 $$ = new CVC3::Expr(VC->listExpr(VC->idExpr("_COUNTERMODEL")));
337 }
338
339 | EXIT_TOK
340 {
341 TMP->done = true;
342 $$ = new CVC3::Expr();
343 }
344 ;
345
346 sexprs:
347 sexpr
348 {
349 $$ = new std::vector<CVC3::Expr>;
350 $$->push_back(*$1);
351 delete $1;
352 }
353 | sexprs sexpr
354 {
355 $1->push_back(*$2);
356 $$ = $1;
357 delete $2;
358 }
359 ;
360
361
362 /* An S-expression that is not a keyword (NOTE: it may contain keywords
363 in sub-expressions; it's just not *only* a keyword). */
364 non_keyword_sexpr:
365 INTEGER_TOK
366 { $$ = new CVC3::Expr(VC->ratExpr(*$1));
367 delete $1; }
368 | DECIMAL_TOK
369 {
370 $$ = new CVC3::Expr(VC->ratExpr(*$1));
371 if(VC->getFlags()["translate"].getBool() && $1->find('.') != std::string::npos) {
372 CVC3::Expr* e = $$;
373 $$ = new CVC3::Expr(CVC3::REAL_CONST, *e);
374 delete e;
375 }
376 delete $1;
377 }
378 | STRING_TOK
379 { $$ = new CVC3::Expr(VC->stringExpr(*$1));
380 delete $1;}
381 | SYM_TOK
382 { $$ = new CVC3::Expr(VC->idExpr(*$1));
383 delete $1;}
384 | LPAREN_TOK sexprs RPAREN_TOK
385 { $$ = new CVC3::Expr(VC->listExpr(*$2));
386 delete $2; }
387 ;
388
389 sexpr:
390 non_keyword_sexpr
391 {
392 $$ = $1;
393 }
394 | KEYWORD_TOK
395 { $$ = new CVC3::Expr(VC->idExpr(*$1));
396 delete $1;}
397
398 /* Possibly empty list of sort symbols */
399 sort_symbols:
400 /* empty */
401 {
402 $$ = new std::vector<CVC3::Expr>;
403 }
404 | sort_symbols_nonempty
405 {
406 $$ = $1;
407 }
408 ;
409
410 sort_symbols_nonempty:
411 sort_symbol
412 {
413 $$ = new std::vector<CVC3::Expr>;
414 $$->push_back(*$1);
415 delete $1;
416 }
417 | sort_symbols sort_symbol
418 {
419 $1->push_back(*$2);
420 $$ = $1;
421 delete $2;
422 }
423 ;
424
425 sort_symbol:
426 identifier
427 {
428 CVC3::Expr id = *$1;
429 if( BVENABLED &&
430 id.isRawList() &&
431 id[0].getKind() == CVC3::ID &&
432 id[0][0].getString() == "BitVec" &&
433 id.arity() == 2 &&
434 id[1].isRational() ) {
435 $$ = new CVC3::Expr( VC->listExpr("_BITVECTOR", id[1]) );
436 delete $1;
437 } else {
438 $$ = $1;
439 }
440 }
441 | LPAREN_TOK identifier sort_symbols_nonempty RPAREN_TOK
442 {
443 CVC3::Expr id = *$2;
444 if (ARRAYSENABLED &&
445 id.getKind() == CVC3::ID &&
446 id[0].getString() == "Array"
447 && $3->size() == 2) {
448 $$ = new CVC3::Expr( VC->listExpr("_ARRAY", *$3) );
449 } else {
450 // FIXME: How to handle non-array parameterized types?
451 $3->insert( $3->begin(), *$2 );
452 $$ = new CVC3::Expr( VC->listExpr(*$3) );
453 }
454 delete $2;
455 delete $3;
456 }
457 ;
458
459 identifier:
460 SYM_TOK
461 {
462 std::string id = *$1;
463 /* If the id is a built-in operator, replace the text with the
464 internal name.
465
466 NOTE: the right way to do this would be would be with a
467 hash_map or trie.
468 */
469 if (id == "and") {
470 id = "_AND";
471 } else if (id == "distinct") {
472 id = "_DISTINCT";
473 } else if (id == "ite") {
474 id = "_IF";
475 } else if (id == "/") {
476 id = "_DIVIDE";
477 } else if (id == "=") {
478 id = "_EQ";
479 } else if (id == ">") {
480 id = "_GT";
481 } else if (id == ">=") {
482 id = "_GE";
483 } else if (id == "=>") {
484 id = "_IMPLIES";
485 } else if (id == "<") {
486 id = "_LT";
487 } else if (id == "<=") {
488 id = "_LE";
489 } else if (id == "-") {
490 id = "_MINUS";
491 } else if (id == "not") {
492 id = "_NOT";
493 } else if (id == "or") {
494 id = "_OR";
495 } else if (id == "+") {
496 id = "_PLUS";
497 } else if (id == "*") {
498 id = "_MULT";
499 } else if (id == "is_int") {
500 id = "_IS_INTEGER";
501 } else if (id == "xor") {
502 id = "_XOR";
503 } else if (ARRAYSENABLED && id == "select") {
504 id = "_READ";
505 } else if (ARRAYSENABLED && id == "store") {
506 id = "_WRITE";
507 } else if (BVENABLED && id == "concat") {
508 id = "_CONCAT";
509 } else if (BVENABLED && id == "bvadd") {
510 id = "_BVPLUS";
511 } else if (BVENABLED && id == "bvand") {
512 id = "_BVAND";
513 } else if (BVENABLED && id == "bvashr") {
514 id = "_BVASHR";
515 } else if (BVENABLED && id == "bvcomp") {
516 id = "_BVCOMP";
517 } else if (BVENABLED && id == "bvlshr") {
518 id = "_BVLSHR";
519 } else if (BVENABLED && id == "bvmul") {
520 id = "_BVMULT";
521 } else if (BVENABLED && id == "bvneg") {
522 id = "_BVUMINUS";
523 } else if (BVENABLED && id == "bvnand") {
524 id = "_BVNAND";
525 } else if (BVENABLED && id == "bvnot") {
526 id = "_BVNEG";
527 } else if (BVENABLED && id == "bvnor") {
528 id = "_BVNOR";
529 } else if (BVENABLED && id == "bvor") {
530 id = "_BVOR";
531 } else if (BVENABLED && id == "bvshl") {
532 id = "_BVSHL";
533 } else if (BVENABLED && id == "bvsdiv") {
534 id = "_BVSDIV";
535 } else if (BVENABLED && id == "bvsge") {
536 id = "_BVSGE";
537 } else if (BVENABLED && id == "bvsgt") {
538 id = "_BVSGT";
539 } else if (BVENABLED && id == "bvsle") {
540 id = "_BVSLE";
541 } else if (BVENABLED && id == "bvslt") {
542 id = "_BVSLT";
543 } else if (BVENABLED && id == "bvsmod") {
544 id = "_BVSMOD";
545 } else if (BVENABLED && id == "bvsrem") {
546 id = "_BVSREM";
547 } else if (BVENABLED && id == "bvsub") {
548 id = "_BVSUB";
549 } else if (BVENABLED && id == "bvudiv") {
550 id = "_BVUDIV";
551 } else if (BVENABLED && id == "bvuge") {
552 id = "_BVGE";
553 } else if (BVENABLED && id == "bvugt") {
554 id = "_BVGT";
555 } else if (BVENABLED && id == "bvule") {
556 id = "_BVLE";
557 } else if (BVENABLED && id == "bvult") {
558 id = "_BVLT";
559 } else if (BVENABLED && id == "bvurem") {
560 id = "_BVUREM";
561 } else if (BVENABLED && id == "bvxnor") {
562 id = "_BVXNOR";
563 } else if (BVENABLED && id == "bvxor") {
564 id = "_BVXOR";
565 }
566 $$ = new CVC3::Expr( VC->idExpr( id ) );
567 delete $1;
568 }
569 | LPAREN_TOK UNDERSCORE_TOK SYM_TOK numerals RPAREN_TOK
570 {
571 std::string id = *$3;
572 std::vector<CVC3::Expr> numerals = *$4;
573 if (BVENABLED &&
574 id.size() > 2 &&
575 id[0] == 'b' &&
576 id[1] == 'v' &&
577 numerals.size() == 1) {
578 DebugAssert( numerals[0].isRational() &&
579 numerals[0].getRational().isInteger(),
580 "Illegal size argument to bit-vector constant." );
581 $$ = new CVC3::Expr( VC->listExpr("_BVCONST",
582 VC->ratExpr(id.substr(2), 10),
583 (*$4)[0]) );
584 } else {
585 if (BVENABLED && id == "extract") {
586 id = "_EXTRACT";
587 } else if (BVENABLED && id == "repeat") {
588 id = "_BVREPEAT";
589 } else if (BVENABLED && id == "zero_extend") {
590 id = "_BVZEROEXTEND";
591 } else if (BVENABLED && id == "sign_extend") {
592 id = "_SX";
593 } else if (BVENABLED && id == "rotate_left") {
594 id = "_BVROTL";
595 } else if (BVENABLED && id == "rotate_right") {
596 id = "_BVROTR";
597 }
598 $$ = new CVC3::Expr( VC->listExpr( id, *$4 ) );
599 }
600 delete $3;
601 delete $4;
602 }
603 ;
604
605 /* a non-empty sequence of integers */
606 numerals:
607 INTEGER_TOK
608 {
609 $$ = new std::vector<CVC3::Expr>;
610 $$->push_back( VC->ratExpr(*$1) );
611 delete $1;
612 }
613 | numerals INTEGER_TOK
614 {
615 $1->push_back( VC->ratExpr(*$2) );
616 $$ = $1;
617 delete $2;
618 }
619 ;
620
621 /* A non-empty sequence of terms. */
622 terms:
623 term
624 {
625 $$ = new std::vector<CVC3::Expr>;
626 $$->push_back(*$1);
627 delete $1;
628 }
629 |
630 terms term
631 {
632 $1->push_back(*$2);
633 $$ = $1;
634 delete $2;
635 }
636 ;
637
638 term:
639 LPAREN_TOK identifier terms RPAREN_TOK
640 {
641 CVC3::Expr op = *$2;
642 std::vector<CVC3::Expr> args = *$3;
643
644 std::vector<CVC3::Expr> resultList;
645
646 bool isId = op.getKind() == CVC3::ID;
647 std::string opStr;
648 if( isId ) {
649 opStr = op[0].getString();
650 }
651
652 if( isId && opStr == "_MINUS" && args.size() == 1 ) {
653 resultList.push_back( VC->idExpr("_UMINUS") );
654 resultList.push_back( args[0] );
655 } else if( isId &&
656 ( opStr == "_AND" ||
657 opStr == "_OR" ||
658 opStr == "_XOR" ||
659 opStr == "_PLUS" ||
660 opStr == "_MULT" ) &&
661 args.size() == 1 ) {
662 smtlib2error("[bin,N]-ary operator used in unary context");
663 } else {
664 const int arity = op.arity();
665 isId = arity > 0 && op[0].getKind() == CVC3::ID;
666 if( isId ) {
667 opStr = op[0][0].getString();
668 }
669
670 if( BVENABLED && arity == 3 && isId &&
671 opStr == "_EXTRACT" &&
672 op[1].isRational() &&
673 op[1].getRational().isInteger() &&
674 op[2].isRational() &&
675 op[2].getRational().isInteger() ) {
676 resultList.push_back( op[0] );
677 resultList.push_back(op[1]);
678 resultList.push_back(op[2]);
679 } else if( BVENABLED && arity == 2 && isId &&
680 ( opStr == "_BVREPEAT" ||
681 opStr == "_BVZEROEXTEND" ||
682 opStr == "_BVROTL" ||
683 opStr == "_BVROTR" ||
684 opStr == "_SX" ) &&
685 op[1].isRational() &&
686 op[1].getRational().isInteger() ) {
687 resultList.push_back( op[0] );
688 if( opStr == "_SX" ) {
689 resultList.push_back(VC->idExpr("_smtlib"));
690 }
691 resultList.push_back(op[1]);
692 } else {
693 resultList.push_back(op);
694 }
695
696 resultList.insert( resultList.end(), args.begin(), args.end() );
697 }
698
699 $$ = new CVC3::Expr(VC->listExpr(resultList));
700 delete $2;
701 delete $3;
702 }
703
704 | LPAREN_TOK LET_TOK LPAREN_TOK bindings RPAREN_TOK term RPAREN_TOK
705 {
706 CVC3::Expr e(VC->listExpr(*$4));
707 $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$6));
708 delete $4;
709 delete $6;
710 }
711
712 | LPAREN_TOK quantifier LPAREN_TOK sorted_vars RPAREN_TOK term RPAREN_TOK
713 {
714 CVC3::Expr e(VC->listExpr(*$4));
715 CVC3::Expr body(*$6);
716 DebugAssert( body.arity() > 0, "Empty quantifier body." );
717 if( body[0].isString() &&
718 body[0].getString() == "_ANNOTATION" ) {
719 CVC3::Expr annots = body[2];
720 body = body[1]; // real body, stripping annot wrapper
721 std::vector<CVC3::Expr> patterns;
722 for( int i = 0; i < annots.arity(); ++i ) {
723 DebugAssert( annots[i].arity() == 2 &&
724 annots[i][0].getKind() == CVC3::ID,
725 "Illegal annotation." );
726 if( annots[i][0][0].getString() == ":pattern" ) {
727 patterns.push_back( annots[i][1] );
728 }
729 }
730 $$ = new CVC3::Expr(VC->listExpr(*$2, e, body, VC->listExpr(patterns)));
731 } else {
732 $$ = new CVC3::Expr(VC->listExpr(*$2, e, body));
733 }
734 delete $2;
735 delete $4;
736 delete $6;
737 }
738
739 | LPAREN_TOK EXCLAMATION_TOK term attributes RPAREN_TOK
740 {
741 $$ = new CVC3::Expr(VC->listExpr(VC->stringExpr("_ANNOTATION"),
742 *$3,
743 VC->listExpr(*$4)));
744 delete $3;
745 delete $4;
746 }
747
748 | identifier
749 {
750 $$ = $1;
751 }
752
753 | DECIMAL_TOK
754 {
755 $$ = new CVC3::Expr(VC->ratExpr(*$1));
756 if(VC->getFlags()["translate"].getBool() && $1->find('.') != std::string::npos) {
757 CVC3::Expr* e = $$;
758 $$ = new CVC3::Expr(CVC3::REAL_CONST, *e);
759 delete e;
760 }
761 delete $1;
762 }
763
764 | INTEGER_TOK
765 {
766 $$ = new CVC3::Expr(VC->ratExpr(*$1));
767 delete $1;
768 }
769
770 | HEX_TOK
771 {
772 std::vector<CVC3::Expr> args;
773 args.push_back(VC->idExpr("_BVCONST"));
774 args.push_back(VC->ratExpr(*$1, 16));
775 args.push_back(VC->ratExpr(4 * $1->length()));
776 $$ = new CVC3::Expr(VC->listExpr(args));
777 delete $1;
778 }
779
780 | BINARY_TOK
781 {
782 std::vector<CVC3::Expr> args;
783 args.push_back(VC->idExpr("_BVCONST"));
784 args.push_back(VC->ratExpr(*$1, 2));
785 args.push_back(VC->ratExpr($1->length()));
786 $$ = new CVC3::Expr(VC->listExpr(args));
787 delete $1;
788 }
789
790 ;
791
792 /* builtin: */
793 /* AND_TOK { $$ = new std::string("_AND"); } */
794 /* | DIV_TOK { $$ = new std::string("_DIVIDE"); } */
795 /* | DISTINCT_TOK { $$ = new std::string("_DISTINCT"); } */
796 /* | EQUAL_TOK { $$ = new std::string("_EQ"); } */
797 /* | GREATER_THAN_TOK { $$ = new std::string("_GT"); } */
798 /* | GREATER_THAN_EQ_TOK { $$ = new std::string("_GE"); } */
799 /* | IFF_TOK { $$ = new std::string("_IFF"); } */
800 /* | IMPLIES_TOK { $$ = new std::string("_IMPLIES"); } */
801 /* | ITE_TOK { $$ = new std::string("_IF"); } */
802 /* | LESS_THAN_TOK { $$ = new std::string("_LT"); } */
803 /* | LESS_THAN_EQ_TOK { $$ = new std::string("_LE"); } */
804 /* | MINUS_TOK { $$ = new std::string("_MINUS"); } */
805 /* | NOT_TOK { $$ = new std::string("_NOT"); } */
806 /* | OR_TOK { $$ = new std::string("_OR"); } */
807 /* | PLUS_TOK { $$ = new std::string("_PLUS"); } */
808 /* | STAR_TOK { $$ = new std::string("_MULT"); } */
809 /* | XOR_TOK { $$ = new std::string("_XOR"); } */
810 /* ; */
811
812 /* Returns a vector containing the operator and its arguments.
813 This is necessary because of the behavior of certain parameterized
814 operators (e.g., extract). */
815 /* op: */
816 /* builtin */
817 /* { */
818 /* $$ = new std::vector<CVC3::Expr>; */
819 /* $$->push_back( VC->idExpr(*$1) ); */
820 /* delete $1; */
821 /* } */
822 /* | identifier */
823 /* { */
824 /* $$ = new std::vector<CVC3::Expr>; */
825 /* CVC3::Expr id = *$1; */
826 /* if( id.getKind() == CVC3::ID ) { */
827 /* std::string fname = id[0].getString(); */
828 /* if (ARRAYSENABLED && fname == "select") { */
829 /* $$->push_back( VC->idExpr("_READ") ); */
830 /* } else if (ARRAYSENABLED && fname == "store") { */
831 /* $$->push_back( VC->idExpr("_WRITE") ); */
832 /* } else if (BVENABLED && fname == "concat") { */
833 /* $$->push_back( VC->idExpr("_CONCAT") ); */
834 /* } else if (BVENABLED && fname == "bvadd") { */
835 /* $$->push_back( VC->idExpr("_BVPLUS") ); */
836 /* } else if (BVENABLED && fname == "bvand") { */
837 /* $$->push_back( VC->idExpr("_BVAND") ); */
838 /* } else if (BVENABLED && fname == "bvashr") { */
839 /* $$->push_back( VC->idExpr("_BVASHR") ); */
840 /* } else if (BVENABLED && fname == "bvcomp") { */
841 /* $$->push_back( VC->idExpr("_BVCOMP") ); */
842 /* } else if (BVENABLED && fname == "bvlshr") { */
843 /* $$->push_back( VC->idExpr("_BVLSHR") ); */
844 /* } else if (BVENABLED && fname == "bvmul") { */
845 /* $$->push_back( VC->idExpr("_BVMULT") ); */
846 /* } else if (BVENABLED && fname == "bvneg") { */
847 /* $$->push_back( VC->idExpr("_BVUMINUS") ); */
848 /* } else if (BVENABLED && fname == "bvnand") { */
849 /* $$->push_back( VC->idExpr("_BVNAND") ); */
850 /* } else if (BVENABLED && fname == "bvnot") { */
851 /* $$->push_back( VC->idExpr("_BVNEG") ); */
852 /* } else if (BVENABLED && fname == "bvnor") { */
853 /* $$->push_back( VC->idExpr("_BVNOR") ); */
854 /* } else if (BVENABLED && fname == "bvor") { */
855 /* $$->push_back( VC->idExpr("_BVOR") ); */
856 /* } else if (BVENABLED && fname == "bvshl") { */
857 /* $$->push_back( VC->idExpr("_BVSHL") ); */
858 /* } else if (BVENABLED && fname == "bvsdiv") { */
859 /* $$->push_back( VC->idExpr("_BVSDIV") ); */
860 /* } else if (BVENABLED && fname == "bvsge") { */
861 /* $$->push_back( VC->idExpr("_BVSGE") ); */
862 /* } else if (BVENABLED && fname == "bvsgt") { */
863 /* $$->push_back( VC->idExpr("_BVSGT") ); */
864 /* } else if (BVENABLED && fname == "bvsle") { */
865 /* $$->push_back( VC->idExpr("_BVSLE") ); */
866 /* } else if (BVENABLED && fname == "bvslt") { */
867 /* $$->push_back( VC->idExpr("_BVSLT") ); */
868 /* } else if (BVENABLED && fname == "bvsrem") { */
869 /* $$->push_back( VC->idExpr("_BVSREM") ); */
870 /* } else if (BVENABLED && fname == "bvsub") { */
871 /* $$->push_back( VC->idExpr("_BVSUB") ); */
872 /* } else if (BVENABLED && fname == "bvudiv") { */
873 /* $$->push_back( VC->idExpr("_BVUDIV") ); */
874 /* } else if (BVENABLED && fname == "bvuge") { */
875 /* $$->push_back( VC->idExpr("_BVUGE") ); */
876 /* } else if (BVENABLED && fname == "bvugt") { */
877 /* $$->push_back( VC->idExpr("_BVUGT") ); */
878 /* } else if (BVENABLED && fname == "bvule") { */
879 /* $$->push_back( VC->idExpr("_BVULE") ); */
880 /* } else if (BVENABLED && fname == "bvult") { */
881 /* $$->push_back( VC->idExpr("_BVLT") ); */
882 /* } else if (BVENABLED && fname == "bvurem") { */
883 /* $$->push_back( VC->idExpr("_BVUREM") ); */
884 /* } else if (BVENABLED && fname == "bvxnor") { */
885 /* $$->push_back( VC->idExpr("_BVXNOR") ); */
886 /* } else if (BVENABLED && fname == "bvxor") { */
887 /* $$->push_back( VC->idExpr("_BVXOR") ); */
888 /* } else { */
889 /* $$->push_back( id ); */
890 /* } */
891 /* } else if( BVENABLED && */
892 /* id.arity() > 0 && */
893 /* id[0].getKind() == CVC3::ID ) { */
894 /* if( id.arity() == 3 && */
895 /* id[0][0].getString() == "extract" && */
896 /* id[1].isRational() && */
897 /* id[1].getRational().isInteger() && */
898 /* id[2].isRational() && */
899 /* id[2].getRational().isInteger() ) { */
900 /* $$->push_back( VC->idExpr("_EXTRACT") ); */
901 /* $$->push_back(id[1]); */
902 /* $$->push_back(id[2]); */
903 /* } else if( id.arity() == 2 && */
904 /* id[0][0].getString() == "repeat" && */
905 /* id[1].isRational() && */
906 /* id[1].getRational().isInteger() ) { */
907 /* $$->push_back( VC->idExpr("_BVREPEAT") ); */
908 /* $$->push_back(id[1]); */
909 /* } else if( id.arity() == 2 && */
910 /* id[0][0].getString() == "zero_extend" && */
911 /* id[1].isRational() && */
912 /* id[1].getRational().isInteger() ) { */
913 /* $$->push_back( VC->idExpr("_BVZEROEXTEND") ); */
914 /* $$->push_back(id[1]); */
915 /* } else if( id.arity() == 2 && */
916 /* id[0][0].getString() == "sign_extend" && */
917 /* id[1].isRational() && */
918 /* id[1].getRational().isInteger() ) { */
919 /* $$->push_back( VC->idExpr("_SX") ); */
920 /* $$->push_back(VC->idExpr("_smtlib")); */
921 /* $$->push_back(id[1]); */
922 /* } else if( id.arity() == 2 && */
923 /* id[0].getKind() == CVC3::ID && */
924 /* id[0][0].getString() == "rotate_left" && */
925 /* id[1].isRational() && */
926 /* id[1].getRational().isInteger() ) { */
927 /* $$->push_back( VC->idExpr("_BVROTL") ); */
928 /* $$->push_back(id[1]); */
929 /* } else if( id.arity() == 2 && */
930 /* id[0].getKind() == CVC3::ID && */
931 /* id[0][0].getString() == "rotate_right" && */
932 /* id[1].isRational() && */
933 /* id[1].getRational().isInteger() ) { */
934 /* $$->push_back( VC->idExpr("_BVROTR") ); */
935 /* $$->push_back(id[1]); */
936 /* } else { */
937 /* $$->push_back(id); */
938 /* } */
939 /* } else { */
940 /* $$->push_back(id); */
941 /* } */
942 /* delete $1; */
943 /* } */
944 /* ; */
945
946 quantifier:
947 EXISTS_TOK
948 {
949 $$ = new std::string("_EXISTS");
950 }
951 | FORALL_TOK
952 {
953 $$ = new std::string("_FORALL");
954 }
955 ;
956
957
958 /* A non-empty sequence of (var term) bindings */
959 bindings:
960 binding
961 {
962 $$ = new std::vector<CVC3::Expr>;
963 $$->push_back(*$1);
964 delete $1;
965 }
966 | bindings binding
967 {
968 $1->push_back(*$2);
969 $$ = $1;
970 delete $2;
971 }
972 ;
973
974 binding:
975 LPAREN_TOK SYM_TOK term RPAREN_TOK
976 { $$ = new CVC3::Expr( VC->listExpr(*$2, *$3) );
977 delete $2;
978 delete $3; }
979 ;
980
981 /* A non-empty sequence of (var sort) decls */
982 sorted_vars:
983 sorted_var
984 {
985 $$ = new std::vector<CVC3::Expr>;
986 $$->push_back(*$1);
987 delete $1;
988 }
989 | sorted_vars sorted_var
990 {
991 $1->push_back(*$2);
992 $$ = $1;
993 delete $2;
994 }
995 ;
996
997 sorted_var:
998 LPAREN_TOK SYM_TOK sort_symbol RPAREN_TOK
999 {
1000 $$ = new CVC3::Expr(VC->listExpr(*$2, *$3));
1001 delete $2;
1002 delete $3;
1003 }
1004 ;
1005
1006 /* A non-empty sequence of attributes */
1007 attributes:
1008 attribute
1009 {
1010 $$ = new std::vector<CVC3::Expr>;
1011 $$->push_back( *$1 );
1012 delete $1;
1013 }
1014 | attributes attribute
1015 {
1016 $1->push_back( *$2 );
1017 $$ = $1;
1018 delete $2;
1019 }
1020 ;
1021
1022 attribute:
1023 KEYWORD_TOK
1024 {
1025 $$ = new CVC3::Expr( VC->idExpr(*$1) );
1026 delete $1;
1027 }
1028
1029 | KEYWORD_TOK SYM_TOK
1030 {
1031 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->idExpr(*$2) ) );
1032 delete $1;
1033 delete $2;
1034 }
1035
1036 | KEYWORD_TOK INTEGER_TOK
1037 {
1038 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->ratExpr(*$2) ) );
1039 delete $1;
1040 delete $2;
1041 }
1042
1043 | KEYWORD_TOK DECIMAL_TOK
1044 {
1045 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->ratExpr(*$2) ) );
1046 delete $1;
1047 delete $2;
1048 }
1049
1050 | KEYWORD_TOK HEX_TOK
1051 {
1052 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->ratExpr(*$2, 16) ) );
1053 delete $1;
1054 delete $2;
1055 }
1056
1057 | KEYWORD_TOK BINARY_TOK
1058 {
1059 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->ratExpr(*$2, 2) ) );
1060 delete $1;
1061 delete $2;
1062 }
1063
1064 | KEYWORD_TOK STRING_TOK
1065 {
1066 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->stringExpr(*$2) ) );
1067 delete $1;
1068 delete $2;
1069 }
1070
1071 | KEYWORD_TOK LPAREN_TOK terms RPAREN_TOK
1072 {
1073 // was "non_keyword_sexpr" above instead of "(terms)", but that breaks :pattern
1074 $$ = new CVC3::Expr( VC->listExpr( VC->idExpr(*$1), VC->listExpr(*$3) ) );
1075 delete $1;
1076 delete $3;
1077 }
1078 ;
1079 %%
1080