From: Andres Noetzli Date: Thu, 19 Mar 2020 06:46:50 +0000 (-0700) Subject: Only allow bv2nat/int2bv with BV and integer logic (#4118) X-Git-Tag: cvc5-1.0.0~3475 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d862942f821ea14973207ef538be3326fb11c17c;p=cvc5.git Only allow bv2nat/int2bv with BV and integer logic (#4118) CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from integers. Those operators are not standard. This commit only enables those operators when parsing is non-strict and both bit-vectors and integers are enabled in the logic. To achieve this, the commit simplifies the handling of logics in the parser: Instead of defining a separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo` directly. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e54f8eaa9..d01fd7a05 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -250,13 +250,10 @@ command [std::unique_ptr* cmd] AntlrInput::tokenText($KEYWORD).c_str() + 1)); } | /* sort declaration */ - DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && - !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && - !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) && - !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) { - PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in "); - } + DECLARE_SORT_TOK + { + PARSER_STATE->checkThatLogicIsSet(); + PARSER_STATE->checkLogicAllowsFreeSorts(); } symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); } @@ -303,12 +300,9 @@ command [std::unique_ptr* cmd] if( !sorts.empty() ) { t = PARSER_STATE->mkFlatFunctionType(sorts, t); } - if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseError( - "Functions (of non-zero arity) cannot " - "be declared in logic " - + PARSER_STATE->getLogic().getLogicString() - + " unless option --uf-ho is used."); + if(t.isFunction()) + { + PARSER_STATE->checkLogicAllowsFunctions(); } // we allow overloading for function declarations if (PARSER_STATE->sygus_v1()) @@ -1259,15 +1253,12 @@ extendedCommand[std::unique_ptr* cmd] /* Support some of Z3's extended SMT-LIB commands */ - | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && - !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && - !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) && - !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) { - PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in "); - } + | DECLARE_SORTS_TOK + { + PARSER_STATE->checkThatLogicIsSet(); + PARSER_STATE->checkLogicAllowsFreeSorts(); + seq.reset(new CVC4::CommandSequence()); } - { seq.reset(new CVC4::CommandSequence()); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); @@ -1286,13 +1277,7 @@ extendedCommand[std::unique_ptr* cmd] nonemptySortList[sorts] RPAREN_TOK { api::Sort tt; if(sorts.size() > 1) { - if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseError( - "Functions (of non-zero arity) cannot " - "be declared in logic " - + PARSER_STATE->getLogic().getLogicString() - + " unless option --uf-ho is used"); - } + PARSER_STATE->checkLogicAllowsFunctions(); // must flatten api::Sort range = sorts.back(); sorts.pop_back(); @@ -1318,13 +1303,7 @@ extendedCommand[std::unique_ptr* cmd] sortList[sorts] RPAREN_TOK { t = SOLVER->getBooleanSort(); if(sorts.size() > 0) { - if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseError( - "Functions (of non-zero arity) cannot " - "be declared in logic " - + PARSER_STATE->getLogic().getLogicString() - + " unless option --uf-ho is used"); - } + PARSER_STATE->checkLogicAllowsFunctions(); t = SOLVER->mkFunctionSort(sorts, t); } // allow overloading @@ -2414,13 +2393,13 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] PARSER_STATE->parseError("Extra parentheses around sort name not " "permitted in SMT-LIB"); } else if(name == "Array" && - PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) { + PARSER_STATE->isTheoryEnabled(theory::THEORY_ARRAYS) ) { if(args.size() != 2) { PARSER_STATE->parseError("Illegal array type."); } t = SOLVER->mkArraySort( args[0], args[1] ); } else if(name == "Set" && - PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) { + PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) ) { if(args.size() != 1) { PARSER_STATE->parseError("Illegal set type."); } @@ -2611,9 +2590,9 @@ DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'decla DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes'; DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes'; PAR_TOK : { PARSER_STATE->v2_6() }?'par'; -COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }?'comprehension'; -TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is'; -MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match'; +COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension'; +TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is'; +MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match'; GET_MODEL_TOK : 'get-model'; BLOCK_MODEL_TOK : 'block-model'; BLOCK_MODEL_VALUES_TOK : 'block-model-values'; @@ -2657,9 +2636,9 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; EXISTS_TOK : 'exists'; FORALL_TOK : 'forall'; -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'; +EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; +TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; +TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->'; HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c30c44362..c7c30005c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -40,7 +40,7 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) { if (!strictModeEnabled()) { - addTheory(Smt2::THEORY_CORE); + addCoreSymbols(); } } @@ -120,7 +120,6 @@ void Smt2::addBitvectorOperators() { addOperator(api::BITVECTOR_SGE, "bvsge"); addOperator(api::BITVECTOR_REDOR, "bvredor"); addOperator(api::BITVECTOR_REDAND, "bvredand"); - addOperator(api::BITVECTOR_TO_NAT, "bv2nat"); addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); @@ -132,7 +131,6 @@ void Smt2::addBitvectorOperators() { api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); addIndexedOperator( api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); - addIndexedOperator(api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); } void Smt2::addDatatypesOperators() @@ -270,161 +268,19 @@ void Smt2::addSepOperators() { Parser::addOperator(api::SEP_EMP); } -void Smt2::addTheory(Theory theory) { - switch(theory) { - case THEORY_ARRAYS: - addOperator(api::SELECT, "select"); - addOperator(api::STORE, "store"); - break; - - case THEORY_BITVECTORS: - addBitvectorOperators(); - break; - - case THEORY_CORE: - defineType("Bool", d_solver->getBooleanSort()); - defineVar("true", d_solver->mkTrue()); - defineVar("false", d_solver->mkFalse()); - addOperator(api::AND, "and"); - addOperator(api::DISTINCT, "distinct"); - addOperator(api::EQUAL, "="); - addOperator(api::IMPLIES, "=>"); - addOperator(api::ITE, "ite"); - addOperator(api::NOT, "not"); - addOperator(api::OR, "or"); - addOperator(api::XOR, "xor"); - break; - - case THEORY_REALS_INTS: - defineType("Real", d_solver->getRealSort()); - addOperator(api::DIVISION, "/"); - addOperator(api::TO_INTEGER, "to_int"); - addOperator(api::IS_INTEGER, "is_int"); - addOperator(api::TO_REAL, "to_real"); - // falling through on purpose, to add Ints part of Reals_Ints - CVC4_FALLTHROUGH; - case THEORY_INTS: - defineType("Int", d_solver->getIntegerSort()); - addArithmeticOperators(); - addOperator(api::INTS_DIVISION, "div"); - addOperator(api::INTS_MODULUS, "mod"); - addOperator(api::ABS, "abs"); - addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible"); - break; - - case THEORY_REALS: - defineType("Real", d_solver->getRealSort()); - addArithmeticOperators(); - addOperator(api::DIVISION, "/"); - if (!strictModeEnabled()) - { - addOperator(api::ABS, "abs"); - } - break; - - case THEORY_TRANSCENDENTALS: - defineVar("real.pi", d_solver->mkTerm(api::PI)); - addTranscendentalOperators(); - break; - - case THEORY_QUANTIFIERS: addQuantifiersOperators(); break; - - case THEORY_SETS: - defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort())); - // 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())); - - addOperator(api::UNION, "union"); - addOperator(api::INTERSECTION, "intersection"); - addOperator(api::SETMINUS, "setminus"); - addOperator(api::SUBSET, "subset"); - addOperator(api::MEMBER, "member"); - addOperator(api::SINGLETON, "singleton"); - addOperator(api::INSERT, "insert"); - addOperator(api::CARD, "card"); - addOperator(api::COMPLEMENT, "complement"); - addOperator(api::JOIN, "join"); - addOperator(api::PRODUCT, "product"); - addOperator(api::TRANSPOSE, "transpose"); - addOperator(api::TCLOSURE, "tclosure"); - break; - - case THEORY_DATATYPES: - { - const std::vector types; - defineType("Tuple", d_solver->mkTupleSort(types)); - addDatatypesOperators(); - break; - } - - case THEORY_STRINGS: - defineType("String", d_solver->getStringSort()); - defineType("RegLan", d_solver->getRegExpSort()); - defineType("Int", d_solver->getIntegerSort()); - - if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) - { - defineVar("re.none", d_solver->mkRegexpEmpty()); - } - else - { - defineVar("re.nostr", d_solver->mkRegexpEmpty()); - } - defineVar("re.allchar", d_solver->mkRegexpSigma()); - - addStringOperators(); - break; - - case THEORY_UF: - Parser::addOperator(api::APPLY_UF); - - if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) - { - addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card"); - addOperator(api::CARDINALITY_VALUE, "fmf.card.val"); - } - break; - - case THEORY_FP: - defineType("RoundingMode", d_solver->getRoundingmodeSort()); - defineType("Float16", d_solver->mkFloatingPointSort(5, 11)); - defineType("Float32", d_solver->mkFloatingPointSort(8, 24)); - defineType("Float64", d_solver->mkFloatingPointSort(11, 53)); - defineType("Float128", d_solver->mkFloatingPointSort(15, 113)); - - defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); - defineVar("roundNearestTiesToEven", - d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); - defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); - defineVar("roundNearestTiesToAway", - d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); - defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); - defineVar("roundTowardPositive", - d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); - defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); - defineVar("roundTowardNegative", - d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); - defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); - defineVar("roundTowardZero", - d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); - - 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())); - - addSepOperators(); - break; - - default: - std::stringstream ss; - ss << "internal error: unsupported theory " << theory; - throw ParserException(ss.str()); - } +void Smt2::addCoreSymbols() +{ + defineType("Bool", d_solver->getBooleanSort()); + defineVar("true", d_solver->mkTrue()); + defineVar("false", d_solver->mkFalse()); + addOperator(api::AND, "and"); + addOperator(api::DISTINCT, "distinct"); + addOperator(api::EQUAL, "="); + addOperator(api::IMPLIES, "=>"); + addOperator(api::ITE, "ite"); + addOperator(api::NOT, "not"); + addOperator(api::OR, "or"); + addOperator(api::XOR, "xor"); } void Smt2::addOperator(api::Kind kind, const std::string& name) @@ -453,42 +309,9 @@ 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_ARRAYS); - case THEORY_BITVECTORS: - return d_logic.isTheoryEnabled(theory::THEORY_BV); - case THEORY_CORE: - return true; - case THEORY_DATATYPES: - return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES); - 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); - case THEORY_FP: - return d_logic.isTheoryEnabled(theory::THEORY_FP); - case THEORY_SEP: - return d_logic.isTheoryEnabled(theory::THEORY_SEP); - default: - std::stringstream ss; - ss << "internal error: unsupported theory " << theory; - throw ParserException(ss.str()); - } +bool Smt2::isTheoryEnabled(theory::TheoryId theory) const +{ + return d_logic.isTheoryEnabled(theory); } bool Smt2::logicIsSet() { @@ -522,7 +345,7 @@ bool Smt2::getTesterName(api::Term cons, std::string& name) api::Term Smt2::mkIndexedConstant(const std::string& name, const std::vector& numerals) { - if (isTheoryEnabled(THEORY_FP)) + if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { if (name == "+oo") { @@ -546,7 +369,7 @@ api::Term Smt2::mkIndexedConstant(const std::string& name, } } - if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0) + if (d_logic.isTheoryEnabled(theory::THEORY_BV) && name.find("bv") == 0) { std::string bvStr = name.substr(2); return d_solver->mkBitVector(numerals[0], bvStr, 10); @@ -628,7 +451,7 @@ void Smt2::reset() { this->Parser::reset(); if( !strictModeEnabled() ) { - addTheory(Smt2::THEORY_CORE); + addCoreSymbols(); } } @@ -760,59 +583,152 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } // Core theory belongs to every logic - addTheory(THEORY_CORE); + addCoreSymbols(); if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { - addTheory(THEORY_UF); + Parser::addOperator(api::APPLY_UF); + + if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) + { + addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card"); + addOperator(api::CARDINALITY_VALUE, "fmf.card.val"); + } } if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { if(d_logic.areIntegersUsed()) { - if(d_logic.areRealsUsed()) { - addTheory(THEORY_REALS_INTS); - } else { - addTheory(THEORY_INTS); + defineType("Int", d_solver->getIntegerSort()); + addArithmeticOperators(); + addOperator(api::INTS_DIVISION, "div"); + addOperator(api::INTS_MODULUS, "mod"); + addOperator(api::ABS, "abs"); + addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible"); + } + + if (d_logic.areRealsUsed()) + { + defineType("Real", d_solver->getRealSort()); + addArithmeticOperators(); + addOperator(api::DIVISION, "/"); + if (!strictModeEnabled()) + { + addOperator(api::ABS, "abs"); } - } else if(d_logic.areRealsUsed()) { - addTheory(THEORY_REALS); + } + + if (d_logic.areIntegersUsed() && d_logic.areRealsUsed()) + { + addOperator(api::TO_INTEGER, "to_int"); + addOperator(api::IS_INTEGER, "is_int"); + addOperator(api::TO_REAL, "to_real"); } if (d_logic.areTranscendentalsUsed()) { - addTheory(THEORY_TRANSCENDENTALS); + defineVar("real.pi", d_solver->mkTerm(api::PI)); + addTranscendentalOperators(); } } if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { - addTheory(THEORY_ARRAYS); + addOperator(api::SELECT, "select"); + addOperator(api::STORE, "store"); } if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { - addTheory(THEORY_BITVECTORS); + addBitvectorOperators(); + + if (!strictModeEnabled() && d_logic.isTheoryEnabled(theory::THEORY_ARITH) + && d_logic.areIntegersUsed()) + { + // Conversions between bit-vectors and integers + addOperator(api::BITVECTOR_TO_NAT, "bv2nat"); + addIndexedOperator( + api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); + } } if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { - addTheory(THEORY_DATATYPES); + const std::vector types; + defineType("Tuple", d_solver->mkTupleSort(types)); + addDatatypesOperators(); } if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) { - addTheory(THEORY_SETS); + defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort())); + // 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())); + + addOperator(api::UNION, "union"); + addOperator(api::INTERSECTION, "intersection"); + addOperator(api::SETMINUS, "setminus"); + addOperator(api::SUBSET, "subset"); + addOperator(api::MEMBER, "member"); + addOperator(api::SINGLETON, "singleton"); + addOperator(api::INSERT, "insert"); + addOperator(api::CARD, "card"); + addOperator(api::COMPLEMENT, "complement"); + addOperator(api::JOIN, "join"); + addOperator(api::PRODUCT, "product"); + addOperator(api::TRANSPOSE, "transpose"); + addOperator(api::TCLOSURE, "tclosure"); } if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { - addTheory(THEORY_STRINGS); + defineType("String", d_solver->getStringSort()); + defineType("RegLan", d_solver->getRegExpSort()); + defineType("Int", d_solver->getIntegerSort()); + + if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) + { + defineVar("re.none", d_solver->mkRegexpEmpty()); + } + else + { + defineVar("re.nostr", d_solver->mkRegexpEmpty()); + } + defineVar("re.allchar", d_solver->mkRegexpSigma()); + + addStringOperators(); } if(d_logic.isQuantified()) { - addTheory(THEORY_QUANTIFIERS); + addQuantifiersOperators(); } if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { - addTheory(THEORY_FP); + defineType("RoundingMode", d_solver->getRoundingmodeSort()); + defineType("Float16", d_solver->mkFloatingPointSort(5, 11)); + defineType("Float32", d_solver->mkFloatingPointSort(8, 24)); + defineType("Float64", d_solver->mkFloatingPointSort(11, 53)); + defineType("Float128", d_solver->mkFloatingPointSort(15, 113)); + + defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); + defineVar("roundNearestTiesToEven", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); + defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); + defineVar("roundNearestTiesToAway", + d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); + defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); + defineVar("roundTowardPositive", + d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); + defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); + defineVar("roundTowardNegative", + d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); + defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); + defineVar("roundTowardZero", + d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); + + addFloatingPointOperators(); } if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) { - addTheory(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())); + + addSepOperators(); } Command* cmd = @@ -871,6 +787,28 @@ void Smt2::checkThatLogicIsSet() } } +void Smt2::checkLogicAllowsFreeSorts() +{ + if (!d_logic.isTheoryEnabled(theory::THEORY_UF) + && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS) + && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES) + && !d_logic.isTheoryEnabled(theory::THEORY_SETS)) + { + parseErrorLogic("Free sort symbols not allowed in "); + } +} + +void Smt2::checkLogicAllowsFunctions() +{ + if (!d_logic.isTheoryEnabled(theory::THEORY_UF)) + { + parseError( + "Functions (of non-zero arity) cannot " + "be declared in logic " + + d_logic.getLogicString() + " unless option --uf-ho is used"); + } +} + /* The include are managed in the lexer but called in the parser */ // Inspired by http://www.antlr3.org/api/C/interop.html diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 6d3c2e6f6..0400c680f 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -46,25 +46,6 @@ 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: /** Has the logic been set (either by forcing it or a set-logic command)? */ bool d_logicSet; @@ -91,11 +72,9 @@ class Smt2 : public Parser public: /** - * Add theory symbols to the parser state. - * - * @param theory the theory to open (e.g., Core, Ints) + * Add core theory symbols to the parser state. */ - void addTheory(Theory theory); + void addCoreSymbols(); void addOperator(api::Kind k, const std::string& name); @@ -117,7 +96,7 @@ class Smt2 : public Parser bool isOperatorEnabled(const std::string& name) const; - bool isTheoryEnabled(Theory theory) const; + bool isTheoryEnabled(theory::TheoryId theory) const; bool logicIsSet() override; @@ -312,6 +291,19 @@ class Smt2 : public Parser void checkThatLogicIsSet(); + /** + * Checks whether the current logic allows free sorts. If the logic does not + * support free sorts, the function triggers a parse error. + */ + void checkLogicAllowsFreeSorts(); + + /** + * Checks whether the current logic allows functions of non-zero arity. If + * the logic does not support such functions, the function triggers a parse + * error. + */ + void checkLogicAllowsFunctions(); + void checkUserSymbol(const std::string& name) { if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) { std::stringstream ss; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bffb2c4db..0ea611435 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -608,6 +608,7 @@ set(regress_0_tests regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 + regress0/parser/bv_nat.smt2 regress0/parser/constraint.smt2 regress0/parser/declarefun-emptyset-uf.smt2 regress0/parser/force_logic_set_logic.smt2 diff --git a/test/regress/regress0/parser/bv_nat.smt2 b/test/regress/regress0/parser/bv_nat.smt2 new file mode 100644 index 000000000..fc2140854 --- /dev/null +++ b/test/regress/regress0/parser/bv_nat.smt2 @@ -0,0 +1,13 @@ +; EXPECT: sat +; EXPECT: not declared +; SCRUBBER: grep -o "sat\|not declared" +; EXIT: 1 +(set-logic QF_BVLIA) +(declare-const x (_ BitVec 4)) +(assert (= (bv2nat x) 0)) +(check-sat) +(reset) +(set-logic QF_BV) +(declare-const x (_ BitVec 4)) +(assert (= (bv2nat x) 0)) +(check-sat) diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 85b379ac0..a829d9a8d 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -316,9 +316,6 @@ public: void setupContext(Parser& parser) override { - if(dynamic_cast(&parser) != NULL){ - dynamic_cast(&parser)->addTheory(Smt2::THEORY_CORE); - } super::setupContext(parser); }