Adding preliminary let/flet support to SMT parser (Bug #51)

diff --git a/.project b/.project
index 9f40fa24590b32c32efd5c9fcd624b54bb20fdd8..cd77320476b1b4c2d9787f5f3e4022474d142608 100644 (file)
--- a/.project
+++ b/.project
@@ -5,6 +5,11 @@
        <projects>
        </projects>
        <buildSpec>
+               <buildCommand>
+                       <name>org.eclipse.dltk.core.scriptbuilder</name>
+                       <arguments>
+                       </arguments>
+               </buildCommand>
                <buildCommand>
                        <name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
                        <triggers>clean,full,incremental,</triggers>
@@ -82,5 +87,6 @@
                <nature>org.eclipse.cdt.core.ccnature</nature>
                <nature>org.eclipse.cdt.managedbuilder.core.managedBuildNature</nature>
                <nature>org.eclipse.cdt.managedbuilder.core.ScannerConfigNature</nature>
+               <nature>net.certiv.antlrdt.core.nature</nature>
        </natures>
 </projectDescription>

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 9b18eeb5a788acfbb2f5392e628f2daf11ad08d2..cadff04ac81a9e382df16254f949504f5fe97412 100644 (file)
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -171,10 +171,8 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
 Expr 
 AntlrParser::mkVar(const std::string& name, const Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
-  Assert( !isDeclared(name) );
   Expr expr = d_exprManager->mkVar(type, name);
-  d_varSymbolTable.bindName(name, expr);
-  Assert( isDeclared(name) );
+  defineVar(name,expr);
   return expr;
 }
 
@@ -188,6 +186,12 @@ AntlrParser::mkVars(const std::vector<std::string> names,
   return vars;
 }
 
+void
+AntlrParser::defineVar(const std::string& name, const Expr& val) {
+  Assert(!isDeclared(name));
+  d_varSymbolTable.bindName(name,val);
+  Assert(isDeclared(name));
+}
 
 const Type* 
 AntlrParser::newSort(const std::string& name) {

diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index e68405eb9dce15a8fadc3ea03de19494d5fdd059..5a6beb1320871d62b1a20482767cf9cf81b3cb29 100644 (file)
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -252,6 +252,8 @@ protected:
   mkVars(const std::vector<std::string> names, 
          const Type* type);
 
+  /** Create a new variable definition (e.g., from a let binding). */
+  void defineVar(const std::string& name, const Expr& val);
 
   /** Returns a function type over the given domain and range types. */
   const Type* functionType(const Type* domain, const Type* range);

diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index 695b7b787aebb7d1f805e8a2bf0678259a7b7fb3..e3985818c082ed8f6a464b9da1d5c9295f8dd4ca 100644 (file)
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -110,10 +110,19 @@ IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
  * Matches an identifier starting with a colon. An identifier is a sequence of letters,
  * digits and "_", "'", "." symbols, starting with a colon.
  */
-C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; }
+C_IDENTIFIER options { paraphrase = "an attribute (e.g., ':x')"; testLiterals = true; }
   :  ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
   ;
 
+VAR_IDENTIFIER options { paraphrase = "a variable (e.g., '?x')"; testLiterals = false; }
+  :  '?' IDENTIFIER 
+  ;
+
+FUN_IDENTIFIER options { paraphrase = "a function variable (e.g, '$x')"; testLiterals = false; }
+  :  '$' IDENTIFIER 
+  ;
+
+
 /**
  * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with
  * an open brace and end with closed brace.

diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 7759cf965bae93ab93a8597d4811d2f501170293..c12aa5f7a588dfecd968c6bc202fa9e121c66aa4 100644 (file)
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -120,6 +120,8 @@ annotatedFormula returns [CVC4::Expr formula]
   Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
   Kind kind = CVC4::kind::UNDEFINED_KIND;
   vector<Expr> args; 
+  std::string name;
+  Expr expr1, expr2, expr3;
 }
   : /* a built-in operator application */
     LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
@@ -127,6 +129,7 @@ annotatedFormula returns [CVC4::Expr formula]
       formula = mkExpr(kind,args); }
 
   | /* a "distinct" expr */
