diff options
-rw-r--r-- | .project | 6 | ||||
-rw-r--r-- | src/parser/antlr_parser.cpp | 10 | ||||
-rw-r--r-- | src/parser/antlr_parser.h | 2 | ||||
-rw-r--r-- | src/parser/smt/smt_lexer.g | 11 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 34 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/flet.smt | 5 | ||||
-rw-r--r-- | test/regress/regress0/flet2.smt | 5 | ||||
-rw-r--r-- | test/regress/regress0/let.smt | 5 | ||||
-rw-r--r-- | test/regress/regress0/let2.smt | 5 |
10 files changed, 82 insertions, 6 deletions
@@ -6,6 +6,11 @@ </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> <arguments> @@ -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 9b18eeb5a..cadff04ac 100644 --- 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 e68405eb9..5a6beb132 100644 --- 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 695b7b787..e3985818c 100644 --- 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 7759cf965..c12aa5f7a 100644 --- 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 a8786b4ff..29141d633 100644 --- 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 index 000000000..95742de77 --- /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 index 000000000..4d71ebf30 --- /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 index 000000000..45d0eaecb --- /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 index 000000000..aa3d20b8c --- /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 |