From cf8b81553abf579d151b04a40cd82dec48bfd6ff Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 3 Feb 2010 22:46:36 +0000 Subject: [PATCH] Adding functions/predicates to SMT grammar --- src/expr/kind.h | 3 +- src/parser/antlr_parser.cpp | 43 ++++++++ src/parser/antlr_parser.h | 50 +++++++++- src/parser/smt/smt_lexer.g | 29 ++++++ src/parser/smt/smt_parser.g | 192 ++++++++++++++++++++++++++++++++++-- test/regress/simple-uf.smt | 7 ++ 6 files changed, 314 insertions(+), 10 deletions(-) create mode 100644 test/regress/simple-uf.smt diff --git a/src/expr/kind.h b/src/expr/kind.h index 8ba282f0f..64991c71c 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -36,6 +36,7 @@ enum Kind { ITE, SKOLEM, VARIABLE, + APPLY, /* propositional connectives */ FALSE, @@ -53,7 +54,6 @@ enum Kind { PLUS, MINUS, MULT - };/* enum Kind */ inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; @@ -70,6 +70,7 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) { case ITE: out << "ITE"; break; case SKOLEM: out << "SKOLEM"; break; case VARIABLE: out << "VARIABLE"; break; + case APPLY: out << "APPLY"; break; /* propositional connectives */ case FALSE: out << "FALSE"; break; diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 34bf4bc82..171da47e8 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -82,6 +82,19 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { return result; } +void AntlrParser::newFunction(std::string name, + const std::vector< std::string>& sorts) { + // FIXME: Need to actually create a function type + d_varSymbolTable.bindName(name, d_exprManager->mkVar()); +} + +void AntlrParser::newFunctions(const std::vector& names, + const std::vector< std::string>& sorts) { + for(unsigned i = 0; i < names.size(); ++i) { + newFunction(names[i], sorts); + } +} + void AntlrParser::newPredicate(std::string name, const std::vector& sorts) { Debug("parser") << "newPredicate(" << name << ")" << std::endl; @@ -99,6 +112,23 @@ void AntlrParser::newPredicates(const std::vector& names, } } +bool AntlrParser::isSort(std::string name) { + return d_sortTable.isBound(name); +} + +void AntlrParser::newSort(std::string name) { + Assert( !isSort(name) ) ; + // Trivial binding + d_sortTable.bindName(name,name); + Assert( isSort(name) ) ; +} + +void AntlrParser::newSorts(const std::vector& names) { + for(unsigned i = 0; i < names.size(); ++i) { + newSort(names[i]); + } +} + void AntlrParser::setExpressionManager(ExprManager* em) { d_exprManager = em; } @@ -132,5 +162,18 @@ bool AntlrParser::checkDeclaration(string varName, DeclarationCheck check) { } } +bool AntlrParser::checkSort(std::string name, DeclarationCheck check) { + switch(check) { + case CHECK_DECLARED: + return isSort(name); + case CHECK_UNDECLARED: + return !isSort(name); + case CHECK_NONE: + return true; + default: + Unhandled("Unknown check type!"); + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index a3015eb22..0c6deb95a 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -119,6 +119,15 @@ protected: */ bool checkDeclaration(std::string varName, DeclarationCheck check); + /** + * Return true if the the declaration policy we want to enforce is true + * on the given sort name. + * @param name the sort symbol to check + * @oaram check the kind of check to perform + * @return true if the check holds + */ + bool checkSort(std::string name, DeclarationCheck check); + /** * Types of symbols. */ @@ -137,6 +146,12 @@ protected: */ bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE); + /** + * Checks if the sort has been declared. + * @param the sort name + */ + bool isSort(std::string name); + /** * Returns the true expression. * @return the true expression @@ -185,8 +200,26 @@ protected: Expr mkExpr(Kind kind, const std::vector& children); /** - * Creates a new predicate over the given sorts. The predicate - * has arity sorts.size(). + * Creates a new function over the given sorts. The function + * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1]. + * @param name the name of the function + * @param sorts the sorts + */ + void newFunction(std::string name, + const std::vector& sorts); + + /** + * Creates new functions over the given sorts. Each function has + * arity sorts.size() - 1 and range type sorts[sorts.size() - 1]. + * @param name the name of the function + * @param sorts the sorts + */ + void newFunctions(const std::vector& names, + const std::vector& sorts); + + /** + * Creates a new predicate over the given sorts. The predicate has + * arity sorts.size(). * @param name the name of the predicate * @param sorts the sorts */ @@ -200,6 +233,16 @@ protected: void newPredicates(const std::vector& names, const std::vector< std::string>& sorts); + /** + * Creates a new sort with the given name. + */ + void newSort(std::string name); + + /** + * Creates a new sorts with the given names. + */ + void newSorts(const std::vector& names); + /** * Returns the precedence rank of the kind. */ @@ -212,6 +255,9 @@ private: /** The symbol table lookup */ SymbolTable d_varSymbolTable; + + /** The sort table */ + SymbolTable d_sortTable; }; }/* CVC4::parser namespace */ diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index e9abab61a..f1c01ea05 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -64,6 +64,20 @@ tokens { EXTRAFUNS_ATTR = ":extrafuns"; EXTRAPREDS_ATTR = ":extrapreds"; C_NOTES = ":notes"; + // arithmetic symbols + EQUAL = "="; + LESS_THAN = "<"; + GREATER_THAN = ">"; + AMPERSAND = "&"; + AT = "@"; + POUND = "#"; + PLUS = "+"; + MINUS = "-"; + STAR = "*"; + DIV = "/"; + PERCENT = "%"; + PIPE = "|"; + TILDE = "~"; } /** @@ -179,3 +193,18 @@ STRING_LITERAL options { paraphrase = "a string literal"; } COMMENT options { paraphrase = "comment"; } : ';' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); } ; + +/* Arithmetic symbol tokens */ +EQUAL : "="; +LESS_THAN : "<"; +GREATER_THAN : ">"; +AMPERSAND : "&"; +AT : "@"; +POUND : "#"; +PLUS : "+"; +MINUS : "-"; +STAR : "*"; +DIV : "/"; +PERCENT : "%"; +PIPE : "|"; +TILDE : "~"; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 3933a04f0..c0e53027d 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -98,10 +98,12 @@ benchAttribute returns [Command* smt_command = 0] { smt_command = new AssertCommand(formula); } | FORMULA_ATTR formula = annotatedFormula { smt_command = new CheckSatCommand(formula); } - | STATUS_ATTR b_status = status - { smt_command = new SetBenchmarkStatusCommand(b_status); } - | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN - | NOTES_ATTR STRING_LITERAL + | STATUS_ATTR b_status = status + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN + | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN + | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN + | NOTES_ATTR STRING_LITERAL | annotation ; @@ -132,17 +134,102 @@ annotatedFormula returns [CVC4::Expr formula] Kind kind; vector children; } +<<<<<<< .mine + : formula = annotatedAtom + | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN + { formula = mkExpr(kind, children); } + /* TODO: let, flet, quantifiers */ +======= : formula = annotatedAtom | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); } +>>>>>>> .r150 ; /** +<<<<<<< .mine + * Matches a sequence of annotaed formulas and puts them into the formulas + * vector. + * @param formulas the vector to fill with formulas + */ +annotatedFormulas[std::vector& formulas] +{ + Expr f; +} + : ( f = annotatedFormula { formulas.push_back(f); } )+ + ; + +/** + * Matches an annotated proposition atom, which is either a propositional atom + * or built of other atoms using a predicate symbol. +======= * Matches an annotated proposition atom, which is either a propositional atom * or built of other atoms using a predicate symbol. +>>>>>>> .r150 * @return expression representing the atom */ +<<<<<<< .mine +annotatedAtom returns [CVC4::Expr atom] +{ + Kind kind; + string predName; + Expr pred; + vector children; +} + : atom = propositionalAtom +======= annotatedAtom returns [CVC4::Expr atom] : atom = propositionalAtom +>>>>>>> .r150 + | LPAREN kind = arithPredicate annotatedTerms[children] RPAREN + { atom = mkExpr(kind,children); } + | LPAREN pred = predicateSymbol + { children.push_back(pred); } + annotatedTerms[children] RPAREN + { atom = mkExpr(CVC4::APPLY,children); } + ; + +/** + * Matches an annotated term. + * @return the expression representing the term + */ +annotatedTerm returns [CVC4::Expr term] +{ + Kind kind; + Expr f, t1, t2; + vector children; +} + : term = baseTerm + | LPAREN f = functionSymbol + { children.push_back(f); } + annotatedTerms[children] RPAREN + { term = mkExpr(CVC4::APPLY, children); } + // | LPAREN kind = arithFunction annotatedTerms[children] RPAREN + // { term = mkExpr(kind,children); } + | LPAREN ITE + f = annotatedFormula + t1 = annotatedTerm + t2 = annotatedTerm RPAREN + { term = mkExpr(CVC4::ITE, f, t1, t2); } + ; + +/** + * Matches a sequence of annotaed formulas and puts them into the formulas + * vector. + * @param formulas the vector to fill with formulas + */ +annotatedTerms[std::vector& terms] +{ + Expr t; +} + : ( t = annotatedFormula { terms.push_back(t); } )+ + ; + +baseTerm returns [CVC4::Expr term] +{ + string name; +} + : name = identifier[CHECK_DECLARED] { term = getVariable(name); } + /* TODO: constants */ ; /** @@ -159,6 +246,8 @@ boolConnective returns [CVC4::Kind kind] ; /** +<<<<<<< .mine +======= * Mathces a sequence of annotaed formulas and puts them into the formulas * vector. * @param formulas the vector to fill with formulas @@ -171,6 +260,7 @@ annotatedFormulas[std::vector& formulas] ; /** +>>>>>>> .r150 * Matches a propositional atom and returns the expression of the atom. * @return atom the expression of the atom */ @@ -178,19 +268,62 @@ propositionalAtom returns [CVC4::Expr atom] { std::string p; } - : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); } + : atom = predicateSymbol | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; +arithPredicate returns [CVC4::Kind kind] + : EQUAL { kind = CVC4::EQUAL; } + /* TODO: lt, gt */ + ; + /** +<<<<<<< .mine + * Matches a (possibly undeclared) predicate identifier (returning the string). +======= * Matches a predicate symbol. +>>>>>>> .r150 * @param check what kind of check to do with the symbol */ predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p] : p = identifier[check] ; +<<<<<<< .mine + +/** + * Matches an previously declared predicate symbol (returning an Expr) + */ +predicateSymbol returns [CVC4::Expr pred] +{ + string name; +} + : name = predicateName[CHECK_DECLARED] + { pred = getVariable(name); } + ; + +/** + * Matches a (possibly undeclared) function identifier (returning the string) + * @param check what kind of check to do with the symbol + */ +functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name] + : name = identifier[check] + ; +/** + * Matches an previously declared function symbol (returning an Expr) + */ +functionSymbol returns [CVC4::Expr fun] +{ + string name; +} + : name = functionName[CHECK_DECLARED] + { fun = getVariable(name); } + ; + +======= + +>>>>>>> .r150 /** * Matches an attribute name from the input (:attribute_name). */ @@ -202,10 +335,32 @@ attribute * Matches the sort symbol, which can be an arbitrary identifier. * @param check the check to perform on the name */ +<<<<<<< .mine +sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] + : name = identifier[CHECK_NONE] + /* We pass CHECK_NONE to identifier, because identifier checks + in the variable namespace, not the sorts namespace. */ + { checkSort(name,check) }? +======= sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s] : s = identifier[check] +>>>>>>> .r150 ; +<<<<<<< .mine +functionDeclaration +{ + string name; + vector sorts; +} + : LPAREN name = functionName[CHECK_UNDECLARED] + sortNames[sorts, CHECK_DECLARED] RPAREN + { newFunction(name, sorts); } + ; + +======= + +>>>>>>> .r150 /** * Matches the declaration of a predicate and declares it */ @@ -214,17 +369,40 @@ predicateDeclaration string p_name; vector p_sorts; } +<<<<<<< .mine + : LPAREN p_name = predicateName[CHECK_UNDECLARED] + sortNames[p_sorts, CHECK_DECLARED] RPAREN + { newPredicate(p_name, p_sorts); } +======= : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } +>>>>>>> .r150 + ; +<<<<<<< .mine + +sortDeclaration +{ + string name; +} + : name = sortName[CHECK_UNDECLARED] + { newSort(name); } ; + +======= +>>>>>>> .r150 /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sortNames[std::vector& sorts] +sortNames[std::vector& sorts,DeclarationCheck check = CHECK_NONE] { - std::string sort; + std::string name; } +<<<<<<< .mine + : ( name = sortName[check] + { sorts.push_back(name); })* +======= : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* +>>>>>>> .r150 ; /** diff --git a/test/regress/simple-uf.smt b/test/regress/simple-uf.smt new file mode 100644 index 000000000..3aaba2ab0 --- /dev/null +++ b/test/regress/simple-uf.smt @@ -0,0 +1,7 @@ +(benchmark simple_uf + :logic QF_UF + :extrasorts (A B) + :extrafuns ((f A B) (x A) (y A)) + :formula (not (implies (= x y) (= (f x) (f y)))) + :status unsat +) -- 2.30.2