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