+    /* TODO: Should there be a DISTINCT kind in the Expr package? */
     LPAREN DISTINCT annotatedFormulas[args] RPAREN
     { std::vector<Expr> diseqs;
       for(unsigned i = 0; i < args.size(); ++i) {
@@ -146,7 +149,20 @@ annotatedFormula returns [CVC4::Expr formula]
     RPAREN
     { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); }
 
+  | /* A let binding */
+    /* TODO: Create an Expr of LET kind? */
+    LPAREN LET LPAREN name=variable[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN
+    { defineVar(name,expr1); }
+    formula=annotatedFormula
+    RPAREN
 
+  | /* An flet binding */
+    /* TODO: Create an Expr of LET kind? */
+    LPAREN FLET LPAREN name=function_var[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN
+    { defineVar(name,expr1); }
+    formula=annotatedFormula
+    RPAREN
+    
   | /* A non-built-in function application */
 
     // Semantic predicate not necessary if parenthesized subexpressions
@@ -162,7 +178,9 @@ annotatedFormula returns [CVC4::Expr formula]
 
   | /* a variable */
     { std::string name; }
-    name = identifier[CHECK_DECLARED]
+    ( name = identifier[CHECK_DECLARED] 
+      | name = variable[CHECK_DECLARED]
+      | name = function_var[CHECK_DECLARED] )
     { formula = getVariable(name); }
 
     /* constants */
@@ -236,6 +254,18 @@ attribute
   :  C_IDENTIFIER
   ;
 
+variable[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+  : x:VAR_IDENTIFIER
+    { name = x->getText();
+      checkDeclaration(name, check, SYM_VARIABLE); }
+  ;
+
+function_var[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+  : x:FUN_IDENTIFIER
+    { name = x->getText();
+      checkDeclaration(name, check, SYM_FUNCTION); }
+  ;
+
 /**
  * Matches the sort symbol, which can be an arbitrary identifier.
  * @param check the check to perform on the name
@@ -328,6 +358,6 @@ returns [std::string id]
 }
   : x:IDENTIFIER
     { id = x->getText();
-      checkDeclaration(id, check,type); }
+      checkDeclaration(id, check, type); }
   ;
 

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index a8786b4ff58eb18796009e4e89be7728f077309a..29141d63343e6524ee58b27dc21027f4a00276e0 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -2,7 +2,12 @@ SUBDIRS = precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
 TESTS =        bug32.cvc \
+    distinct.smt \
+    flet.smt \
+    flet2.smt \
        hole6.cvc \
+       let.smt \
+       let2.smt \
        logops.01.cvc \
        logops.02.cvc \
        logops.03.cvc \

diff --git a/test/regress/regress0/flet.smt b/test/regress/regress0/flet.smt
new file mode 100644 (file)
index 0000000..95742de
--- /dev/null
+++ b/test/regress/regress0/flet.smt
@@ -0,0 +1,5 @@
+(benchmark flet_test
+  :logic QF_UF
+  :status unsat
+  :extrapreds ((a) (b)) 
+  :formula (flet ($x (and a b)) (and $x (or (not a) (not b)))))
\ No newline at end of file

diff --git a/test/regress/regress0/flet2.smt b/test/regress/regress0/flet2.smt
new file mode 100644 (file)
index 0000000..4d71ebf
--- /dev/null
+++ b/test/regress/regress0/flet2.smt
@@ -0,0 +1,5 @@
+(benchmark flet_test
+  :logic QF_UF
+  :status sat
+  :extrapreds ((a) (b)) 
+  :formula (flet ($x (and a b)) (and $x (or a b))))
\ No newline at end of file

diff --git a/test/regress/regress0/let.smt b/test/regress/regress0/let.smt
new file mode 100644 (file)
index 0000000..45d0eae
--- /dev/null
+++ b/test/regress/regress0/let.smt
@@ -0,0 +1,5 @@
+(benchmark let_test
+  :logic QF_UF
+  :status unsat
+  :extrafuns ((a U) (b U) (f U U)) 
+  :formula (let (?x a) (not (= ?x a))))
\ No newline at end of file

diff --git a/test/regress/regress0/let2.smt b/test/regress/regress0/let2.smt
new file mode 100644 (file)
index 0000000..aa3d20b
--- /dev/null
+++ b/test/regress/regress0/let2.smt
@@ -0,0 +1,5 @@
+(benchmark let_test
+  :logic QF_UF
+  :status sat
+  :extrafuns ((a U) (b U) (f U U)) 
+  :formula (let (?x (f a)) (= ?x (f b))))
\ No newline at end of file