From c83ce8f341f88bbffcae8fd2bfbed5c33abf4f66 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 12 Jun 2019 09:07:00 -0700 Subject: [PATCH] Refactor parser to define fewer tokens for symbols (#2936) --- src/expr/symbol_table.cpp | 2 +- src/parser/parser.cpp | 6 +- src/parser/parser.h | 6 +- src/parser/smt2/Smt2.g | 475 ++++-------------- src/parser/smt2/smt2.cpp | 266 ++++++++-- src/parser/smt2/smt2.h | 153 ++++-- .../regress0/bv/core/constant_core.smt2 | 2 +- test/regress/regress0/expect/scrub.08.sy | 2 +- test/regress/regress0/nl/nta/real-pi.smt2 | 2 +- test/regress/regress0/strings/bug613.smt2 | 2 +- test/regress/regress0/strings/str004.smt2 | 2 +- test/regress/regress0/strings/type001.smt2 | 2 +- .../regress0/strings/unsound-0908.smt2 | 2 +- .../strings/artemis-0512-nonterm.smt2 | 2 +- test/regress/regress1/strings/at001.smt2 | 2 +- test/regress/regress1/strings/fmf002.smt2 | 2 +- .../regress1/strings/issue2429-code.smt2 | 2 +- test/regress/regress1/strings/kaluza-fl.smt2 | 2 +- test/regress/regress1/strings/loop005.smt2 | 2 +- test/regress/regress1/strings/loop007.smt2 | 2 +- test/regress/regress1/strings/loop008.smt2 | 2 +- .../regress1/strings/re-agg-total1.smt2 | 2 +- test/regress/regress1/strings/reloop.smt2 | 2 +- test/regress/regress1/strings/substr001.smt2 | 2 +- test/regress/regress1/strings/type002.smt2 | 2 +- test/regress/regress1/strings/type003.smt2 | 2 +- test/unit/parser/parser_black.h | 6 + 27 files changed, 459 insertions(+), 495 deletions(-) diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 600f666bc..dd75170b5 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -456,7 +456,7 @@ bool SymbolTable::Implementation::isBound(const string& name) const { bool SymbolTable::Implementation::isBoundDefinedFunction( const string& name) const { - CDHashMap::iterator found = d_exprMap->find(name); + CDHashMap::const_iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 28489154a..5e036ee69 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -47,8 +47,7 @@ Parser::Parser(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) - : d_solver(solver), - d_resourceManager(d_solver->getExprManager()->getResourceManager()), + : d_resourceManager(solver->getExprManager()->getResourceManager()), d_input(input), d_symtabAllocated(), d_symtab(&d_symtabAllocated), @@ -61,7 +60,8 @@ Parser::Parser(api::Solver* solver, d_parseOnly(parseOnly), d_canIncludeFile(true), d_logicIsForced(false), - d_forcedLogic() + d_forcedLogic(), + d_solver(solver) { d_input->setParser(*this); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 826d460b2..fcc37d5d3 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -137,9 +137,6 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { class CVC4_PUBLIC Parser { friend class ParserBuilder; private: - /** The API Solver object. */ - api::Solver* d_solver; - /** The resource manager associated with this expr manager */ ResourceManager* d_resourceManager; @@ -244,6 +241,9 @@ private: Expr getSymbol(const std::string& var_name, SymbolType type); protected: + /** The API Solver object. */ + api::Solver* d_solver; + /** * Create a parser state. * diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b224032e8..4a30841e6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -891,14 +891,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] } : LPAREN_TOK //read operator - ( builtinOp[k]{ - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " - << name << std::endl; - sgt.d_name = kind::kindToString(k); - sgt.d_gterm_type = SygusGTerm::gterm_op; - sgt.d_expr = EXPR_MANAGER->operatorOf(k); - } - | SYGUS_LET_TOK LPAREN_TOK { + ( SYGUS_LET_TOK LPAREN_TOK { sgt.d_name = std::string("let"); sgt.d_gterm_type = SygusGTerm::gterm_let; PARSER_STATE->pushScope(true); @@ -1645,12 +1638,6 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } - | builtinOp[k] - { std::stringstream ss; - ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) - << EXPR_MANAGER->mkConst(k); - sexpr = SExpr(ss.str()); - } ; keyword[std::string& s] @@ -1700,10 +1687,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind = kind::NULL_EXPR; Expr op; - std::string name, name2; + std::string name; std::vector args; std::vector< std::pair > sortedVarNames; - Expr f, f2, f3, f4; + Expr f, f2, f3; std::string attr; Expr attexpr; std::vector patexprs; @@ -1719,49 +1706,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Type type2; api::Term atomTerm; } - : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK - { - if( !PARSER_STATE->strictModeEnabled() && - (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && - args.size() == 1) { - /* Unary AND/OR can be replaced with the argument. - * It just so happens expr should already be the only argument. */ - assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && - args.size() > EXPR_MANAGER->maxArity(kind) ) { - /* Special treatment for associative operators with lots of children */ - expr = EXPR_MANAGER->mkAssociative(kind, args); - } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) { - expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); - } - else if ((kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS - || kind == CVC4::kind::DIVISION) - && args.size() > 2) - { - /* left-associative, but CVC4 internally only supports 2 args */ - expr = EXPR_MANAGER->mkLeftAssociative(kind,args); - } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) { - /* right-associative, but CVC4 internally only supports 2 args */ - expr = EXPR_MANAGER->mkRightAssociative(kind,args); - } else if( ( kind == CVC4::kind::EQUAL || - kind == CVC4::kind::LT || kind == CVC4::kind::GT || - kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) && - args.size() > 2 ) { - /* "chainable", but CVC4 internally only supports 2 args */ - expr = MK_EXPR(MK_CONST(Chain(kind)), args); - } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS && - args.size() == 1 && !args[0].getType().isInteger() ) { - /* first, check that ABS is even defined in this logic */ - PARSER_STATE->checkOperator(kind, args.size()); - PARSER_STATE->parseError("abs can only be applied to Int, not Real, " - "while in strict SMT-LIB compliance mode"); - } else { - PARSER_STATE->checkOperator(kind, args.size()); - expr = MK_EXPR(kind, args); - } - } - | LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } ) + : LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } ) sortSymbol[type, CHECK_DECLARED] RPAREN_TOK { if(readVariable) { @@ -1843,7 +1788,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] | LPAREN_TOK functionName[name, CHECK_NONE] { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); if(isBuiltinOperator) { - /* A built-in operator not already handled by the lexer */ + /* A built-in operator */ kind = PARSER_STATE->getOperatorKind(name); } else { /* A non-built-in function application */ @@ -1883,17 +1828,69 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types."); } } - Kind lassocKind = CVC4::kind::UNDEFINED_KIND; - if (args.size() >= 2) + + bool done = false; + if (isBuiltinOperator) { - if (kind == CVC4::kind::INTS_DIVISION - || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6())) + if (args.size() > 2) { - // Builtin operators that are not tokenized, are left associative, - // but not internally variadic must set this. - lassocKind = kind; + if (kind == CVC4::kind::INTS_DIVISION || kind == CVC4::kind::XOR + || kind == CVC4::kind::MINUS || kind == CVC4::kind::DIVISION + || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6())) + { + // Builtin operators that are not tokenized, are left associative, + // but not internally variadic must set this. + expr = + EXPR_MANAGER->mkLeftAssociative(kind, args); + done = true; + } + else if (kind == CVC4::kind::IMPLIES) + { + /* right-associative, but CVC4 internally only supports 2 args */ + expr = EXPR_MANAGER->mkRightAssociative(kind, args); + done = true; + } + else if (kind == CVC4::kind::EQUAL || kind == CVC4::kind::LT + || kind == CVC4::kind::GT || kind == CVC4::kind::LEQ + || kind == CVC4::kind::GEQ) + { + /* "chainable", but CVC4 internally only supports 2 args */ + expr = MK_EXPR(MK_CONST(Chain(kind)), args); + done = true; + } + } + + if (!done) + { + if (CVC4::kind::isAssociative(kind) + && args.size() > EXPR_MANAGER->maxArity(kind)) + { + /* Special treatment for associative operators with lots of children + */ + expr = EXPR_MANAGER->mkAssociative(kind, args); + } + else if (!PARSER_STATE->strictModeEnabled() + && (kind == CVC4::kind::AND || kind == CVC4::kind::OR) + && args.size() == 1) + { + /* Unary AND/OR can be replaced with the argument. + * It just so happens expr should already be the only argument. */ + assert(expr == args[0]); + } + else if (kind == CVC4::kind::MINUS && args.size() == 1) + { + expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); + } + else + { + PARSER_STATE->checkOperator(kind, args.size()); + expr = MK_EXPR(kind, args); + } } - else + } + else + { + if (args.size() >= 2) { // may be partially applied function, in this case we use HO_APPLY Type argt = args[0].getType(); @@ -1906,22 +1903,17 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Debug("parser") << " : #argTypes = " << arity; Debug("parser") << ", #args = " << args.size() - 1 << std::endl; // must curry the partial application - lassocKind = CVC4::kind::HO_APPLY; + expr = + EXPR_MANAGER->mkLeftAssociative(CVC4::kind::HO_APPLY, args); + done = true; } } } - } - if (lassocKind != CVC4::kind::UNDEFINED_KIND) - { - expr = EXPR_MANAGER->mkLeftAssociative(lassocKind, args); - } - else - { - if (isBuiltinOperator) + + if (!done) { - PARSER_STATE->checkOperator(kind, args.size()); + expr = MK_EXPR(kind, args); } - expr = MK_EXPR(kind, args); } } | LPAREN_TOK @@ -2023,9 +2015,11 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } binders.push_back(std::make_pair(name, expr)); } )+ ) { // now implement these bindings - for(std::vector< std::pair >::iterator - i = binders.begin(); i != binders.end(); ++i) { - PARSER_STATE->defineVar((*i).first, (*i).second); + for (const std::pair& binder : binders) + { + { + PARSER_STATE->defineVar(binder.first, binder.second); + } } } RPAREN_TOK @@ -2240,6 +2234,7 @@ termAtomic[CVC4::api::Term& atomTerm] Type type; Type type2; std::string s; + std::vector numerals; } /* constants */ : INTEGER_LITERAL @@ -2254,65 +2249,24 @@ termAtomic[CVC4::api::Term& atomTerm] SOLVER->getRealSort()); } - // Pi constant - | REAL_PI_TOK { atomTerm = SOLVER->mkPi(); } - // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity // as a 32-bit floating-point constant) | LPAREN_TOK INDEX_TOK - ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL - { - if(AntlrInput::tokenText($bvLit).find("bv") == 0) - { - std::string bvStr = AntlrInput::tokenTextSubstr($bvLit, 2); - uint32_t bvSize = AntlrInput::tokenToUnsigned($size); - atomTerm = SOLVER->mkBitVector(bvSize, bvStr, 10); - } - else - { - PARSER_STATE->parseError("Unexpected symbol `" + - AntlrInput::tokenText($bvLit) + "'"); - } - } - - // Floating-point constants - | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { - atomTerm = SOLVER->mkPosInf(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)); - } - | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { - atomTerm = SOLVER->mkNegInf(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)); - } - | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { - atomTerm = SOLVER->mkNaN(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)); - } - | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { - atomTerm = SOLVER->mkPosZero(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)); - } - | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { - atomTerm = SOLVER->mkNegZero(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)); - } - - // Empty heap constant in seperation logic - | EMP_TOK + ( EMP_TOK sortSymbol[type,CHECK_DECLARED] sortSymbol[type2,CHECK_DECLARED] { + // Empty heap constant in seperation logic api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1"); api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2"); atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } - - // NOTE: Theory parametric constants go here + | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] + { + atomTerm = + PARSER_STATE->mkIndexedConstant(AntlrInput::tokenText($sym), + numerals); + } ) RPAREN_TOK @@ -2330,42 +2284,9 @@ termAtomic[CVC4::api::Term& atomTerm] atomTerm = SOLVER->mkBitVector(binStr, 2); } - // Floating-point rounding mode constants - | FP_RNE_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); } - | FP_RNA_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); } - | FP_RTP_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); } - | FP_RTN_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); } - | FP_RTZ_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); } - | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); } - | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); } - | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); } - | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); } - | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); } - // String constant | str[s,false] { atomTerm = SOLVER->mkString(s, true); } - // Regular expression constants - | RENOSTR_TOK { atomTerm = SOLVER->mkRegexpEmpty(); } - | REALLCHAR_TOK { atomTerm = SOLVER->mkRegexpSigma(); } - - // Set constants - | EMPTYSET_TOK { atomTerm = SOLVER->mkEmptySet(SOLVER->getNullSort()); } - | UNIVSET_TOK - { - // the Boolean sort is a placeholder here since we don't have type info - // without type annotation - atomTerm = SOLVER->mkUniverseSet(SOLVER->getBooleanSort()); - } - - // Separation logic constants - | NILREF_TOK - { - // the Boolean sort is a placeholder here since we don't have type info - // without type annotation - atomTerm = SOLVER->mkSepNil(SOLVER->getBooleanSort()); - } - // NOTE: Theory constants go here // Empty tuple constant @@ -2525,64 +2446,10 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] @init { Expr expr; Expr expr2; + std::vector numerals; } : LPAREN_TOK INDEX_TOK - ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL - { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), - AntlrInput::tokenToUnsigned($n2))); } - | 'repeat' n=INTEGER_LITERAL - { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } - | 'zero_extend' n=INTEGER_LITERAL - { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } - | 'sign_extend' n=INTEGER_LITERAL - { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); } - | 'rotate_left' n=INTEGER_LITERAL - { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } - | 'rotate_right' n=INTEGER_LITERAL - { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } - | DIVISIBLE_TOK n=INTEGER_LITERAL - { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); } - | INT2BV_TOK n=INTEGER_LITERAL - { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n))); - 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"); - } } - | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPGeneric( - AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); - } - | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPIEEEBitVector( - AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); - } - | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPFloatingPoint( - AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); - } - | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); - } - | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPSignedBitVector( - AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); - } - | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPUnsignedBitVector( - AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); - } - | FP_TO_UBV_TOK m=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); } - | FP_TO_SBV_TOK m=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); } - | TESTER_TOK term[expr, expr2] { + ( TESTER_TOK term[expr, expr2] { if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){ //for nullary constructors, must get the operator expr = expr.getOperator(); @@ -2598,25 +2465,15 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] //put m in op so that the caller (termNonVariable) can deal with this case op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); } - | badIndexedFunctionName + | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] + { + op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals) + .getExpr(); + } ) RPAREN_TOK ; -/** - * Matches an erroneous indexed function name (and args) for better - * error reporting. - */ -badIndexedFunctionName -@declarations { - std::string name; -} - : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL) - { PARSER_STATE->parseError(std::string("Unknown indexed function `") + - AntlrInput::tokenText($id) + "'"); - } - ; - /** * Matches a sequence of terms and puts them into the formulas * vector. @@ -2682,56 +2539,6 @@ str[std::string& s, bool fsmtlib] } ; -/** - * Matches a builtin operator symbol and sets kind to its associated Expr kind. - */ -builtinOp[CVC4::Kind& kind] -@init { - Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : NOT_TOK { $kind = CVC4::kind::NOT; } - | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } - | AND_TOK { $kind = CVC4::kind::AND; } - | OR_TOK { $kind = CVC4::kind::OR; } - | XOR_TOK { $kind = CVC4::kind::XOR; } - | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } - | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } - | ITE_TOK { $kind = CVC4::kind::ITE; } - | GREATER_THAN_TOK - { $kind = CVC4::kind::GT; } - | GREATER_THAN_EQUAL_TOK - { $kind = CVC4::kind::GEQ; } - | LESS_THAN_EQUAL_TOK - { $kind = CVC4::kind::LEQ; } - | LESS_THAN_TOK - { $kind = CVC4::kind::LT; } - | PLUS_TOK { $kind = CVC4::kind::PLUS; } - | MINUS_TOK { $kind = CVC4::kind::MINUS; } - | STAR_TOK { $kind = CVC4::kind::MULT; } - | DIV_TOK { $kind = CVC4::kind::DIVISION; } - - | BV2NAT_TOK - { $kind = CVC4::kind::BITVECTOR_TO_NAT; - 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"); - } - } - - | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } - | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } - | FMFCARDVAL_TOK { $kind = CVC4::kind::CARDINALITY_VALUE; } - | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } - - // NOTE: Theory operators no longer go here, add to smt2.cpp. Only - // special cases may go here. When this comment was written (2015 - // Apr), the special cases were: core theory operators, arith - // operators which start with symbols like * / + >= etc, quantifier - // theory operators, and operators which depended on parser's state - // to accept or reject. - ; - quantOp[CVC4::Kind& kind] @init { Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl; @@ -2923,10 +2730,10 @@ symbol[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } } - | ( 'repeat' { id = "repeat"; } + | /* these are keywords in SyGuS but we don't want to inhibit their * use as symbols in SMT-LIB */ - | SET_OPTIONS_TOK { id = "set-options"; } + ( SET_OPTIONS_TOK { id = "set-options"; } | DECLARE_VAR_TOK { id = "declare-var"; } | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; } | SYNTH_FUN_TOK { id = "synth-fun"; } @@ -3049,7 +2856,6 @@ GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; -ITE_TOK : 'ite'; LET_TOK : { !PARSER_STATE->sygus() }? 'let'; SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let'; ATTRIBUTE_TOK : '!'; @@ -3065,7 +2871,7 @@ GET_OPTION_TOK : 'get-option'; PUSH_TOK : 'push'; POP_TOK : 'pop'; AS_TOK : 'as'; -CONST_TOK : 'const'; +CONST_TOK : { !PARSER_STATE->strictModeEnabled() }? 'const'; // extended commands DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype'; @@ -3093,17 +2899,16 @@ INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; DECLARE_HEAP : 'declare-heap'; -EMP_TOK : 'emp'; // SyGuS commands -SYNTH_FUN_TOK : 'synth-fun'; -SYNTH_INV_TOK : 'synth-inv'; -CHECK_SYNTH_TOK : 'check-synth'; -DECLARE_VAR_TOK : 'declare-var'; -DECLARE_PRIMED_VAR_TOK : 'declare-primed-var'; -CONSTRAINT_TOK : 'constraint'; -INV_CONSTRAINT_TOK : 'inv-constraint'; -SET_OPTIONS_TOK : 'set-options'; +SYNTH_FUN_TOK : { PARSER_STATE->sygus() }? 'synth-fun'; +SYNTH_INV_TOK : { PARSER_STATE->sygus() }? 'synth-inv'; +CHECK_SYNTH_TOK : { PARSER_STATE->sygus() }? 'check-synth'; +DECLARE_VAR_TOK : { PARSER_STATE->sygus() }? 'declare-var'; +DECLARE_PRIMED_VAR_TOK : { PARSER_STATE->sygus() }? 'declare-primed-var'; +CONSTRAINT_TOK : { PARSER_STATE->sygus() }? 'constraint'; +INV_CONSTRAINT_TOK : { PARSER_STATE->sygus() }? 'inv-constraint'; +SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options'; SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant'; SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable'; SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable'; @@ -3117,80 +2922,12 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; ATTRIBUTE_RR_PRIORITY : ':rr-priority'; // operators (NOTE: theory symbols go here) -AMPERSAND_TOK : '&'; -AND_TOK : 'and'; -AT_TOK : '@'; -DISTINCT_TOK : 'distinct'; -DIV_TOK : '/'; -EQUAL_TOK : '='; EXISTS_TOK : 'exists'; FORALL_TOK : 'forall'; -GREATER_THAN_TOK : '>'; -GREATER_THAN_EQUAL_TOK : '>='; -IMPLIES_TOK : '=>'; -LESS_THAN_TOK : '<'; -LESS_THAN_EQUAL_TOK : '<='; -MINUS_TOK : '-'; -NOT_TOK : 'not'; -OR_TOK : 'or'; -// PERCENT_TOK : '%'; -PLUS_TOK : '+'; -//POUND_TOK : '#'; -STAR_TOK : '*'; -// TILDE_TOK : '~'; -XOR_TOK : 'xor'; - - -DIVISIBLE_TOK : 'divisible'; - -BV2NAT_TOK : 'bv2nat'; -INT2BV_TOK : 'int2bv'; - -RENOSTR_TOK : 're.nostr'; -REALLCHAR_TOK : 're.allchar'; - -DTSIZE_TOK : 'dt.size'; - -FMFCARD_TOK : 'fmf.card'; -FMFCARDVAL_TOK : 'fmf.card.val'; - -INST_CLOSURE_TOK : 'inst-closure'; -EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; -UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset'; -NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil'; +EMP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'emp'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSel'; -// Other set theory operators are not -// tokenized and handled directly when -// processing a term - -REAL_PI_TOK : 'real.pi'; - -FP_PINF_TOK : '+oo'; -FP_NINF_TOK : '-oo'; -FP_PZERO_TOK : '+zero'; -FP_NZERO_TOK : '-zero'; -FP_NAN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'NaN'; - -FP_TO_FP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp'; -FP_TO_FPBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_bv'; -FP_TO_FPFP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_fp'; -FP_TO_FPR_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_real'; -FP_TO_FPS_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_signed'; -FP_TO_FPU_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_unsigned'; -FP_TO_UBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_ubv'; -FP_TO_SBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_sbv'; -FP_RNE_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNE'; -FP_RNA_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNA'; -FP_RTP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTP'; -FP_RTN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTN'; -FP_RTZ_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTZ'; -FP_RNE_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToEven'; -FP_RNA_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToAway'; -FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardPositive'; -FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative'; -FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero'; HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->'; HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda'; @@ -3223,8 +2960,8 @@ KEYWORD * digit, and is not the special reserved symbols '!' or '_'. */ SIMPLE_SYMBOL - : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+ - | ALPHA + : ALPHA (ALPHA | DIGIT | SYMBOL_CHAR)* + | SYMBOL_CHAR (ALPHA | DIGIT | SYMBOL_CHAR)+ | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2e1abf710..12b43f346 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -15,7 +15,6 @@ **/ #include "parser/smt2/smt2.h" -#include "api/cvc4cpp.h" #include "expr/type.h" #include "options/options.h" #include "parser/antlr_input.h" @@ -45,17 +44,21 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) } void Smt2::addArithmeticOperators() { - Parser::addOperator(kind::PLUS); - Parser::addOperator(kind::MINUS); + addOperator(kind::PLUS, "+"); + addOperator(kind::MINUS, "-"); + // kind::MINUS is converted to kind::UMINUS if there is only a single operand Parser::addOperator(kind::UMINUS); - Parser::addOperator(kind::MULT); - Parser::addOperator(kind::LT); - Parser::addOperator(kind::LEQ); - Parser::addOperator(kind::GT); - Parser::addOperator(kind::GEQ); - - // NOTE: this operator is non-standard - addOperator(kind::POW, "^"); + addOperator(kind::MULT, "*"); + addOperator(kind::LT, "<"); + addOperator(kind::LEQ, "<="); + addOperator(kind::GT, ">"); + addOperator(kind::GEQ, ">="); + + if (!strictModeEnabled()) + { + // NOTE: this operator is non-standard + addOperator(kind::POW, "^"); + } } void Smt2::addTranscendentalOperators() @@ -76,6 +79,14 @@ void Smt2::addTranscendentalOperators() addOperator(kind::SQRT, "sqrt"); } +void Smt2::addQuantifiersOperators() +{ + if (!strictModeEnabled()) + { + addOperator(kind::INST_CLOSURE, "inst-closure"); + } +} + void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_CONCAT, "concat"); addOperator(kind::BITVECTOR_NOT, "bvnot"); @@ -108,17 +119,39 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_SGE, "bvsge"); addOperator(kind::BITVECTOR_REDOR, "bvredor"); addOperator(kind::BITVECTOR_REDAND, "bvredand"); + addOperator(kind::BITVECTOR_TO_NAT, "bv2nat"); + + addIndexedOperator( + kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract"); + addIndexedOperator( + kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat"); + addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND, + api::BITVECTOR_ZERO_EXTEND_OP, + "zero_extend"); + addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND, + api::BITVECTOR_SIGN_EXTEND_OP, + "sign_extend"); + addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT, + api::BITVECTOR_ROTATE_LEFT_OP, + "rotate_left"); + addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT, + api::BITVECTOR_ROTATE_RIGHT_OP, + "rotate_right"); + addIndexedOperator( + kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv"); +} - 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); +void Smt2::addDatatypesOperators() +{ + Parser::addOperator(kind::APPLY_CONSTRUCTOR); + Parser::addOperator(kind::APPLY_TESTER); + Parser::addOperator(kind::APPLY_SELECTOR); + Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); - Parser::addOperator(kind::INT_TO_BITVECTOR); - Parser::addOperator(kind::BITVECTOR_TO_NAT); + if (!strictModeEnabled()) + { + addOperator(kind::DT_SIZE, "dt.size"); + } } void Smt2::addStringOperators() { @@ -194,14 +227,32 @@ void Smt2::addFloatingPointOperators() { addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive"); addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real"); - Parser::addOperator(kind::FLOATINGPOINT_TO_FP_GENERIC); - Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); - Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); - Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL); - Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); - Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); - Parser::addOperator(kind::FLOATINGPOINT_TO_UBV); - Parser::addOperator(kind::FLOATINGPOINT_TO_SBV); + addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC, + api::FLOATINGPOINT_TO_FP_GENERIC_OP, + "to_fp"); + addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, + "to_fp_unsigned"); + addIndexedOperator( + kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv"); + addIndexedOperator( + kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv"); + + if (!strictModeEnabled()) + { + addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, + "to_fp_bv"); + addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, + api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, + "to_fp_fp"); + addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL, + api::FLOATINGPOINT_TO_FP_REAL_OP, + "to_fp_real"); + addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, + "to_fp_signed"); + } } void Smt2::addSepOperators() { @@ -230,19 +281,19 @@ void Smt2::addTheory(Theory theory) { defineType("Bool", getExprManager()->booleanType()); defineVar("true", getExprManager()->mkConst(true)); defineVar("false", getExprManager()->mkConst(false)); - Parser::addOperator(kind::AND); - Parser::addOperator(kind::DISTINCT); - Parser::addOperator(kind::EQUAL); - Parser::addOperator(kind::IMPLIES); - Parser::addOperator(kind::ITE); - Parser::addOperator(kind::NOT); - Parser::addOperator(kind::OR); - Parser::addOperator(kind::XOR); + addOperator(kind::AND, "and"); + addOperator(kind::DISTINCT, "distinct"); + addOperator(kind::EQUAL, "="); + addOperator(kind::IMPLIES, "=>"); + addOperator(kind::ITE, "ite"); + addOperator(kind::NOT, "not"); + addOperator(kind::OR, "or"); + addOperator(kind::XOR, "xor"); break; case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); - Parser::addOperator(kind::DIVISION); + addOperator(kind::DIVISION, "/"); addOperator(kind::TO_INTEGER, "to_int"); addOperator(kind::IS_INTEGER, "is_int"); addOperator(kind::TO_REAL, "to_real"); @@ -253,21 +304,36 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::INTS_DIVISION, "div"); addOperator(kind::INTS_MODULUS, "mod"); addOperator(kind::ABS, "abs"); - Parser::addOperator(kind::DIVISIBLE); + addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible"); break; case THEORY_REALS: defineType("Real", getExprManager()->realType()); addArithmeticOperators(); - Parser::addOperator(kind::DIVISION); + addOperator(kind::DIVISION, "/"); + if (!strictModeEnabled()) + { + addOperator(kind::ABS, "abs"); + } break; - case THEORY_TRANSCENDENTALS: addTranscendentalOperators(); break; - - case THEORY_QUANTIFIERS: + case THEORY_TRANSCENDENTALS: + defineVar("real.pi", + getExprManager()->mkNullaryOperator(getExprManager()->realType(), + CVC4::kind::PI)); + addTranscendentalOperators(); break; + case THEORY_QUANTIFIERS: addQuantifiersOperators(); break; + case THEORY_SETS: + defineVar("emptyset", + d_solver->mkEmptySet(d_solver->getNullSort()).getExpr()); + // the Boolean sort is a placeholder here since we don't have type info + // without type annotation + defineVar("univset", + d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr()); + addOperator(kind::UNION, "union"); addOperator(kind::INTERSECTION, "intersection"); addOperator(kind::SETMINUS, "setminus"); @@ -287,10 +353,7 @@ void Smt2::addTheory(Theory theory) { { const std::vector types; defineType("Tuple", getExprManager()->mkTupleType(types)); - Parser::addOperator(kind::APPLY_CONSTRUCTOR); - Parser::addOperator(kind::APPLY_TESTER); - Parser::addOperator(kind::APPLY_SELECTOR); - Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); + addDatatypesOperators(); break; } @@ -298,11 +361,21 @@ void Smt2::addTheory(Theory theory) { defineType("String", getExprManager()->stringType()); defineType("RegLan", getExprManager()->regExpType()); defineType("Int", getExprManager()->integerType()); + + defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr()); + defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr()); + addStringOperators(); break; case THEORY_UF: Parser::addOperator(kind::APPLY_UF); + + if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) + { + addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card"); + addOperator(kind::CARDINALITY_VALUE, "fmf.card.val"); + } break; case THEORY_FP: @@ -311,10 +384,41 @@ void Smt2::addTheory(Theory theory) { defineType("Float32", getExprManager()->mkFloatingPointType(8, 24)); defineType("Float64", getExprManager()->mkFloatingPointType(11, 53)); defineType("Float128", getExprManager()->mkFloatingPointType(15, 113)); + + defineVar( + "RNE", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr()); + defineVar( + "roundNearestTiesToEven", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr()); + defineVar( + "RNA", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr()); + defineVar( + "roundNearestTiesToAway", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr()); + defineVar("RTP", + d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr()); + defineVar("roundTowardPositive", + d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr()); + defineVar("RTN", + d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr()); + defineVar("roundTowardNegative", + d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr()); + defineVar("RTZ", + d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr()); + defineVar("roundTowardZero", + d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr()); + addFloatingPointOperators(); break; case THEORY_SEP: + // the Boolean sort is a placeholder here since we don't have type info + // without type annotation + defineVar("sep.nil", + d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr()); + addSepOperators(); break; @@ -332,6 +436,14 @@ void Smt2::addOperator(Kind kind, const std::string& name) { operatorKindMap[name] = kind; } +void Smt2::addIndexedOperator(Kind tKind, + api::Kind opKind, + const std::string& name) +{ + Parser::addOperator(tKind); + d_indexedOpKindMap[name] = opKind; +} + Kind Smt2::getOperatorKind(const std::string& name) const { // precondition: isOperatorEnabled(name) return operatorKindMap.find(name)->second; @@ -395,6 +507,66 @@ Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) { } } +api::Term Smt2::mkIndexedConstant(const std::string& name, + const std::vector& numerals) +{ + if (isTheoryEnabled(THEORY_FP)) + { + if (name == "+oo") + { + return d_solver->mkPosInf(numerals[0], numerals[1]); + } + else if (name == "-oo") + { + return d_solver->mkNegInf(numerals[0], numerals[1]); + } + else if (name == "NaN") + { + return d_solver->mkNaN(numerals[0], numerals[1]); + } + else if (name == "+zero") + { + return d_solver->mkPosZero(numerals[0], numerals[1]); + } + else if (name == "-zero") + { + return d_solver->mkNegZero(numerals[0], numerals[1]); + } + } + + if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0) + { + std::string bvStr = name.substr(2); + return d_solver->mkBitVector(numerals[0], bvStr, 10); + } + + // NOTE: Theory parametric constants go here + + parseError(std::string("Unknown indexed literal `") + name + "'"); + return api::Term(); +} + +api::OpTerm Smt2::mkIndexedOp(const std::string& name, + const std::vector& numerals) +{ + const auto& kIt = d_indexedOpKindMap.find(name); + if (kIt != d_indexedOpKindMap.end()) + { + api::Kind k = (*kIt).second; + if (numerals.size() == 1) + { + return d_solver->mkOpTerm(k, numerals[0]); + } + else if (numerals.size() == 2) + { + return d_solver->mkOpTerm(k, numerals[0], numerals[1]); + } + } + + parseError(std::string("Unknown indexed function `") + name + "'"); + return api::OpTerm(); +} + Expr Smt2::mkDefineFunRec( const std::string& fname, const std::vector >& sortedVarNames, @@ -1233,5 +1405,5 @@ InputLanguage Smt2::getLanguage() const return em->getOptions().getInputLanguage(); } -}/* CVC4::parser namespace */ +} // namespace parser }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ee694db06..d4d310b89 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -25,6 +25,7 @@ #include #include +#include "api/cvc4cpp.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "theory/logic_info.h" @@ -40,32 +41,38 @@ class Solver; namespace parser { -class Smt2 : public Parser { +class Smt2 : public Parser +{ friend class ParserBuilder; -public: - enum Theory - { - THEORY_ARRAYS, - THEORY_BITVECTORS, - THEORY_CORE, - THEORY_DATATYPES, - THEORY_INTS, - THEORY_REALS, - THEORY_TRANSCENDENTALS, - THEORY_REALS_INTS, - THEORY_QUANTIFIERS, - THEORY_SETS, - THEORY_STRINGS, - THEORY_UF, - THEORY_FP, - THEORY_SEP - }; - -private: + public: + enum Theory + { + THEORY_ARRAYS, + THEORY_BITVECTORS, + THEORY_CORE, + THEORY_DATATYPES, + THEORY_INTS, + THEORY_REALS, + THEORY_TRANSCENDENTALS, + THEORY_REALS_INTS, + THEORY_QUANTIFIERS, + THEORY_SETS, + THEORY_STRINGS, + THEORY_UF, + THEORY_FP, + THEORY_SEP + }; + + private: bool d_logicSet; LogicInfo d_logic; std::unordered_map operatorKindMap; + /** + * Maps indexed symbols to the kind of the operator (e.g. "extract" to + * BITVECTOR_EXTRACT_OP). + */ + std::unordered_map d_indexedOpKindMap; std::pair d_lastNamedTerm; // for sygus std::vector d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, @@ -87,6 +94,20 @@ private: void addOperator(Kind k, const std::string& name); + /** + * Registers an indexed function symbol. + * + * @param tKind The kind of the term that uses the operator kind (e.g. + * BITVECTOR_EXTRACT). NOTE: this is an internal kind for now + * because that is what we use to create expressions. Eventually + * it will be an api::Kind. + * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT_OP) + * @param name The name of the symbol (e.g. "extract") + */ + void addIndexedOperator(Kind tKind, + api::Kind opKind, + const std::string& name); + Kind getOperatorKind(const std::string& name) const; bool isOperatorEnabled(const std::string& name) const; @@ -96,24 +117,47 @@ private: bool logicIsSet() override; /** - * Returns the expression that name should be interpreted as. + * Creates an indexed constant, e.g. (_ +oo 8 24) (positive infinity + * as a 32-bit floating-point constant). + * + * @param name The name of the constant (e.g. "+oo") + * @param numerals The parameters for the constant (e.g. [8, 24]) + * @return The term corresponding to the constant or a parse error if name is + * not valid. + */ + api::Term mkIndexedConstant(const std::string& name, + const std::vector& numerals); + + /** + * Creates an indexed operator term, e.g. (_ extract 5 0). + * + * @param name The name of the operator (e.g. "extract") + * @param numerals The parameters for the operator (e.g. [5, 0]) + * @return The operator term corresponding to the indexed operator or a parse + * error if the name is not valid. + */ + api::OpTerm mkIndexedOp(const std::string& name, + const std::vector& numerals); + + /** + * Returns the expression that name should be interpreted as. */ Expr getExpressionForNameAndType(const std::string& name, Type t) override; /** Make function defined by a define-fun(s)-rec command. - * - * fname : the name of the function. - * sortedVarNames : the list of variable arguments for the function. - * t : the range type of the function we are defining. - * - * This function will create a bind a new function term to name fname. - * The type of this function is - * Parser::mkFlatFunctionType(sorts,t,flattenVars), - * where sorts are the types in the second components of sortedVarNames. - * As descibed in Parser::mkFlatFunctionType, new bound variables may be - * added to flattenVars in this function if the function is given a function - * range type. - */ + * + * fname : the name of the function. + * sortedVarNames : the list of variable arguments for the function. + * t : the range type of the function we are defining. + * + * This function will create a bind a new function term to name fname. + * The type of this function is + * Parser::mkFlatFunctionType(sorts,t,flattenVars), + * where sorts are the types in the second components of sortedVarNames. + * As descibed in Parser::mkFlatFunctionType, new bound variables may be + * added to flattenVars in this function if the function is given a function + * range type. + */ Expr mkDefineFunRec( const std::string& fname, const std::vector >& sortedVarNames, @@ -122,21 +166,21 @@ private: /** Push scope for define-fun-rec * - * This calls Parser::pushScope(bindingLevel) and sets up - * initial information for reading a body of a function definition - * in the define-fun-rec and define-funs-rec command. - * The input parameters func/flattenVars are the result - * of a call to mkDefineRec above. - * - * func : the function whose body we are defining. - * sortedVarNames : the list of variable arguments for the function. - * flattenVars : the implicit variables introduced when defining func. - * - * This function: - * (1) Calls Parser::pushScope(bindingLevel). - * (2) Computes the bound variable list for the quantified formula - * that defined this definition and stores it in bvs. - */ + * This calls Parser::pushScope(bindingLevel) and sets up + * initial information for reading a body of a function definition + * in the define-fun-rec and define-funs-rec command. + * The input parameters func/flattenVars are the result + * of a call to mkDefineRec above. + * + * func : the function whose body we are defining. + * sortedVarNames : the list of variable arguments for the function. + * flattenVars : the implicit variables introduced when defining func. + * + * This function: + * (1) Calls Parser::pushScope(bindingLevel). + * (2) Computes the bound variable list for the quantified formula + * that defined this definition and stores it in bvs. + */ void pushDefineFunRecScope( const std::vector >& sortedVarNames, Expr func, @@ -161,7 +205,8 @@ private: */ const LogicInfo& getLogic() const { return d_logic; } - bool v2_0() const { + bool v2_0() const + { return getLanguage() == language::input::LANG_SMTLIB_V2_0; } /** @@ -400,8 +445,12 @@ private: void addTranscendentalOperators(); + void addQuantifiersOperators(); + void addBitvectorOperators(); + void addDatatypesOperators(); + void addStringOperators(); void addFloatingPointOperators(); @@ -409,7 +458,7 @@ private: void addSepOperators(); InputLanguage getLanguage() const; -};/* class Smt2 */ +}; /* class Smt2 */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2 index c7a5a605f..1e2bcde68 100644 --- a/test/regress/regress0/bv/core/constant_core.smt2 +++ b/test/regress/regress0/bv/core/constant_core.smt2 @@ -12,4 +12,4 @@ (not (= (_ bv0 3) x)) )) (check-sat) -(exit) \ No newline at end of file +(exit) diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 24a0aab2e..aec265f2b 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -8,5 +8,5 @@ (declare-var n Int) (synth-fun f ((n Int)) Int) -(constraint (= (/ n n) 1)) +(constraint (= (div n n) 1)) (check-synth) diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2 index a303f48b1..4163e09f9 100644 --- a/test/regress/regress0/nl/nta/real-pi.smt2 +++ b/test/regress/regress0/nl/nta/real-pi.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --nl-ext --no-check-models ; EXPECT: sat -(set-logic QF_NRA) +(set-logic QF_NRAT) (set-info :status sat) (assert (<= 3.0 real.pi)) (assert (<= real.pi 4.0)) diff --git a/test/regress/regress0/strings/bug613.smt2 b/test/regress/regress0/strings/bug613.smt2 index 506076cd6..09c5e9a2a 100644 --- a/test/regress/regress0/strings/bug613.smt2 +++ b/test/regress/regress0/strings/bug613.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2 index 8a03f4481..21570a2da 100644 --- a/test/regress/regress0/strings/str004.smt2 +++ b/test/regress/regress0/strings/str004.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status unsat) (declare-fun xx () String) diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2 index 89191ac34..36a6aaec1 100644 --- a/test/regress/regress0/strings/type001.smt2 +++ b/test/regress/regress0/strings/type001.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2 index 2b25e6dc8..9c91d135f 100644 --- a/test/regress/regress0/strings/unsound-0908.smt2 +++ b/test/regress/regress0/strings/unsound-0908.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (declare-const x String) (assert (= (str.len x) 1)) diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2 index a3cca23a2..328317ea4 100644 --- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 +++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status unsat) diff --git a/test/regress/regress1/strings/at001.smt2 b/test/regress/regress1/strings/at001.smt2 index 2ecbcc993..04933b8f7 100644 --- a/test/regress/regress1/strings/at001.smt2 +++ b/test/regress/regress1/strings/at001.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2 index ab3dc2ae2..2f2209ae7 100644 --- a/test/regress/regress1/strings/fmf002.smt2 +++ b/test/regress/regress1/strings/fmf002.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-option :strings-exp true) (set-option :strings-fmf true) (set-info :status sat) diff --git a/test/regress/regress1/strings/issue2429-code.smt2 b/test/regress/regress1/strings/issue2429-code.smt2 index 2d906c1fd..9dc29794e 100644 --- a/test/regress/regress1/strings/issue2429-code.smt2 +++ b/test/regress/regress1/strings/issue2429-code.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-option :strings-exp true) (set-option :produce-models true) (set-info :status sat) diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2 index 20c2e6aa4..d277d85e6 100644 --- a/test/regress/regress1/strings/kaluza-fl.smt2 +++ b/test/regress/regress1/strings/kaluza-fl.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (declare-fun I0_15 () Int) diff --git a/test/regress/regress1/strings/loop005.smt2 b/test/regress/regress1/strings/loop005.smt2 index 039409ea6..cc115ebf4 100644 --- a/test/regress/regress1/strings/loop005.smt2 +++ b/test/regress/regress1/strings/loop005.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress1/strings/loop007.smt2 b/test/regress/regress1/strings/loop007.smt2 index a97d97d54..492162ae6 100644 --- a/test/regress/regress1/strings/loop007.smt2 +++ b/test/regress/regress1/strings/loop007.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status sat) diff --git a/test/regress/regress1/strings/loop008.smt2 b/test/regress/regress1/strings/loop008.smt2 index f84ba442b..672ecd371 100644 --- a/test/regress/regress1/strings/loop008.smt2 +++ b/test/regress/regress1/strings/loop008.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status sat) diff --git a/test/regress/regress1/strings/re-agg-total1.smt2 b/test/regress/regress1/strings/re-agg-total1.smt2 index 4e5b21c0f..2950066a0 100644 --- a/test/regress/regress1/strings/re-agg-total1.smt2 +++ b/test/regress/regress1/strings/re-agg-total1.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status unsat) (set-option :strings-exp true) (set-option :re-elim-agg true) diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2 index 967e564ce..22537b957 100644 --- a/test/regress/regress1/strings/reloop.smt2 +++ b/test/regress/regress1/strings/reloop.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status sat) diff --git a/test/regress/regress1/strings/substr001.smt2 b/test/regress/regress1/strings/substr001.smt2 index 78f3ffee7..47fa995ff 100644 --- a/test/regress/regress1/strings/substr001.smt2 +++ b/test/regress/regress1/strings/substr001.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2 index 458ac75fe..3b46b25a8 100644 --- a/test/regress/regress1/strings/type002.smt2 +++ b/test/regress/regress1/strings/type002.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2 index 4185041f7..332ec3ec3 100644 --- a/test/regress/regress1/strings/type003.smt2 +++ b/test/regress/regress1/strings/type003.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.5) -(set-logic QF_S) +(set-logic QF_SLIA) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 33ad3740a..f2f5f24b6 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -138,6 +138,12 @@ class ParserBlack .withInputLanguage(d_lang) .build(); + if (d_lang == LANG_SMTLIB_V2) + { + // Use QF_LIA to make multiplication ("*") available + static_cast(parser)->setLogic("QF_LIA"); + } + TS_ASSERT(!parser->done()); setupContext(*parser); TS_ASSERT(!parser->done()); -- 2.30.2