From 831feca5415d7da807542cb1820909f09675b31b Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 4 Mar 2014 22:16:21 -0500 Subject: [PATCH] Don't tokenize SET_THEORY operators in smt2 parser --- src/parser/parser.cpp | 6 +- src/parser/smt2/Smt2.g | 106 ++++++---------- src/parser/smt2/smt2.cpp | 219 ++++++++++++++++++++------------ src/parser/smt2/smt2.h | 13 +- test/regress/regress0/error.cvc | 2 +- 5 files changed, 197 insertions(+), 149 deletions(-) diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d65a68310..c3019966a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -377,7 +377,7 @@ void Parser::checkDeclaration(const std::string& varName, switch(check) { case CHECK_DECLARED: if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared as a " + + parseError("Symbol '" + varName + "' not declared as a " + (type == SYM_VARIABLE ? "variable" : "type") + (notes.size() == 0 ? notes : "\n" + notes)); } @@ -385,7 +385,7 @@ void Parser::checkDeclaration(const std::string& varName, case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared as a " + + parseError("Symbol '" + varName + "' previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type") + (notes.size() == 0 ? notes : "\n" + notes)); } @@ -491,7 +491,7 @@ Expr Parser::nextExpression() throw(ParserException) { void Parser::attributeNotSupported(const std::string& attr) { if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) { stringstream ss; - ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)"; + ss << "warning: Attribute '" << attr << "' not supported (ignoring this and all following uses)"; d_input->warning(ss.str()); d_attributesWarnedAbout.insert(attr); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6e9f04ce9..f1acac6ba 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -770,6 +770,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::vector< std::pair > binders; Type type; std::string s; + bool isBuiltinOperator = false; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -835,7 +836,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else if(f.getKind() == CVC4::kind::EMPTYSET) { Debug("parser") << "Empty set encountered: " << f << " " << f2 << " " << type << std::endl; - // TODO: what is f2 about, should we add some assertions? expr = MK_CONST( ::CVC4::EmptySet(type) ); } else { if(f.getType() != type) { @@ -879,34 +879,44 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - | /* A non-built-in function application */ - LPAREN_TOK - functionName[name, CHECK_DECLARED] - { PARSER_STATE->checkFunctionLike(name); - const bool isDefinedFunction = - PARSER_STATE->isDefinedFunction(name); - if(isDefinedFunction) { - expr = PARSER_STATE->getFunction(name); - kind = CVC4::kind::APPLY; + | LPAREN_TOK functionName[name, CHECK_NONE] + { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); + if(isBuiltinOperator) { + /* A built-in operator not already handled by the lexer */ + kind = PARSER_STATE->getOperatorKind(name); } else { - expr = PARSER_STATE->getVariable(name); - Type t = expr.getType(); - if(t.isConstructor()) { - kind = CVC4::kind::APPLY_CONSTRUCTOR; - } else if(t.isSelector()) { - kind = CVC4::kind::APPLY_SELECTOR; - } else if(t.isTester()) { - kind = CVC4::kind::APPLY_TESTER; + /* A non-built-in function application */ + PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE); + PARSER_STATE->checkFunctionLike(name); + const bool isDefinedFunction = + PARSER_STATE->isDefinedFunction(name); + if(isDefinedFunction) { + expr = PARSER_STATE->getFunction(name); + kind = CVC4::kind::APPLY; } else { - kind = CVC4::kind::APPLY_UF; + expr = PARSER_STATE->getVariable(name); + Type t = expr.getType(); + if(t.isConstructor()) { + kind = CVC4::kind::APPLY_CONSTRUCTOR; + } else if(t.isSelector()) { + kind = CVC4::kind::APPLY_SELECTOR; + } else if(t.isTester()) { + kind = CVC4::kind::APPLY_TESTER; + } else { + kind = CVC4::kind::APPLY_UF; + } } + args.push_back(expr); } - args.push_back(expr); - } + } termList[args,expr] RPAREN_TOK { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl; - for(std::vector::iterator i = args.begin(); i != args.end(); ++i) + for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { Debug("parser") << "++ " << *i << std::endl; + } + if(isBuiltinOperator) { + PARSER_STATE->checkOperator(kind, args.size()); + } expr = MK_EXPR(kind, args); } | /* An indexed function application */ @@ -1283,14 +1293,6 @@ builtinOp[CVC4::Kind& kind] if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); } } - //NEW string - //STRCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; } - //STRREVCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; } - //STRHEAD_TOK { $kind = CVC4::kind::STRING_CONCAT; } - //STRTAIL_TOK { $kind = CVC4::kind::STRING_CONCAT; } - //STRLAST_TOK { $kind = CVC4::kind::STRING_CONCAT; } - //STRFIRST_TOK { $kind = CVC4::kind::STRING_CONCAT; } - //OLD string | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } @@ -1311,12 +1313,6 @@ builtinOp[CVC4::Kind& kind] | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; } | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } - | SETUNION_TOK { $kind = CVC4::kind::UNION; } - | SETINT_TOK { $kind = CVC4::kind::INTERSECTION; } - | SETMINUS_TOK { $kind = CVC4::kind::SETMINUS; } - | SETSUB_TOK { $kind = CVC4::kind::SUBSET; } - | SETIN_TOK { $kind = CVC4::kind::MEMBER; } - | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; } // NOTE: Theory operators go here ; @@ -1337,18 +1333,6 @@ functionName[std::string& name, CVC4::parser::DeclarationCheck check] : symbol[name,check,SYM_VARIABLE] ; -/** - * Matches an previously declared function symbol (returning an Expr) - */ -functionSymbol[CVC4::Expr& fun] -@declarations { - std::string name; -} - : functionName[name,CHECK_DECLARED] - { PARSER_STATE->checkFunctionLike(name); - fun = PARSER_STATE->getVariable(name); } - ; - /** * Matches a sequence of sort symbols and fills them into the given * vector. @@ -1421,12 +1405,14 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK { - if(name == "Array") { + if(name == "Array" && + PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) { if(args.size() != 2) { PARSER_STATE->parseError("Illegal array type."); } t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); - } else if(name == "Set") { + } else if(name == "Set" && + PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) { if(args.size() != 1) { PARSER_STATE->parseError("Illegal set type."); } @@ -1682,15 +1668,6 @@ BVSGE_TOK : 'bvsge'; BV2NAT_TOK : 'bv2nat'; INT2BV_TOK : 'int2bv'; -//STRING -//NEW -//STRCONS_TOK : 'str.cons'; -//STRREVCONS_TOK : 'str.revcons'; -//STRHEAD_TOK : 'str.head'; -//STRTAIL_TOK : 'str.tail'; -//STRLAST_TOK : 'str.last'; -//STRFIRST_TOK : 'str.first'; -//OLD STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; STRSUB_TOK : 'str.substr' ; @@ -1714,13 +1691,10 @@ RERANGE_TOK : 're.range'; RENOSTR_TOK : 're.nostr'; REALLCHAR_TOK : 're.allchar'; -SETUNION_TOK: 'union'; -SETINT_TOK: 'intersection'; -SETMINUS_TOK: 'setminus'; -SETSUB_TOK: 'subseteq'; -SETIN_TOK: 'in'; -SETSINGLETON_TOK: 'setenum'; -EMPTYSET_TOK: 'emptyset'; +EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not + // tokenized and handled directly when + // processing a term + /** * A sequence of printable ASCII characters (except backslash) that starts diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b1621e9e5..b59880a5e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -37,111 +37,121 @@ Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn } void Smt2::addArithmeticOperators() { - addOperator(kind::PLUS); - addOperator(kind::MINUS); - addOperator(kind::UMINUS); - addOperator(kind::MULT); - addOperator(kind::LT); - addOperator(kind::LEQ); - addOperator(kind::GT); - addOperator(kind::GEQ); + Parser::addOperator(kind::PLUS); + Parser::addOperator(kind::MINUS); + Parser::addOperator(kind::UMINUS); + Parser::addOperator(kind::MULT); + Parser::addOperator(kind::LT); + Parser::addOperator(kind::LEQ); + Parser::addOperator(kind::GT); + Parser::addOperator(kind::GEQ); } void Smt2::addBitvectorOperators() { - addOperator(kind::BITVECTOR_CONCAT); - addOperator(kind::BITVECTOR_AND); - addOperator(kind::BITVECTOR_OR); - addOperator(kind::BITVECTOR_XOR); - addOperator(kind::BITVECTOR_NOT); - addOperator(kind::BITVECTOR_NAND); - addOperator(kind::BITVECTOR_NOR); - addOperator(kind::BITVECTOR_XNOR); - addOperator(kind::BITVECTOR_COMP); - addOperator(kind::BITVECTOR_MULT); - addOperator(kind::BITVECTOR_PLUS); - addOperator(kind::BITVECTOR_SUB); - addOperator(kind::BITVECTOR_NEG); - addOperator(kind::BITVECTOR_UDIV); - addOperator(kind::BITVECTOR_UREM); - addOperator(kind::BITVECTOR_SDIV); - addOperator(kind::BITVECTOR_SREM); - addOperator(kind::BITVECTOR_SMOD); - addOperator(kind::BITVECTOR_SHL); - addOperator(kind::BITVECTOR_LSHR); - addOperator(kind::BITVECTOR_ASHR); - addOperator(kind::BITVECTOR_ULT); - addOperator(kind::BITVECTOR_ULE); - addOperator(kind::BITVECTOR_UGT); - addOperator(kind::BITVECTOR_UGE); - addOperator(kind::BITVECTOR_SLT); - addOperator(kind::BITVECTOR_SLE); - addOperator(kind::BITVECTOR_SGT); - addOperator(kind::BITVECTOR_SGE); - addOperator(kind::BITVECTOR_BITOF); - addOperator(kind::BITVECTOR_EXTRACT); - addOperator(kind::BITVECTOR_REPEAT); - addOperator(kind::BITVECTOR_ZERO_EXTEND); - addOperator(kind::BITVECTOR_SIGN_EXTEND); - addOperator(kind::BITVECTOR_ROTATE_LEFT); - addOperator(kind::BITVECTOR_ROTATE_RIGHT); - - addOperator(kind::INT_TO_BITVECTOR); - addOperator(kind::BITVECTOR_TO_NAT); + Parser::addOperator(kind::BITVECTOR_CONCAT); + Parser::addOperator(kind::BITVECTOR_AND); + Parser::addOperator(kind::BITVECTOR_OR); + Parser::addOperator(kind::BITVECTOR_XOR); + Parser::addOperator(kind::BITVECTOR_NOT); + Parser::addOperator(kind::BITVECTOR_NAND); + Parser::addOperator(kind::BITVECTOR_NOR); + Parser::addOperator(kind::BITVECTOR_XNOR); + Parser::addOperator(kind::BITVECTOR_COMP); + Parser::addOperator(kind::BITVECTOR_MULT); + Parser::addOperator(kind::BITVECTOR_PLUS); + Parser::addOperator(kind::BITVECTOR_SUB); + Parser::addOperator(kind::BITVECTOR_NEG); + Parser::addOperator(kind::BITVECTOR_UDIV); + Parser::addOperator(kind::BITVECTOR_UREM); + Parser::addOperator(kind::BITVECTOR_SDIV); + Parser::addOperator(kind::BITVECTOR_SREM); + Parser::addOperator(kind::BITVECTOR_SMOD); + Parser::addOperator(kind::BITVECTOR_SHL); + Parser::addOperator(kind::BITVECTOR_LSHR); + Parser::addOperator(kind::BITVECTOR_ASHR); + Parser::addOperator(kind::BITVECTOR_ULT); + Parser::addOperator(kind::BITVECTOR_ULE); + Parser::addOperator(kind::BITVECTOR_UGT); + Parser::addOperator(kind::BITVECTOR_UGE); + Parser::addOperator(kind::BITVECTOR_SLT); + Parser::addOperator(kind::BITVECTOR_SLE); + Parser::addOperator(kind::BITVECTOR_SGT); + Parser::addOperator(kind::BITVECTOR_SGE); + Parser::addOperator(kind::BITVECTOR_BITOF); + Parser::addOperator(kind::BITVECTOR_EXTRACT); + Parser::addOperator(kind::BITVECTOR_REPEAT); + Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND); + Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND); + Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT); + Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT); + + Parser::addOperator(kind::INT_TO_BITVECTOR); + Parser::addOperator(kind::BITVECTOR_TO_NAT); } void Smt2::addStringOperators() { - addOperator(kind::STRING_CONCAT); - addOperator(kind::STRING_LENGTH); - //addOperator(kind::STRING_IN_REGEXP); + Parser::addOperator(kind::STRING_CONCAT); + Parser::addOperator(kind::STRING_LENGTH); } void Smt2::addTheory(Theory theory) { switch(theory) { + case THEORY_ARRAYS: + Parser::addOperator(kind::SELECT); + Parser::addOperator(kind::STORE); + break; + + case THEORY_BITVECTORS: + addBitvectorOperators(); + break; + case THEORY_CORE: defineType("Bool", getExprManager()->booleanType()); defineVar("true", getExprManager()->mkConst(true)); defineVar("false", getExprManager()->mkConst(false)); - addOperator(kind::AND); - addOperator(kind::DISTINCT); - addOperator(kind::EQUAL); - addOperator(kind::IFF); - addOperator(kind::IMPLIES); - addOperator(kind::ITE); - addOperator(kind::NOT); - addOperator(kind::OR); - addOperator(kind::XOR); - break; - - case THEORY_ARRAYS: - addOperator(kind::SELECT); - addOperator(kind::STORE); + Parser::addOperator(kind::AND); + Parser::addOperator(kind::DISTINCT); + Parser::addOperator(kind::EQUAL); + Parser::addOperator(kind::IFF); + Parser::addOperator(kind::IMPLIES); + Parser::addOperator(kind::ITE); + Parser::addOperator(kind::NOT); + Parser::addOperator(kind::OR); + Parser::addOperator(kind::XOR); break; case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); - addOperator(kind::DIVISION); - addOperator(kind::TO_INTEGER); - addOperator(kind::IS_INTEGER); - addOperator(kind::TO_REAL); + Parser::addOperator(kind::DIVISION); + Parser::addOperator(kind::TO_INTEGER); + Parser::addOperator(kind::IS_INTEGER); + Parser::addOperator(kind::TO_REAL); // falling through on purpose, to add Ints part of Reals_Ints - case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); - addOperator(kind::INTS_DIVISION); - addOperator(kind::INTS_MODULUS); - addOperator(kind::ABS); - addOperator(kind::DIVISIBLE); + Parser::addOperator(kind::INTS_DIVISION); + Parser::addOperator(kind::INTS_MODULUS); + Parser::addOperator(kind::ABS); + Parser::addOperator(kind::DIVISIBLE); break; case THEORY_REALS: defineType("Real", getExprManager()->realType()); addArithmeticOperators(); - addOperator(kind::DIVISION); + Parser::addOperator(kind::DIVISION); break; - case THEORY_BITVECTORS: - addBitvectorOperators(); + case THEORY_QUANTIFIERS: + break; + + case THEORY_SETS: + addOperator(kind::UNION, "union"); + addOperator(kind::INTERSECTION, "intersection"); + addOperator(kind::SETMINUS, "setminus"); + addOperator(kind::SUBSET, "subseteq"); + addOperator(kind::MEMBER, "in"); + addOperator(kind::SET_SINGLETON, "setenum"); break; case THEORY_STRINGS: @@ -149,7 +159,8 @@ void Smt2::addTheory(Theory theory) { addStringOperators(); break; - case THEORY_QUANTIFIERS: + case THEORY_UF: + Parser::addOperator(kind::APPLY_UF); break; default: @@ -159,6 +170,54 @@ void Smt2::addTheory(Theory theory) { } } +void Smt2::addOperator(Kind kind, const std::string& name) { + Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" + << std::endl; + Parser::addOperator(kind); + operatorKindMap[name] = kind; +} + +Kind Smt2::getOperatorKind(const std::string& name) const { + // precondition: isOperatorEnabled(name) + return operatorKindMap.find(name)->second; +} + +bool Smt2::isOperatorEnabled(const std::string& name) const { + return operatorKindMap.find(name) != operatorKindMap.end(); +} + +bool Smt2::isTheoryEnabled(Theory theory) const { + switch(theory) { + case THEORY_ARRAYS: + return d_logic.isTheoryEnabled(theory::THEORY_ARRAY); + case THEORY_BITVECTORS: + return d_logic.isTheoryEnabled(theory::THEORY_BV); + case THEORY_CORE: + return true; + case THEORY_INTS: + return d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() ); + case THEORY_REALS: + return d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed(); + case THEORY_REALS_INTS: + return d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + d_logic.areIntegersUsed() && d_logic.areRealsUsed(); + case THEORY_QUANTIFIERS: + return d_logic.isQuantified(); + case THEORY_SETS: + return d_logic.isTheoryEnabled(theory::THEORY_SETS); + case THEORY_STRINGS: + return d_logic.isTheoryEnabled(theory::THEORY_STRINGS); + case THEORY_UF: + return d_logic.isTheoryEnabled(theory::THEORY_UF); + default: + std::stringstream ss; + ss << "internal error: unsupported theory " << theory; + throw ParserException(ss.str()); + } +} + bool Smt2::logicIsSet() { return d_logicSet; } @@ -171,7 +230,7 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_CORE); if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { - addOperator(kind::APPLY_UF); + addTheory(THEORY_UF); } if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { @@ -194,6 +253,10 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); } + if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) { + addTheory(THEORY_SETS); + } + if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { addTheory(THEORY_STRINGS); } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 837adb15c..969892c5f 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -44,12 +44,15 @@ public: THEORY_REALS, THEORY_REALS_INTS, THEORY_QUANTIFIERS, - THEORY_STRINGS + THEORY_SETS, + THEORY_STRINGS, + THEORY_UF }; private: bool d_logicSet; LogicInfo d_logic; + std::hash_map operatorKindMap; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -62,6 +65,14 @@ public: */ void addTheory(Theory theory); + void addOperator(Kind k, const std::string& name); + + Kind getOperatorKind(const std::string& name) const; + + bool isOperatorEnabled(const std::string& name) const; + + bool isTheoryEnabled(Theory theory) const; + bool logicIsSet(); /** diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index 6d1641092..dd3db0fdd 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,4 +1,4 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: error.cvc:3.8: Symbol BOOL not declared as a type +% EXPECT-ERROR: Parse Error: error.cvc:3.8: Symbol 'BOOL' not declared as a type p : BOOL; % EXIT: 1 -- 2.30.2