diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
commit | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch) | |
tree | 4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/parser | |
parent | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff) |
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 82 | ||||
-rw-r--r-- | src/parser/parser.h | 64 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 4 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 77 |
4 files changed, 140 insertions, 87 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 39f61c16d..297a2d804 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -66,11 +66,15 @@ Expr Parser::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } +Expr Parser::getFunction(const std::string& name) { + return getSymbol(name, SYM_VARIABLE); +} + Type Parser::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); - Type t = getSymbol(var_name,type).getType(); + Type t = getSymbol(var_name, type).getType(); return t; } @@ -83,8 +87,7 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope.lookupType(name); - Warning() << "FIXME use params to realize parameterized sort\n"; + Type t = d_declScope.lookupType(name, params); return t; } @@ -98,6 +101,11 @@ bool Parser::isFunction(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); } +/* Returns true if name is bound to a defined function. */ +bool Parser::isDefinedFunction(const std::string& name) { + return isFunction(name) && d_declScope.isBoundDefinedFunction(name); +} + /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); @@ -105,32 +113,54 @@ bool Parser::isPredicate(const std::string& name) { Expr Parser::mkVar(const std::string& name, const Type& type) { - Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); - defineVar(name,expr); + defineVar(name, expr); + return expr; +} + +Expr +Parser::mkFunction(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; + Expr expr = d_exprManager->mkVar(name, type); + defineFunction(name, expr); return expr; } const std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, - const Type& type) { + const Type& type) { std::vector<Expr> vars; for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i],type)); + vars.push_back(mkVar(names[i], type)); } return vars; } void Parser::defineVar(const std::string& name, const Expr& val) { - d_declScope.bind(name,val); - Assert(isDeclared(name)); + d_declScope.bind(name, val); + Assert( isDeclared(name) ); +} + +void +Parser::defineFunction(const std::string& name, const Expr& val) { + d_declScope.bindDefinedFunction(name, val); + Assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { - d_declScope.bindType(name,type); - Assert( isDeclared(name, SYM_SORT) ) ; + d_declScope.bindType(name, type); + Assert( isDeclared(name, SYM_SORT) ); +} + +void +Parser::defineType(const std::string& name, + const std::vector<Type>& params, + const Type& type) { + d_declScope.bindType(name, params, type); + Assert( isDeclared(name, SYM_SORT) ); } void @@ -139,20 +169,30 @@ Parser::defineParameterizedType(const std::string& name, const Type& type) { if(Debug.isOn("parser")) { Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", ["; - copy(params.begin(), params.end() - 1, - ostream_iterator<Type>(Debug("parser"), ", ") ); - Debug("parser") << params.back(); + if(params.size() > 0) { + copy(params.begin(), params.end() - 1, + ostream_iterator<Type>(Debug("parser"), ", ") ); + Debug("parser") << params.back(); + } Debug("parser") << "], " << type << ")" << std::endl; } - Warning("defineSort unimplemented\n"); - defineType(name,type); + defineType(name, params, type); +} + +Type +Parser::mkSort(const std::string& name) { + Debug("parser") << "newSort(" << name << ")" << std::endl; + Type type = d_exprManager->mkSort(name); + defineType(name, type); + return type; } Type -Parser::mkSort(const std::string& name, size_t arity) { - Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl; - Type type = d_exprManager->mkSort(name, arity); - defineType(name,type); +Parser::mkSortConstructor(const std::string& name, size_t arity) { + Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" + << std::endl; + Type type = d_exprManager->mkSortConstructor(name, arity); + defineType(name, vector<Type>(arity), type); return type; } @@ -239,7 +279,7 @@ void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserExcepti if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) { parseError( "Operator is not defined in the current logic: " + kindToString(kind) ); } - checkArity(kind,numArgs); + checkArity(kind, numArgs); } void Parser::addOperator(Kind kind) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 0faf9bebf..1c492c843 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -186,26 +186,21 @@ public: bool strictModeEnabled() { return d_strictMode; } - /** Get the name of the input file. */ -/* - inline const std::string getFilename() { - return d_filename; - } -*/ - /** - * Sets the logic for the current benchmark. Declares any logic symbols. + * Returns a variable, given a name. * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) + * @param name the name of the variable + * @return the variable expression */ -// void setLogic(const std::string& name); + Expr getVariable(const std::string& name); /** - * Returns a variable, given a name and a type. + * Returns a function, given a name. + * * @param var_name the name of the variable * @return the variable expression */ - Expr getVariable(const std::string& var_name); + Expr getFunction(const std::string& name); /** * Returns a sort, given a name. @@ -213,7 +208,7 @@ public: Type getSort(const std::string& sort_name); /** - * Returns a sort, given a name and args. + * Returns a (parameterized) sort, given a name and args. */ Type getSort(const std::string& sort_name, const std::vector<Type>& params); @@ -240,7 +235,8 @@ public: /** * Checks whether the given name is bound to a function. * @param name the name to check - * @throws ParserException if checks are enabled and name is not bound to a function + * @throws ParserException if checks are enabled and name is not + * bound to a function */ void checkFunction(const std::string& name) throw (ParserException); @@ -248,23 +244,26 @@ public: * Check that <code>kind</code> can accept <code>numArgs</code> arguments. * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be - * applied to <code>numArgs</code> arguments. + * @throws ParserException if checks are enabled and the operator + * <code>kind</code> cannot be applied to <code>numArgs</code> + * arguments. */ void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); - /** Check that <code>kind</code> is a legal operator in the current logic and - * that it can accept <code>numArgs</code> arguments. + /** + * Check that <code>kind</code> is a legal operator in the current + * logic and that it can accept <code>numArgs</code> arguments. * * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws ParserException if the parser mode is strict and the operator <code>kind</kind> - * has not been enabled + * @throws ParserException if the parser mode is strict and the + * operator <code>kind</kind> has not been enabled */ void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); /** * Returns the type for the variable with the given name. + * * @param var_name the symbol to lookup * @param type the (namespace) type of the symbol */ @@ -274,27 +273,41 @@ public: Expr mkVar(const std::string& name, const Type& type); /** - * Create a set of new CVC4 variable expressions of the given - * type. + * Create a set of new CVC4 variable expressions of the given type. */ const std::vector<Expr> mkVars(const std::vector<std::string> names, const Type& type); + /** Create a new CVC4 function expression of the given type. */ + Expr mkFunction(const std::string& name, const Type& type); + /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); + /** Create a new function definition (e.g., from a define-fun). */ + void defineFunction(const std::string& name, const Expr& val); + /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); + /** Create a new (parameterized) type definition. */ + void defineType(const std::string& name, + const std::vector<Type>& params, const Type& type); + /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ void defineParameterizedType(const std::string& name, const std::vector<Type>& params, const Type& type); /** - * Creates a new sort with the given name and arity. + * Creates a new sort with the given name. + */ + Type mkSort(const std::string& name); + + /** + * Creates a new sort constructor with the given name and arity. */ - Type mkSort(const std::string& name, size_t arity = 0); + Type mkSortConstructor(const std::string& name, size_t arity); /** * Creates new sorts with the given names (all of arity 0). @@ -314,6 +327,9 @@ public: /** Is the symbol bound to a function? */ bool isFunction(const std::string& name); + /** Is the symbol bound to a defined function? */ + bool isDefinedFunction(const std::string& name); + /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index da352c226..7ff738dd7 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -85,8 +85,8 @@ void Smt::addTheory(Theory theory) { case THEORY_ARRAYS_EX: { Type indexType = mkSort("Index"); Type elementType = mkSort("Element"); - - defineType("Array",getExprManager()->mkArrayType(indexType,elementType)); + + defineType("Array", getExprManager()->mkArrayType(indexType,elementType)); addOperator(kind::SELECT); addOperator(kind::STORE); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4c742adfc..9ad8c3177 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -19,8 +19,8 @@ grammar Smt2; options { - language = 'C'; // C output for antlr -// defaultErrorHandler = false; // Skip the default error handling, just break with exceptions + language = 'C'; // C output for antlr + //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions k = 2; } @@ -162,8 +162,15 @@ command returns [CVC4::Command* cmd] DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; - PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n)); - $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); } + unsigned arity = AntlrInput::tokenToUnsigned(n); + if(arity == 0) { + PARSER_STATE->mkSort(name); + $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType()); + } else { + PARSER_STATE->mkSortConstructor(name, arity); + $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType()); + } + } | /* sort definition */ DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK @@ -223,8 +230,8 @@ command returns [CVC4::Command* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - PARSER_STATE->mkVar(name, t); - $cmd = new DefineFunctionCommand(name,sortedVars,t,expr); + PARSER_STATE->mkFunction(name, t); + $cmd = new DefineFunctionCommand(name, sortedVars, t, expr); } | /* value query */ GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -315,22 +322,18 @@ term[CVC4::Expr& expr] | /* A non-built-in function application */ LPAREN_TOK - functionSymbol[expr] - { args.push_back(expr); } + functionName[name,CHECK_DECLARED] + { args.push_back(Expr()); } termList[args,expr] RPAREN_TOK - // TODO: check arity - { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } - - // | /* An ite expression */ - // LPAREN_TOK ITE_TOK - // term[expr] - // { args.push_back(expr); } - // term[expr] - // { args.push_back(expr); } - // term[expr] - // { args.push_back(expr); } - // RPAREN_TOK - // { expr = MK_EXPR(CVC4::kind::ITE, args); } + { PARSER_STATE->checkFunction(name); + const bool isDefinedFunction = + PARSER_STATE->isDefinedFunction(name); + expr = isDefinedFunction ? + PARSER_STATE->getFunction(name) : + PARSER_STATE->getVariable(name); + args[0] = expr; + // TODO: check arity + expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); } | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK @@ -479,7 +482,7 @@ sortSymbol[CVC4::Type& t] } t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); } else { - PARSER_STATE->parseError("Unhandled parameterized type."); + t = PARSER_STATE->getSort(name, args); } } ; @@ -516,9 +519,7 @@ symbol[std::string& id, // Base SMT-LIB tokens ASSERT_TOK : 'assert'; -//CATEGORY_TOK : ':category'; CHECKSAT_TOK : 'check-sat'; -//DIFFICULTY_TOK : ':difficulty'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; @@ -526,23 +527,15 @@ DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; -//FALSE_TOK : 'false'; ITE_TOK : 'ite'; LET_TOK : 'let'; LPAREN_TOK : '('; -//NOTES_TOK : ':notes'; RPAREN_TOK : ')'; -//SAT_TOK : 'sat'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; +GET_INFO_TOK : 'get-info'; SET_OPTION_TOK : 'set-option'; GET_OPTION_TOK : 'get-option'; -//SMT_VERSION_TOK : ':smt-lib-version'; -//SOURCE_TOK : ':source'; -//STATUS_TOK : ':status'; -//TRUE_TOK : 'true'; -//UNKNOWN_TOK : 'unknown'; -//UNSAT_TOK : 'unsat'; // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; @@ -605,15 +598,18 @@ WHITESPACE ; /** - * Matches an integer constant from the input (non-empty sequence of digits, with - * no leading zeroes). + * Matches an integer constant from the input (non-empty sequence of + * digits, with no leading zeroes). */ INTEGER_LITERAL : NUMERAL ; -/** Match an integer constant. In non-strict mode, this is any sequence of - * digits. In strict mode, non-zero integers can't have leading zeroes. */ +/** + * Match an integer constant. In non-strict mode, this is any sequence + * of digits. In strict mode, non-zero integers can't have leading + * zeroes. + */ fragment NUMERAL @init { char *start = (char*) GETCHARINDEX(); @@ -631,8 +627,8 @@ fragment NUMERAL ; /** - * Matches a decimal constant from the input. - */ + * Matches a decimal constant from the input. + */ DECIMAL_LITERAL : NUMERAL '.' DIGIT+ ; @@ -684,7 +680,8 @@ fragment DIGIT : '0'..'9'; fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; -/** Matches the characters that may appear in a "symbol" (i.e., an identifier) +/** + * Matches the characters that may appear in a "symbol" (i.e., an identifier) */ fragment SYMBOL_CHAR : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' |