adding three features to CVC parser that drastically improve its support for the...

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8fa1ca55a12b01440928852271f96da5edb3a9b7..3a8db1c03d9fe788e2b2e3d88c09101e16e67010 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -107,22 +107,41 @@ parseCommand returns [CVC4::Command* cmd]
 command returns [CVC4::Command* cmd = 0]
 @init {
   Expr f;
+  SExpr sexpr;
+  std::string s;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
   | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); }
+  | OPTION_TOK STRING_LITERAL symbolicExpr[sexpr] SEMICOLON
+    { cmd = new SetOptionCommand(AntlrInput::tokenText($STRING_LITERAL), sexpr); }
   | PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
   | POP_TOK SEMICOLON { cmd = new PopCommand(); }
   | declaration[cmd]
   | EOF
   ;
 
+symbolicExpr[CVC4::SExpr& sexpr]
+@declarations {
+  std::vector<SExpr> children;
+}
+  : INTEGER_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
+  | DECIMAL_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
+  | STRING_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); }
+  | IDENTIFIER
+    { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
+  | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
+    { sexpr = SExpr(children); }
+  ;
+
 /**
  * Match a declaration
  */
-
 declaration[CVC4::Command*& cmd]
 @init {
   std::vector<std::string> ids;
@@ -233,7 +252,7 @@ formula[CVC4::Expr& formula]
 @init {
   Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  :  iffFormula[formula]
+  : letBinding[formula]
   ;
 
 /**
@@ -249,6 +268,40 @@ formulaList[std::vector<CVC4::Expr>& formulas]
     )*
   ;
 
+/**
+ * Matches a LET binding
+ */
+letBinding[CVC4::Expr& f]
+@init {
+}
+  : LET_TOK
+    { PARSER_STATE->pushScope(); }
+    letDecls
+    IN_TOK letBinding[f]
+    { PARSER_STATE->popScope(); }
+  | iffFormula[f]
+  ;
+
+/**
+ * Matches (and defines) LET declarations in order.  Note this implements
+ * sequential-let (think "let*") rather than simultaneous-let.
+ */
+letDecls
+  : letDecl (COMMA letDecl)*
+  ;
+
+/**
+ * Matches (and defines) a single LET declaration.
+ */
+letDecl
+@init {
+  Expr e;
+  std::string name;
+}
+  : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
+    { PARSER_STATE->defineVar(name, e); }
+  ;
+
 /**
  * Matches a Boolean IFF formula (right-associative)
  */
@@ -390,14 +443,42 @@ multTerm[CVC4::Expr& f]
   Kind op;
   Debug("parser-extra") << "multiplication term: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : unaryTerm[f]
+  : expTerm[f]
     ( ( STAR_TOK { op = CVC4::kind::MULT; }
       | DIV_TOK { op = CVC4::kind::DIVISION; } ) 
-      unaryTerm[e]
+      expTerm[e]
       { f = MK_EXPR(op, f, e); }
     )*
   ;
 
+/**
+ * Parses an exponential term (left-associative).
+ * NOTE that the exponent must be a nonnegative integer constant
+ * (for now).
+ */
+expTerm[CVC4::Expr& f]
+@init {
+  Expr e;
+  Debug("parser-extra") << "exponential term: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : unaryTerm[f]
+    ( EXP_TOK INTEGER_LITERAL
+      { Integer n = AntlrInput::tokenToInteger($INTEGER_LITERAL);
+        if(n == 0) {
+          f = MK_CONST( Integer(1) );
+        } else if(n == 1) {
+          /* f remains the same */
+        } else {
+          std::vector<Expr> v;
+          for(Integer i = 0; i < n; i = i + 1) {
+            v.push_back(f);
+          }
+          f = MK_EXPR(CVC4::kind::MULT, v);
+        }
+      }
+    )*
+  ;
+
 /**
  * Parses a unary term.
  */
@@ -429,7 +510,7 @@ unaryTerm[CVC4::Expr& f]
   | TRUE_TOK  { f = MK_CONST(true); }
   | FALSE_TOK { f = MK_CONST(false); }
 
-  | NUMERAL_TOK { f = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
+  | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
@@ -494,8 +575,11 @@ ELSE_TOK : 'ELSE';
 ENDIF_TOK : 'ENDIF';
 FALSE_TOK : 'FALSE';
 IF_TOK : 'IF';
+IN_TOK : 'IN';
 INT_TOK : 'INT';
+LET_TOK : 'LET';
 NOT_TOK : 'NOT';
+OPTION_TOK : 'OPTION';
 OR_TOK : 'OR';
 POPTO_TOK : 'POPTO';
 POP_TOK : 'POP';
@@ -521,6 +605,7 @@ SEMICOLON : ';';
 ARROW_TOK : '->';
 DIV_TOK : '/';
 EQUAL_TOK : '=';
+EXP_TOK : '^';
 GT_TOK : '>';
 GEQ_TOK : '>=';
 IFF_TOK : '<=>';
@@ -538,9 +623,20 @@ STAR_TOK : '*';
 IDENTIFIER : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*;
 
 /**
- * Matches a numeral from the input (non-empty sequence of digits).
+ * Matches an integer literal.
+ */
+INTEGER_LITERAL: DIGIT+;
+
+/**
+ * Matches a decimal literal.
+ */
+DECIMAL_LITERAL: DIGIT+ '.' DIGIT+;
+
+/**
+ * Matches a double quoted string literal. Escaping is supported, and
+ * escape character '\' has to be escaped.
  */
-NUMERAL_TOK: (DIGIT)+;
+STRING_LITERAL: '"' (ESCAPE | ~('"'|'\\'))* '"';
 
 /**
  * Matches any letter ('a'-'z' and 'A'-'Z').
@@ -562,3 +658,8 @@ WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP();; };
  */
 COMMENT : '%' (~('\n' | '\r'))* { SKIP();; };
 
+/**
+ * Matches an allowed escaped character.
+ */
+fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
+

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 383cb01cb169675f625358a9952491607919c2f4..50c43fcb9bd7cd9bc79221f3cca7650e9d89c818 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -41,6 +41,7 @@ CVC_TESTS = \
        boolean-prec.cvc \
        hole6.cvc \
        ite.cvc \
+       let.cvc \
        logops.01.cvc \
        logops.02.cvc \
        logops.03.cvc \

diff --git a/test/regress/regress0/let.cvc b/test/regress/regress0/let.cvc
new file mode 100644 (file)
index 0000000..da628de
--- /dev/null
+++ b/test/regress/regress0/let.cvc
@@ -0,0 +1,8 @@
+% EXPECT: valid
+U: TYPE;
+a: U;
+b: U;
+f: U -> U;
+QUERY LET v_0 = (a = b)
+IN NOT (v_0 AND NOT v_0);
+% EXIT: 20