diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 980 |
1 files changed, 507 insertions, 473 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 15fdd8461..73be8910f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -45,242 +45,236 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) } void Smt2::addArithmeticOperators() { - addOperator(kind::PLUS, "+"); - addOperator(kind::MINUS, "-"); - // kind::MINUS is converted to kind::UMINUS if there is only a single operand - Parser::addOperator(kind::UMINUS); - addOperator(kind::MULT, "*"); - addOperator(kind::LT, "<"); - addOperator(kind::LEQ, "<="); - addOperator(kind::GT, ">"); - addOperator(kind::GEQ, ">="); + addOperator(api::PLUS, "+"); + addOperator(api::MINUS, "-"); + // api::MINUS is converted to api::UMINUS if there is only a single operand + Parser::addOperator(api::UMINUS); + addOperator(api::MULT, "*"); + addOperator(api::LT, "<"); + addOperator(api::LEQ, "<="); + addOperator(api::GT, ">"); + addOperator(api::GEQ, ">="); if (!strictModeEnabled()) { // NOTE: this operator is non-standard - addOperator(kind::POW, "^"); + addOperator(api::POW, "^"); } } void Smt2::addTranscendentalOperators() { - addOperator(kind::EXPONENTIAL, "exp"); - addOperator(kind::SINE, "sin"); - addOperator(kind::COSINE, "cos"); - addOperator(kind::TANGENT, "tan"); - addOperator(kind::COSECANT, "csc"); - addOperator(kind::SECANT, "sec"); - addOperator(kind::COTANGENT, "cot"); - addOperator(kind::ARCSINE, "arcsin"); - addOperator(kind::ARCCOSINE, "arccos"); - addOperator(kind::ARCTANGENT, "arctan"); - addOperator(kind::ARCCOSECANT, "arccsc"); - addOperator(kind::ARCSECANT, "arcsec"); - addOperator(kind::ARCCOTANGENT, "arccot"); - addOperator(kind::SQRT, "sqrt"); + addOperator(api::EXPONENTIAL, "exp"); + addOperator(api::SINE, "sin"); + addOperator(api::COSINE, "cos"); + addOperator(api::TANGENT, "tan"); + addOperator(api::COSECANT, "csc"); + addOperator(api::SECANT, "sec"); + addOperator(api::COTANGENT, "cot"); + addOperator(api::ARCSINE, "arcsin"); + addOperator(api::ARCCOSINE, "arccos"); + addOperator(api::ARCTANGENT, "arctan"); + addOperator(api::ARCCOSECANT, "arccsc"); + addOperator(api::ARCSECANT, "arcsec"); + addOperator(api::ARCCOTANGENT, "arccot"); + addOperator(api::SQRT, "sqrt"); } void Smt2::addQuantifiersOperators() { if (!strictModeEnabled()) { - addOperator(kind::INST_CLOSURE, "inst-closure"); + addOperator(api::INST_CLOSURE, "inst-closure"); } } void Smt2::addBitvectorOperators() { - addOperator(kind::BITVECTOR_CONCAT, "concat"); - addOperator(kind::BITVECTOR_NOT, "bvnot"); - addOperator(kind::BITVECTOR_AND, "bvand"); - addOperator(kind::BITVECTOR_OR, "bvor"); - addOperator(kind::BITVECTOR_NEG, "bvneg"); - addOperator(kind::BITVECTOR_PLUS, "bvadd"); - addOperator(kind::BITVECTOR_MULT, "bvmul"); - addOperator(kind::BITVECTOR_UDIV, "bvudiv"); - addOperator(kind::BITVECTOR_UREM, "bvurem"); - addOperator(kind::BITVECTOR_SHL, "bvshl"); - addOperator(kind::BITVECTOR_LSHR, "bvlshr"); - addOperator(kind::BITVECTOR_ULT, "bvult"); - addOperator(kind::BITVECTOR_NAND, "bvnand"); - addOperator(kind::BITVECTOR_NOR, "bvnor"); - addOperator(kind::BITVECTOR_XOR, "bvxor"); - addOperator(kind::BITVECTOR_XNOR, "bvxnor"); - addOperator(kind::BITVECTOR_COMP, "bvcomp"); - addOperator(kind::BITVECTOR_SUB, "bvsub"); - addOperator(kind::BITVECTOR_SDIV, "bvsdiv"); - addOperator(kind::BITVECTOR_SREM, "bvsrem"); - addOperator(kind::BITVECTOR_SMOD, "bvsmod"); - addOperator(kind::BITVECTOR_ASHR, "bvashr"); - addOperator(kind::BITVECTOR_ULE, "bvule"); - addOperator(kind::BITVECTOR_UGT, "bvugt"); - addOperator(kind::BITVECTOR_UGE, "bvuge"); - addOperator(kind::BITVECTOR_SLT, "bvslt"); - addOperator(kind::BITVECTOR_SLE, "bvsle"); - addOperator(kind::BITVECTOR_SGT, "bvsgt"); - addOperator(kind::BITVECTOR_SGE, "bvsge"); - addOperator(kind::BITVECTOR_REDOR, "bvredor"); - addOperator(kind::BITVECTOR_REDAND, "bvredand"); - addOperator(kind::BITVECTOR_TO_NAT, "bv2nat"); - + addOperator(api::BITVECTOR_CONCAT, "concat"); + addOperator(api::BITVECTOR_NOT, "bvnot"); + addOperator(api::BITVECTOR_AND, "bvand"); + addOperator(api::BITVECTOR_OR, "bvor"); + addOperator(api::BITVECTOR_NEG, "bvneg"); + addOperator(api::BITVECTOR_PLUS, "bvadd"); + addOperator(api::BITVECTOR_MULT, "bvmul"); + addOperator(api::BITVECTOR_UDIV, "bvudiv"); + addOperator(api::BITVECTOR_UREM, "bvurem"); + addOperator(api::BITVECTOR_SHL, "bvshl"); + addOperator(api::BITVECTOR_LSHR, "bvlshr"); + addOperator(api::BITVECTOR_ULT, "bvult"); + addOperator(api::BITVECTOR_NAND, "bvnand"); + addOperator(api::BITVECTOR_NOR, "bvnor"); + addOperator(api::BITVECTOR_XOR, "bvxor"); + addOperator(api::BITVECTOR_XNOR, "bvxnor"); + addOperator(api::BITVECTOR_COMP, "bvcomp"); + addOperator(api::BITVECTOR_SUB, "bvsub"); + addOperator(api::BITVECTOR_SDIV, "bvsdiv"); + addOperator(api::BITVECTOR_SREM, "bvsrem"); + addOperator(api::BITVECTOR_SMOD, "bvsmod"); + addOperator(api::BITVECTOR_ASHR, "bvashr"); + addOperator(api::BITVECTOR_ULE, "bvule"); + addOperator(api::BITVECTOR_UGT, "bvugt"); + addOperator(api::BITVECTOR_UGE, "bvuge"); + addOperator(api::BITVECTOR_SLT, "bvslt"); + addOperator(api::BITVECTOR_SLE, "bvsle"); + addOperator(api::BITVECTOR_SGT, "bvsgt"); + 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"); addIndexedOperator( - kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); - addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); + api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); addIndexedOperator( - kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); + api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); addIndexedOperator( - kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); + api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); addIndexedOperator( - kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); - addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT, - api::BITVECTOR_ROTATE_RIGHT, - "rotate_right"); - addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); + api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); + addIndexedOperator(api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); } 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(api::APPLY_CONSTRUCTOR); + Parser::addOperator(api::APPLY_TESTER); + Parser::addOperator(api::APPLY_SELECTOR); if (!strictModeEnabled()) { - addOperator(kind::DT_SIZE, "dt.size"); + addOperator(api::DT_SIZE, "dt.size"); } } void Smt2::addStringOperators() { - defineVar("re.all", - getSolver() - ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()) - .getExpr()); - - addOperator(kind::STRING_CONCAT, "str.++"); - addOperator(kind::STRING_LENGTH, "str.len"); - addOperator(kind::STRING_SUBSTR, "str.substr" ); - addOperator(kind::STRING_STRCTN, "str.contains" ); - addOperator(kind::STRING_CHARAT, "str.at" ); - addOperator(kind::STRING_STRIDOF, "str.indexof" ); - addOperator(kind::STRING_STRREPL, "str.replace" ); + defineVar( + "re.all", + getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())); + addOperator(api::STRING_CONCAT, "str.++"); + addOperator(api::STRING_LENGTH, "str.len"); + addOperator(api::STRING_SUBSTR, "str.substr"); + addOperator(api::STRING_STRCTN, "str.contains"); + addOperator(api::STRING_CHARAT, "str.at"); + addOperator(api::STRING_STRIDOF, "str.indexof"); + addOperator(api::STRING_STRREPL, "str.replace"); if (!strictModeEnabled()) { - addOperator(kind::STRING_TOLOWER, "str.tolower"); - addOperator(kind::STRING_TOUPPER, "str.toupper"); - addOperator(kind::STRING_REV, "str.rev"); - } - addOperator(kind::STRING_PREFIX, "str.prefixof" ); - addOperator(kind::STRING_SUFFIX, "str.suffixof" ); - addOperator(kind::STRING_FROM_CODE, "str.from_code"); - addOperator(kind::STRING_IS_DIGIT, "str.is_digit" ); - + addOperator(api::STRING_TOLOWER, "str.tolower"); + addOperator(api::STRING_TOUPPER, "str.toupper"); + addOperator(api::STRING_REV, "str.rev"); + } + addOperator(api::STRING_PREFIX, "str.prefixof"); + addOperator(api::STRING_SUFFIX, "str.suffixof"); + addOperator(api::STRING_FROM_CODE, "str.from_code"); + addOperator(api::STRING_IS_DIGIT, "str.is_digit"); // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 || getLanguage() == language::input::LANG_SYGUS_V2) { - addOperator(kind::STRING_ITOS, "str.from_int"); - addOperator(kind::STRING_STOI, "str.to_int"); - addOperator(kind::STRING_IN_REGEXP, "str.in_re"); - addOperator(kind::STRING_TO_REGEXP, "str.to_re"); - addOperator(kind::STRING_TO_CODE, "str.to_code"); - addOperator(kind::STRING_STRREPLALL, "str.replace_all"); + addOperator(api::STRING_ITOS, "str.from_int"); + addOperator(api::STRING_STOI, "str.to_int"); + addOperator(api::STRING_IN_REGEXP, "str.in_re"); + addOperator(api::STRING_TO_REGEXP, "str.to_re"); + addOperator(api::STRING_TO_CODE, "str.to_code"); + addOperator(api::STRING_STRREPLALL, "str.replace_all"); } else { - addOperator(kind::STRING_ITOS, "int.to.str"); - addOperator(kind::STRING_STOI, "str.to.int"); - addOperator(kind::STRING_IN_REGEXP, "str.in.re"); - addOperator(kind::STRING_TO_REGEXP, "str.to.re"); - addOperator(kind::STRING_TO_CODE, "str.code"); - addOperator(kind::STRING_STRREPLALL, "str.replaceall"); - } - - addOperator(kind::REGEXP_CONCAT, "re.++"); - addOperator(kind::REGEXP_UNION, "re.union"); - addOperator(kind::REGEXP_INTER, "re.inter"); - addOperator(kind::REGEXP_STAR, "re.*"); - addOperator(kind::REGEXP_PLUS, "re.+"); - addOperator(kind::REGEXP_OPT, "re.opt"); - addOperator(kind::REGEXP_RANGE, "re.range"); - addOperator(kind::REGEXP_LOOP, "re.loop"); - addOperator(kind::REGEXP_COMPLEMENT, "re.comp"); - addOperator(kind::REGEXP_DIFF, "re.diff"); - addOperator(kind::STRING_LT, "str.<"); - addOperator(kind::STRING_LEQ, "str.<="); + addOperator(api::STRING_ITOS, "int.to.str"); + addOperator(api::STRING_STOI, "str.to.int"); + addOperator(api::STRING_IN_REGEXP, "str.in.re"); + addOperator(api::STRING_TO_REGEXP, "str.to.re"); + addOperator(api::STRING_TO_CODE, "str.code"); + addOperator(api::STRING_STRREPLALL, "str.replaceall"); + } + + addOperator(api::REGEXP_CONCAT, "re.++"); + addOperator(api::REGEXP_UNION, "re.union"); + addOperator(api::REGEXP_INTER, "re.inter"); + addOperator(api::REGEXP_STAR, "re.*"); + addOperator(api::REGEXP_PLUS, "re.+"); + addOperator(api::REGEXP_OPT, "re.opt"); + addOperator(api::REGEXP_RANGE, "re.range"); + addOperator(api::REGEXP_LOOP, "re.loop"); + addOperator(api::REGEXP_COMPLEMENT, "re.comp"); + addOperator(api::REGEXP_DIFF, "re.diff"); + addOperator(api::STRING_LT, "str.<"); + addOperator(api::STRING_LEQ, "str.<="); } void Smt2::addFloatingPointOperators() { - addOperator(kind::FLOATINGPOINT_FP, "fp"); - addOperator(kind::FLOATINGPOINT_EQ, "fp.eq"); - addOperator(kind::FLOATINGPOINT_ABS, "fp.abs"); - addOperator(kind::FLOATINGPOINT_NEG, "fp.neg"); - addOperator(kind::FLOATINGPOINT_PLUS, "fp.add"); - addOperator(kind::FLOATINGPOINT_SUB, "fp.sub"); - addOperator(kind::FLOATINGPOINT_MULT, "fp.mul"); - addOperator(kind::FLOATINGPOINT_DIV, "fp.div"); - addOperator(kind::FLOATINGPOINT_FMA, "fp.fma"); - addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt"); - addOperator(kind::FLOATINGPOINT_REM, "fp.rem"); - addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral"); - addOperator(kind::FLOATINGPOINT_MIN, "fp.min"); - addOperator(kind::FLOATINGPOINT_MAX, "fp.max"); - addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq"); - addOperator(kind::FLOATINGPOINT_LT, "fp.lt"); - addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq"); - addOperator(kind::FLOATINGPOINT_GT, "fp.gt"); - addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal"); - addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal"); - addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero"); - addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite"); - addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN"); - addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative"); - addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive"); - addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real"); - - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC, + addOperator(api::FLOATINGPOINT_FP, "fp"); + addOperator(api::FLOATINGPOINT_EQ, "fp.eq"); + addOperator(api::FLOATINGPOINT_ABS, "fp.abs"); + addOperator(api::FLOATINGPOINT_NEG, "fp.neg"); + addOperator(api::FLOATINGPOINT_PLUS, "fp.add"); + addOperator(api::FLOATINGPOINT_SUB, "fp.sub"); + addOperator(api::FLOATINGPOINT_MULT, "fp.mul"); + addOperator(api::FLOATINGPOINT_DIV, "fp.div"); + addOperator(api::FLOATINGPOINT_FMA, "fp.fma"); + addOperator(api::FLOATINGPOINT_SQRT, "fp.sqrt"); + addOperator(api::FLOATINGPOINT_REM, "fp.rem"); + addOperator(api::FLOATINGPOINT_RTI, "fp.roundToIntegral"); + addOperator(api::FLOATINGPOINT_MIN, "fp.min"); + addOperator(api::FLOATINGPOINT_MAX, "fp.max"); + addOperator(api::FLOATINGPOINT_LEQ, "fp.leq"); + addOperator(api::FLOATINGPOINT_LT, "fp.lt"); + addOperator(api::FLOATINGPOINT_GEQ, "fp.geq"); + addOperator(api::FLOATINGPOINT_GT, "fp.gt"); + addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal"); + addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal"); + addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero"); + addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite"); + addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN"); + addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative"); + addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive"); + addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real"); + + addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, "to_fp_unsigned"); addIndexedOperator( - kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); + api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); addIndexedOperator( - kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); + api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); if (!strictModeEnabled()) { - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, "to_fp_bv"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, "to_fp_fp"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL, api::FLOATINGPOINT_TO_FP_REAL, "to_fp_real"); - addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, "to_fp_signed"); } } void Smt2::addSepOperators() { - addOperator(kind::SEP_STAR, "sep"); - addOperator(kind::SEP_PTO, "pto"); - addOperator(kind::SEP_WAND, "wand"); - addOperator(kind::SEP_EMP, "emp"); - Parser::addOperator(kind::SEP_STAR); - Parser::addOperator(kind::SEP_PTO); - Parser::addOperator(kind::SEP_WAND); - Parser::addOperator(kind::SEP_EMP); + addOperator(api::SEP_STAR, "sep"); + addOperator(api::SEP_PTO, "pto"); + addOperator(api::SEP_WAND, "wand"); + addOperator(api::SEP_EMP, "emp"); + Parser::addOperator(api::SEP_STAR); + Parser::addOperator(api::SEP_PTO); + Parser::addOperator(api::SEP_WAND); + Parser::addOperator(api::SEP_EMP); } void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_ARRAYS: - addOperator(kind::SELECT, "select"); - addOperator(kind::STORE, "store"); + addOperator(api::SELECT, "select"); + addOperator(api::STORE, "store"); break; case THEORY_BITVECTORS: @@ -288,145 +282,132 @@ void Smt2::addTheory(Theory theory) { break; case THEORY_CORE: - defineType("Bool", getExprManager()->booleanType()); - defineVar("true", getExprManager()->mkConst(true)); - defineVar("false", getExprManager()->mkConst(false)); - 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"); + 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", getExprManager()->realType()); - addOperator(kind::DIVISION, "/"); - addOperator(kind::TO_INTEGER, "to_int"); - addOperator(kind::IS_INTEGER, "is_int"); - addOperator(kind::TO_REAL, "to_real"); + 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", getExprManager()->integerType()); + defineType("Int", d_solver->getIntegerSort()); addArithmeticOperators(); - addOperator(kind::INTS_DIVISION, "div"); - addOperator(kind::INTS_MODULUS, "mod"); - addOperator(kind::ABS, "abs"); - addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible"); + 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", getExprManager()->realType()); + defineType("Real", d_solver->getRealSort()); addArithmeticOperators(); - addOperator(kind::DIVISION, "/"); + addOperator(api::DIVISION, "/"); if (!strictModeEnabled()) { - addOperator(kind::ABS, "abs"); + addOperator(api::ABS, "abs"); } break; case THEORY_TRANSCENDENTALS: - defineVar("real.pi", - getExprManager()->mkNullaryOperator(getExprManager()->realType(), - CVC4::kind::PI)); + 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()).getExpr()); + 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()).getExpr()); - - addOperator(kind::UNION, "union"); - addOperator(kind::INTERSECTION, "intersection"); - addOperator(kind::SETMINUS, "setminus"); - addOperator(kind::SUBSET, "subset"); - addOperator(kind::MEMBER, "member"); - addOperator(kind::SINGLETON, "singleton"); - addOperator(kind::INSERT, "insert"); - addOperator(kind::CARD, "card"); - addOperator(kind::COMPLEMENT, "complement"); - addOperator(kind::JOIN, "join"); - addOperator(kind::PRODUCT, "product"); - addOperator(kind::TRANSPOSE, "transpose"); - addOperator(kind::TCLOSURE, "tclosure"); + 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<Type> types; - defineType("Tuple", getExprManager()->mkTupleType(types)); + const std::vector<api::Sort> types; + defineType("Tuple", d_solver->mkTupleSort(types)); addDatatypesOperators(); break; } case THEORY_STRINGS: - defineType("String", getExprManager()->stringType()); - defineType("RegLan", getExprManager()->regExpType()); - defineType("Int", getExprManager()->integerType()); + 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().getExpr()); + defineVar("re.none", d_solver->mkRegexpEmpty()); } else { - defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr()); + defineVar("re.nostr", d_solver->mkRegexpEmpty()); } - defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr()); + defineVar("re.allchar", d_solver->mkRegexpSigma()); addStringOperators(); break; case THEORY_UF: - Parser::addOperator(kind::APPLY_UF); + Parser::addOperator(api::APPLY_UF); if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) { - addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card"); - addOperator(kind::CARDINALITY_VALUE, "fmf.card.val"); + addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card"); + addOperator(api::CARDINALITY_VALUE, "fmf.card.val"); } break; case THEORY_FP: - defineType("RoundingMode", getExprManager()->roundingModeType()); - defineType("Float16", getExprManager()->mkFloatingPointType(5, 11)); - 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()); + 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).getExpr()); - defineVar("RTN", - d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr()); + 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).getExpr()); - defineVar("RTZ", - d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr()); + 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).getExpr()); + d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); addFloatingPointOperators(); break; @@ -434,8 +415,7 @@ void Smt2::addTheory(Theory theory) { 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()); + defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); addSepOperators(); break; @@ -447,14 +427,15 @@ void Smt2::addTheory(Theory theory) { } } -void Smt2::addOperator(Kind kind, const std::string& name) { +void Smt2::addOperator(api::Kind kind, const std::string& name) +{ Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" << std::endl; Parser::addOperator(kind); operatorKindMap[name] = kind; } -void Smt2::addIndexedOperator(Kind tKind, +void Smt2::addIndexedOperator(api::Kind tKind, api::Kind opKind, const std::string& name) { @@ -462,7 +443,8 @@ void Smt2::addIndexedOperator(Kind tKind, d_indexedOpKindMap[name] = opKind; } -Kind Smt2::getOperatorKind(const std::string& name) const { +api::Kind Smt2::getOperatorKind(const std::string& name) const +{ // precondition: isOperatorEnabled(name) return operatorKindMap.find(name)->second; } @@ -513,7 +495,9 @@ bool Smt2::logicIsSet() { return d_logicSet; } -Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) { +api::Term Smt2::getExpressionForNameAndType(const std::string& name, + api::Sort t) +{ if (isAbstractValue(name)) { return mkAbstractValue(name); @@ -581,40 +565,40 @@ api::Op Smt2::mkIndexedOp(const std::string& name, return api::Op(); } -Expr Smt2::mkDefineFunRec( +api::Term Smt2::bindDefineFunRec( const std::string& fname, - const std::vector<std::pair<std::string, Type> >& sortedVarNames, - Type t, - std::vector<Expr>& flattenVars) + const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, + api::Sort t, + std::vector<api::Term>& flattenVars) { - std::vector<Type> sorts; - for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames) + std::vector<api::Sort> sorts; + for (const std::pair<std::string, api::Sort>& svn : sortedVarNames) { sorts.push_back(svn.second); } // make the flattened function type, add bound variables // to flattenVars if the defined function was given a function return type. - Type ft = mkFlatFunctionType(sorts, t, flattenVars); + api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars); // allow overloading - return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true); + return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true); } void Smt2::pushDefineFunRecScope( - const std::vector<std::pair<std::string, Type> >& sortedVarNames, - Expr func, - const std::vector<Expr>& flattenVars, - std::vector<Expr>& bvs, + const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, + api::Term func, + const std::vector<api::Term>& flattenVars, + std::vector<api::Term>& bvs, bool bindingLevel) { pushScope(bindingLevel); // bound variables are those that are explicitly named in the preamble // of the define-fun(s)-rec command, we define them here - for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames) + for (const std::pair<std::string, api::Sort>& svn : sortedVarNames) { - Expr v = mkBoundVar(svn.first, svn.second); + api::Term v = bindBoundVar(svn.first, svn.second); bvs.push_back(v); } @@ -626,7 +610,7 @@ void Smt2::reset() { d_seenSetLogic = false; d_logic = LogicInfo(); operatorKindMap.clear(); - d_lastNamedTerm = std::pair<Expr, std::string>(); + d_lastNamedTerm = std::pair<api::Term, std::string>(); this->Parser::reset(); if( !strictModeEnabled() ) { @@ -645,8 +629,8 @@ Smt2::SynthFunFactory::SynthFunFactory( Smt2* smt2, const std::string& fun, bool isInv, - Type range, - std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames) + api::Sort range, + std::vector<std::pair<std::string, api::Sort>>& sortedVarNames) : d_smt2(smt2), d_fun(fun), d_isInv(isInv) { if (range.isNull()) @@ -657,38 +641,37 @@ Smt2::SynthFunFactory::SynthFunFactory( { smt2->parseError("Cannot use synth-fun with function return type."); } - std::vector<Type> varSorts; - for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames) + std::vector<api::Sort> varSorts; + for (const std::pair<std::string, api::Sort>& p : sortedVarNames) { varSorts.push_back(p.second); } Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; - Type synthFunType = - varSorts.size() > 0 - ? d_smt2->getExprManager()->mkFunctionType(varSorts, range) - : range; + api::Sort synthFunType = + varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range) + : range; // we do not allow overloading for synth fun - d_synthFun = d_smt2->mkBoundVar(fun, synthFunType); + d_synthFun = d_smt2->bindBoundVar(fun, synthFunType); // set the sygus type to be range by default, which is overwritten below // if a grammar is provided d_sygusType = range; d_smt2->pushScope(true); - d_sygusVars = d_smt2->mkBoundVars(sortedVarNames); + d_sygusVars = d_smt2->bindBoundVars(sortedVarNames); } Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); } -std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar) +std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Sort grammar) { Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl; - return std::unique_ptr<Command>( - new SynthFunCommand(d_fun, - d_synthFun, - grammar.isNull() ? d_sygusType : grammar, - d_isInv, - d_sygusVars)); + return std::unique_ptr<Command>(new SynthFunCommand( + d_fun, + d_synthFun.getExpr(), + grammar.isNull() ? d_sygusType.getType() : grammar.getType(), + d_isInv, + api::termVectorToExprs(d_sygusVars))); } std::unique_ptr<Command> Smt2::invConstraint( @@ -705,7 +688,7 @@ std::unique_ptr<Command> Smt2::invConstraint( "arguments."); } - std::vector<Expr> terms; + std::vector<api::Term> terms; for (const std::string& name : names) { if (!isDeclared(name)) @@ -718,7 +701,8 @@ std::unique_ptr<Command> Smt2::invConstraint( terms.push_back(getVariable(name)); } - return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms)); + return std::unique_ptr<Command>( + new SygusInvConstraintCommand(api::termVectorToExprs(terms))); } Command* Smt2::setLogic(std::string name, bool fromCommand) @@ -932,33 +916,32 @@ void Smt2::includeFile(const std::string& filename) { parseError("Couldn't open include file `" + path + "'"); } } - bool Smt2::isAbstractValue(const std::string& name) { return name.length() >= 2 && name[0] == '@' && name[1] != '0' && name.find_first_not_of("0123456789", 1) == std::string::npos; } -Expr Smt2::mkAbstractValue(const std::string& name) +api::Term Smt2::mkAbstractValue(const std::string& name) { assert(isAbstractValue(name)); // remove the '@' - return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); + return d_solver->mkAbstractValue(name.substr(1)); } -void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) { +void Smt2::mkSygusConstantsForType(const api::Sort& type, + std::vector<api::Term>& ops) +{ if( type.isInteger() ){ - ops.push_back(getExprManager()->mkConst(Rational(0))); - ops.push_back(getExprManager()->mkConst(Rational(1))); + ops.push_back(d_solver->mkReal(0)); + ops.push_back(d_solver->mkReal(1)); }else if( type.isBitVector() ){ - unsigned sz = ((BitVectorType)type).getSize(); - BitVector bval0(sz, (unsigned int)0); - ops.push_back( getExprManager()->mkConst(bval0) ); - BitVector bval1(sz, (unsigned int)1); - ops.push_back( getExprManager()->mkConst(bval1) ); + uint32_t sz = type.getBVSize(); + ops.push_back(d_solver->mkBitVector(sz, 0)); + ops.push_back(d_solver->mkBitVector(sz, 1)); }else if( type.isBoolean() ){ - ops.push_back(getExprManager()->mkConst(true)); - ops.push_back(getExprManager()->mkConst(false)); + ops.push_back(d_solver->mkTrue()); + ops.push_back(d_solver->mkFalse()); } //TODO : others? } @@ -969,36 +952,37 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym, - const std::vector<CVC4::Expr>& sygus_vars, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, - std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, - CVC4::Type& ret, + const std::vector<api::Term>& sygus_vars, + std::map<api::Sort, api::Sort>& sygus_to_builtin, + std::map<api::Sort, api::Term>& sygus_to_builtin_expr, + api::Sort& ret, bool isNested) { if (sgt.d_gterm_type == SygusGTerm::gterm_op) { Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype " << index << std::endl; - Kind oldKind; - Kind newKind = kind::UNDEFINED_KIND; + api::Kind oldKind; + api::Kind newKind = api::UNDEFINED_KIND; //convert to UMINUS if one child of MINUS - if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS) + if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == api::MINUS) { - oldKind = kind::MINUS; - newKind = kind::UMINUS; + oldKind = api::MINUS; + newKind = api::UMINUS; } - if( newKind!=kind::UNDEFINED_KIND ){ + if (newKind != api::UNDEFINED_KIND) + { Debug("parser-sygus") << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl; sgt.d_op.d_kind = newKind; - std::string oldName = kind::kindToString(oldKind); - std::string newName = kind::kindToString(newKind); + std::string oldName = api::kindToString(oldKind); + std::string newName = api::kindToString(newKind); size_t pos = 0; if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){ sgt.d_name.replace(pos, oldName.length(), newName); @@ -1006,22 +990,32 @@ void Smt2::processSygusGTerm( } ops[index].push_back(sgt.d_op); cnames[index].push_back( sgt.d_name ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back(std::vector<api::Sort>()); for( unsigned i=0; i<sgt.d_children.size(); i++ ){ std::stringstream ss; ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i; std::string sub_dname = ss.str(); //add datatype for child - Type null_type; + api::Sort null_type; pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); int sub_dt_index = datatypes.size()-1; //process child - Type sub_ret; + api::Sort sub_ret; processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true ); //process the nested gterm (either pop the last datatype, or flatten the argument) - Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + api::Sort tt = processSygusNestedGTerm(sub_dt_index, + sub_dname, + datatypes, + sorts, + ops, + cnames, + cargs, + allow_const, + unresolved_gterm_sym, + sygus_to_builtin, + sygus_to_builtin_expr, + sub_ret); cargs[index].back().push_back(tt); } } @@ -1030,7 +1024,7 @@ void Smt2::processSygusGTerm( if( sgt.getNumChildren()!=0 ){ parseError("Bad syntax for Sygus Constant."); } - std::vector< Expr > consts; + std::vector<api::Term> consts; mkSygusConstantsForType( sgt.d_type, consts ); Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; for( unsigned i=0; i<consts.size(); i++ ){ @@ -1041,7 +1035,7 @@ void Smt2::processSygusGTerm( constOp.d_expr = consts[i]; ops[index].push_back(constOp); cnames[index].push_back( ss.str() ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back(std::vector<api::Sort>()); } allow_const[index] = true; } @@ -1053,7 +1047,8 @@ void Smt2::processSygusGTerm( } Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; for( unsigned i=0; i<sygus_vars.size(); i++ ){ - if( sygus_vars[i].getType()==sgt.d_type ){ + if (sygus_vars[i].getSort() == sgt.d_type) + { std::stringstream ss; ss << sygus_vars[i]; Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; @@ -1061,7 +1056,7 @@ void Smt2::processSygusGTerm( varOp.d_expr = sygus_vars[i]; ops[index].push_back(varOp); cnames[index].push_back( ss.str() ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back(std::vector<api::Sort>()); } } } @@ -1092,13 +1087,13 @@ void Smt2::processSygusGTerm( } bool Smt2::pushSygusDatatypeDef( - Type t, + api::Sort t, std::string& dname, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym) { @@ -1106,7 +1101,7 @@ bool Smt2::pushSygusDatatypeDef( datatypes.push_back(Datatype(getExprManager(), dname)); ops.push_back(std::vector<ParseOp>()); cnames.push_back(std::vector<std::string>()); - cargs.push_back(std::vector<std::vector<CVC4::Type> >()); + cargs.push_back(std::vector<std::vector<api::Sort>>()); allow_const.push_back(false); unresolved_gterm_sym.push_back(std::vector< std::string >()); return true; @@ -1114,10 +1109,10 @@ bool Smt2::pushSygusDatatypeDef( bool Smt2::popSygusDatatypeDef( std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym) { @@ -1131,21 +1126,21 @@ bool Smt2::popSygusDatatypeDef( return true; } -Type Smt2::processSygusNestedGTerm( +api::Sort Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops, std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<std::vector<std::vector<api::Sort>>>& cargs, std::vector<bool>& allow_const, std::vector<std::vector<std::string>>& unresolved_gterm_sym, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, - std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, - Type sub_ret) + std::map<api::Sort, api::Sort>& sygus_to_builtin, + std::map<api::Sort, CVC4::api::Term>& sygus_to_builtin_expr, + api::Sort sub_ret) { - Type t = sub_ret; + api::Sort t = sub_ret; Debug("parser-sygus") << "Argument is "; if( t.isNull() ){ //then, it is the datatype we constructed, which should have a single constructor @@ -1156,13 +1151,16 @@ Type Smt2::processSygusNestedGTerm( parseError(std::string("Internal error : datatype for nested gterm does not have a constructor.")); } ParseOp op = ops[sub_dt_index][0]; - Type curr_t; + api::Sort curr_t; if (!op.d_expr.isNull() && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty())) { - Expr sop = op.d_expr; - curr_t = sop.getType(); - Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl; + api::Term sop = op.d_expr; + curr_t = sop.getSort(); + Debug("parser-sygus") + << ": it is constant/0-arg cons " << sop << " with type " + << sop.getSort() << ", debug=" << sop.isConst() << " " + << cargs[sub_dt_index][0].size() << std::endl; // only cache if it is a singleton datatype (has unique expr) if (ops[sub_dt_index].size() == 1) { @@ -1176,24 +1174,29 @@ Type Smt2::processSygusNestedGTerm( } else { - std::vector< Expr > children; + std::vector<api::Term> children; for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){ - std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] ); + std::map<api::Sort, CVC4::api::Term>::iterator it = + sygus_to_builtin_expr.find(cargs[sub_dt_index][0][i]); if( it==sygus_to_builtin_expr.end() ){ if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){ std::stringstream ss; ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl; ss << "Builtin types are currently : " << std::endl; - for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){ + for (std::map<api::Sort, api::Sort>::iterator itb = + sygus_to_builtin.begin(); + itb != sygus_to_builtin.end(); + ++itb) + { ss << " " << itb->first << " -> " << itb->second << std::endl; } parseError(ss.str()); } - Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; + api::Sort bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; std::stringstream ss; ss << t << "_x_" << i; - Expr bv = mkBoundVar(ss.str(), bt); + api::Term bv = bindBoundVar(ss.str(), bt); children.push_back( bv ); d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i]; }else{ @@ -1201,9 +1204,10 @@ Type Smt2::processSygusNestedGTerm( children.push_back( it->second ); } } - Expr e = applyParseOp(op, children); - Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl; - curr_t = e.getType(); + api::Term e = applyParseOp(op, children); + Debug("parser-sygus") << ": constructed " << e << ", which has type " + << e.getSort() << std::endl; + curr_t = e.getSort(); sygus_to_builtin_expr[t] = e; } sorts[sub_dt_index] = curr_t; @@ -1221,12 +1225,12 @@ Type Smt2::processSygusNestedGTerm( void Smt2::setSygusStartIndex(const std::string& fun, int startIndex, std::vector<CVC4::Datatype>& datatypes, - std::vector<CVC4::Type>& sorts, + std::vector<api::Sort>& sorts, std::vector<std::vector<ParseOp>>& ops) { if( startIndex>0 ){ CVC4::Datatype tmp_dt = datatypes[0]; - Type tmp_sort = sorts[0]; + api::Sort tmp_sort = sorts[0]; std::vector<ParseOp> tmp_ops; tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); datatypes[0] = datatypes[startIndex]; @@ -1247,9 +1251,9 @@ void Smt2::setSygusStartIndex(const std::string& fun, void Smt2::mkSygusDatatype(CVC4::Datatype& dt, std::vector<ParseOp>& ops, std::vector<std::string>& cnames, - std::vector<std::vector<CVC4::Type>>& cargs, + std::vector<std::vector<api::Sort>>& cargs, std::vector<std::string>& unresolved_gterm_sym, - std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin) + std::map<api::Sort, api::Sort>& sygus_to_builtin) { Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; @@ -1295,28 +1299,29 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << std::endl; // make into define-fun - std::vector<Type> ltypes; + std::vector<api::Sort> ltypes; for (unsigned j = 0, size = cargs[i].size(); j < size; j++) { ltypes.push_back(sygus_to_builtin[cargs[i][j]]); } - std::vector<Expr> largs; - Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); + std::vector<api::Term> largs; + api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); // make the let_body - Expr body = applyParseOp(ops[i], largs); + api::Term body = applyParseOp(ops[i], largs); // replace by lambda ParseOp pLam; - pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + pLam.d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); ops[i] = pLam; Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; // callback prints as the expression - spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs); + spc = std::make_shared<printer::SygusExprPrintCallback>( + body.getExpr(), api::termVectorToExprs(largs)); } else { - Expr sop = ops[i].d_expr; - if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst()) + api::Term sop = ops[i].d_expr; + if (!sop.isNull() && sop.getSort().isBitVector() && sop.isConst()) { Debug("parser-sygus") << "--> Bit-vector constant " << sop << " (" << cnames[i] << ")" << std::endl; @@ -1326,22 +1331,22 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, // the given name. spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); } - else if (!sop.isNull() && sop.getKind() == kind::VARIABLE) + else if (!sop.isNull() && sop.getKind() == api::VARIABLE) { Debug("parser-sygus") << "--> Defined function " << ops[i] << std::endl; // turn f into (lammbda (x) (f x)) // in a degenerate case, ops[i] may be a defined constant, // in which case we do not replace by a lambda. - if (sop.getType().isFunction()) + if (sop.getSort().isFunction()) { - std::vector<Type> ftypes = - static_cast<FunctionType>(sop.getType()).getArgTypes(); - std::vector<Expr> largs; - Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); + std::vector<api::Sort> ftypes = + sop.getSort().getFunctionDomainSorts(); + std::vector<api::Term> largs; + api::Term lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); largs.insert(largs.begin(), sop); - Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs); - ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + api::Term body = d_solver->mkTerm(api::APPLY_UF, largs); + ops[i].d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } @@ -1364,15 +1369,22 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, cnames[i] = ss.str(); Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." << std::endl; + // Add the sygus constructor, either using the expression operator of // ops[i], or the kind. if (!ops[i].d_expr.isNull()) { - dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc); + dt.addSygusConstructor(ops[i].d_expr.getExpr(), + cnames[i], + api::sortVectorToTypes(cargs[i]), + spc); } - else if (ops[i].d_kind != kind::NULL_EXPR) + else if (ops[i].d_kind != api::NULL_EXPR) { - dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc); + dt.addSygusConstructor(extToIntKind(ops[i].d_kind), + cnames[i], + api::sortVectorToTypes(cargs[i]), + spc); } else { @@ -1387,36 +1399,38 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl; if( !unresolved_gterm_sym.empty() ){ - std::vector< Type > types; + std::vector<api::Sort> types; Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl; for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){ Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl; if( isUnresolvedType(unresolved_gterm_sym[i]) ){ Debug("parser-sygus") << " it is an unresolved type." << std::endl; - Type t = getSort(unresolved_gterm_sym[i]); + api::Sort t = getSort(unresolved_gterm_sym[i]); if( std::find( types.begin(), types.end(), t )==types.end() ){ types.push_back( t ); //identity element - Type bt = dt.getSygusType(); + api::Sort bt = dt.getSygusType(); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; std::stringstream ss; ss << t << "_x"; - Expr var = mkBoundVar(ss.str(), bt); - std::vector<Expr> lchildren; - lchildren.push_back( - getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var)); + api::Term var = bindBoundVar(ss.str(), bt); + std::vector<api::Term> lchildren; + lchildren.push_back(d_solver->mkTerm(api::BOUND_VAR_LIST, var)); lchildren.push_back(var); - Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren); + api::Term id_op = d_solver->mkTerm(api::LAMBDA, lchildren); // empty sygus callback (should not be printed) std::shared_ptr<SygusPrintCallback> sepc = std::make_shared<printer::SygusEmptyPrintCallback>(); //make the sygus argument list - std::vector< Type > id_carg; + std::vector<api::Sort> id_carg; id_carg.push_back( t ); - dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc); + dt.addSygusConstructor(id_op.getExpr(), + unresolved_gterm_sym[i], + api::sortVectorToTypes(id_carg), + sepc); //add to operators ParseOp idOp; @@ -1432,31 +1446,30 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, } } -Expr Smt2::makeSygusBoundVarList(Datatype& dt, - unsigned i, - const std::vector<Type>& ltypes, - std::vector<Expr>& lvars) +api::Term Smt2::makeSygusBoundVarList(CVC4::Datatype& dt, + unsigned i, + const std::vector<api::Sort>& ltypes, + std::vector<api::Term>& lvars) { for (unsigned j = 0, size = ltypes.size(); j < size; j++) { std::stringstream ss; ss << dt.getName() << "_x_" << i << "_" << j; - Expr v = mkBoundVar(ss.str(), ltypes[j]); + api::Term v = bindBoundVar(ss.str(), ltypes[j]); lvars.push_back(v); } - return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); + return d_solver->mkTerm(api::BOUND_VAR_LIST, lvars); } -void Smt2::addSygusConstructorTerm(Datatype& dt, - Expr term, - std::map<Expr, Type>& ntsToUnres) const +void Smt2::addSygusConstructorTerm( + Datatype& dt, + api::Term term, + std::map<api::Term, api::Sort>& ntsToUnres) const { Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl; - // Ensure that we do type checking here to catch sygus constructors with - // malformed builtin operators. The argument "true" to getType here forces - // a recursive well-typedness check. - term.getType(true); - // purify each occurrence of a non-terminal symbol in term, replace by + // At this point, we should know that dt is well founded, and that its + // builtin sygus operators are well-typed. + // Now, purify each occurrence of a non-terminal symbol in term, replace by // free variables. These become arguments to constructors. Notice we must do // a tree traversal in this function, since unique paths to the same term // should be treated as distinct terms. @@ -1464,7 +1477,7 @@ void Smt2::addSygusConstructorTerm(Datatype& dt, // this does not lead to exponential behavior with respect to input size. std::vector<api::Term> args; std::vector<api::Sort> cargs; - api::Term op = purifySygusGTerm(api::Term(term), ntsToUnres, args, cargs); + api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs); std::stringstream ssCName; ssCName << op.getKind(); Trace("parser-sygus2") << "Purified operator " << op @@ -1487,14 +1500,14 @@ void Smt2::addSygusConstructorTerm(Datatype& dt, } api::Term Smt2::purifySygusGTerm(api::Term term, - std::map<Expr, Type>& ntsToUnres, + std::map<api::Term, api::Sort>& ntsToUnres, std::vector<api::Term>& args, std::vector<api::Sort>& cargs) const { Trace("parser-sygus2-debug") << "purifySygusGTerm: " << term << " #nchild=" << term.getExpr().getNumChildren() << std::endl; - std::map<Expr, Type>::iterator itn = ntsToUnres.find(term.getExpr()); + std::map<api::Term, api::Sort>::iterator itn = ntsToUnres.find(term); if (itn != ntsToUnres.end()) { api::Term ret = d_solver->mkVar(term.getSort()); @@ -1526,35 +1539,35 @@ api::Term Smt2::purifySygusGTerm(api::Term term, } void Smt2::addSygusConstructorVariables(Datatype& dt, - const std::vector<Expr>& sygusVars, - Type type) const + const std::vector<api::Term>& sygusVars, + api::Sort type) const { // each variable of appropriate type becomes a sygus constructor in dt. for (unsigned i = 0, size = sygusVars.size(); i < size; i++) { - Expr v = sygusVars[i]; - if (v.getType() == type) + api::Term v = sygusVars[i]; + if (v.getSort() == type) { std::stringstream ss; ss << v; - std::vector<CVC4::Type> cargs; - dt.addSygusConstructor(v, ss.str(), cargs); + std::vector<api::Sort> cargs; + dt.addSygusConstructor( + v.getExpr(), ss.str(), api::sortVectorToTypes(cargs)); } } } InputLanguage Smt2::getLanguage() const { - ExprManager* em = getExprManager(); - return em->getOptions().getInputLanguage(); + return getExprManager()->getOptions().getInputLanguage(); } -void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) +void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) { Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type << std::endl; // (as const (Array T1 T2)) - if (p.d_kind == kind::STORE_ALL) + if (p.d_kind == api::STORE_ALL) { if (!type.isArray()) { @@ -1576,6 +1589,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) if (isDeclared(p.d_name, SYM_VARIABLE)) { p.d_expr = getExpressionForNameAndType(p.d_name, type); + p.d_name = std::string(""); } if (p.d_expr.isNull()) { @@ -1586,17 +1600,18 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) } } Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr; - Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType(); + Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort(); Trace("parser-qid") << std::endl; // otherwise, we process the type ascription p.d_expr = applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr(); } -Expr Smt2::parseOpToExpr(ParseOp& p) +api::Term Smt2::parseOpToExpr(ParseOp& p) { - Expr expr; - if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull()) + Debug("parser") << "parseOpToExpr: " << p << std::endl; + api::Term expr; + if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull()) { parseError( "Bad syntax for qualified identifier operator in term position."); @@ -1611,7 +1626,7 @@ Expr Smt2::parseOpToExpr(ParseOp& p) && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos) { // allow unary minus in sygus version 1 - expr = getExprManager()->mkConst(Rational(p.d_name)); + expr = d_solver->mkReal(p.d_name); } else { @@ -1628,38 +1643,41 @@ Expr Smt2::parseOpToExpr(ParseOp& p) return expr; } -Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) +api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) { bool isBuiltinOperator = false; // the builtin kind of the overall return expression - Kind kind = kind::NULL_EXPR; + api::Kind kind = api::NULL_EXPR; // First phase: process the operator if (Debug.isOn("parser")) { Debug("parser") << "applyParseOp: " << p << " to:" << std::endl; - for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); + ++i) { Debug("parser") << "++ " << *i << std::endl; } } api::Op op; - if (p.d_kind != kind::NULL_EXPR) + if (p.d_kind != api::NULL_EXPR) { // It is a special case, e.g. tupSel or array constant specification. // We have to wait until the arguments are parsed to resolve it. } else if (!p.d_expr.isNull()) { - // An explicit operator, e.g. an indexed symbol. - args.insert(args.begin(), p.d_expr); - Kind fkind = getKindForFunction(p.d_expr); - if (fkind != kind::UNDEFINED_KIND) + // An explicit operator, e.g. an apply function + api::Kind fkind = getKindForFunction(p.d_expr); + if (fkind != api::UNDEFINED_KIND) { // Some operators may require a specific kind. // Testers are handled differently than other indexed operators, // since they require a kind. kind = fkind; + Debug("parser") << "Got function kind " << kind << " for expression " + << std::endl; } + args.insert(args.begin(), p.d_expr); } else if (!p.d_op.isNull()) { @@ -1678,7 +1696,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) { // A non-built-in function application, get the expression checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE); - Expr v = getVariable(p.d_name); + api::Term v = getVariable(p.d_name); if (!v.isNull()) { checkFunctionLike(v); @@ -1691,12 +1709,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) // Could not find the expression. It may be an overloaded symbol, // in which case we may find it after knowing the types of its // arguments. - std::vector<Type> argTypes; - for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + std::vector<api::Sort> argTypes; + for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); + ++i) { - argTypes.push_back((*i).getType()); + argTypes.push_back((*i).getSort()); } - Expr fop = getOverloadedFunctionForTypes(p.d_name, argTypes); + api::Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes); if (!fop.isNull()) { checkFunctionLike(fop); @@ -1715,13 +1734,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) // Second phase: apply the arguments to the parse op ExprManager* em = getExprManager(); // handle special cases - if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull()) + if (p.d_kind == api::STORE_ALL && !p.d_type.isNull()) { if (args.size() != 1) { parseError("Too many arguments to array constant."); } - Expr constVal = args[0]; + api::Term constVal = args[0]; if (!constVal.isConst()) { // To parse array constants taking reals whose values are specified by @@ -1732,12 +1751,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) // like 5.0 which are converted to (/ 5 1) to distinguish them from // integer constants. We must ensure numerator and denominator are // constant and the denominator is non-zero. - if (constVal.getKind() == kind::DIVISION && constVal[0].isConst() + if (constVal.getKind() == api::DIVISION && constVal[0].isConst() && constVal[1].isConst() - && !constVal[1].getConst<Rational>().isZero()) + && !constVal[1].getExpr().getConst<Rational>().isZero()) { - constVal = em->mkConst(constVal[0].getConst<Rational>() - / constVal[1].getConst<Rational>()); + std::stringstream sdiv; + sdiv << constVal[0] << "/" << constVal[1]; + constVal = d_solver->mkReal(sdiv.str()); } if (!constVal.isConst()) { @@ -1748,47 +1768,52 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) parseError(ss.str()); } } - ArrayType aqtype = static_cast<ArrayType>(p.d_type); - if (!aqtype.getConstituentType().isComparableTo(constVal.getType())) + if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) { std::stringstream ss; ss << "type mismatch inside array constant term:" << std::endl << "array type: " << p.d_type << std::endl - << "expected const type: " << aqtype.getConstituentType() << std::endl - << "computed const type: " << constVal.getType(); + << "expected const type: " << p.d_type.getArrayElementSort() + << std::endl + << "computed const type: " << constVal.getSort(); parseError(ss.str()); } - return em->mkConst(ArrayStoreAll(p.d_type, constVal)); + api::Term ret = d_solver->mkConstArray(p.d_type, constVal); + Debug("parser") << "applyParseOp: return store all " << ret << std::endl; + return ret; } - else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull()) + else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull()) { // tuple selector case - Integer x = p.d_expr.getConst<Rational>().getNumerator(); + Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator(); if (!x.fitsUnsignedInt()) { parseError("index of tupSel is larger than size of unsigned int"); } unsigned int n = x.toUnsignedInt(); - if (args.size() > 1) + if (args.size() != 1) { - parseError("tupSel applied to more than one tuple argument"); + parseError("tupSel should only be applied to one tuple argument"); } - Type t = args[0].getType(); + api::Sort t = args[0].getSort(); if (!t.isTuple()) { parseError("tupSel applied to non-tuple"); } - size_t length = ((DatatypeType)t).getTupleLength(); + size_t length = t.getTupleLength(); if (n >= length) { std::stringstream ss; ss << "tuple is of length " << length << "; cannot access index " << n; parseError(ss.str()); } - const Datatype& dt = ((DatatypeType)t).getDatatype(); - return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args); + const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); + api::Term ret = d_solver->mkTerm( + api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]); + Debug("parser") << "applyParseOp: return selector " << ret << std::endl; + return ret; } - else if (p.d_kind != kind::NULL_EXPR) + else if (p.d_kind != api::NULL_EXPR) { // it should not have an expression or type specified at this point if (!p.d_expr.isNull() || !p.d_type.isNull()) @@ -1802,43 +1827,47 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) } else if (isBuiltinOperator) { + Trace("ajr-temp") << "mkTerm builtin operator" << std::endl; if (!em->getOptions().getUfHo() - && (kind == kind::EQUAL || kind == kind::DISTINCT)) + && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args - for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); + ++i) { - if ((*i).getType().isFunction()) + if ((*i).getSort().isFunction()) { parseError( "Cannot apply equalty to functions unless --uf-ho is set."); } } } - if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR) + if (!strictModeEnabled() && (kind == api::AND || kind == api::OR) && args.size() == 1) { // Unary AND/OR can be replaced with the argument. + Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl; return args[0]; } - else if (kind == kind::MINUS && args.size() == 1) + else if (kind == api::MINUS && args.size() == 1) { - return em->mkExpr(kind::UMINUS, args[0]); + api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]); + Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; + return ret; } - api::Term ret = - d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args)); + api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; - return ret.getExpr(); + return ret; } if (args.size() >= 2) { // may be partially applied function, in this case we use HO_APPLY - Type argt = args[0].getType(); + api::Sort argt = args[0].getSort(); if (argt.isFunction()) { - unsigned arity = static_cast<FunctionType>(argt).getArity(); + unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { if (!em->getOptions().getUfHo()) @@ -1848,26 +1877,33 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) Debug("parser") << "Partial application of " << args[0]; Debug("parser") << " : #argTypes = " << arity; Debug("parser") << ", #args = " << args.size() - 1 << std::endl; + api::Term ret = d_solver->mkTerm(api::HO_APPLY, args); + Debug("parser") << "applyParseOp: return curry higher order " << ret + << std::endl; // must curry the partial application - return em->mkLeftAssociative(kind::HO_APPLY, args); + return ret; } } } if (!op.isNull()) { - api::Term ret = d_solver->mkTerm(op, api::exprVectorToTerms(args)); + api::Term ret = d_solver->mkTerm(op, args); Debug("parser") << "applyParseOp: return op : " << ret << std::endl; - return ret.getExpr(); + return ret; } - if (kind == kind::NULL_EXPR) + if (kind == api::NULL_EXPR) { - std::vector<Expr> eargs(args.begin() + 1, args.end()); - return em->mkExpr(args[0], eargs); - } - return em->mkExpr(kind, args); + // should never happen in the new API + parseError("do not know how to process parse op"); + } + Debug("parser") << "Try default term construction for kind " << kind + << " #args = " << args.size() << "..." << std::endl; + api::Term ret = d_solver->mkTerm(kind, args); + Debug("parser") << "applyParseOp: return : " << ret << std::endl; + return ret; } -Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) +api::Term Smt2::setNamedAttribute(api::Term& expr, const SExpr& sexpr) { if (!sexpr.isKeyword()) { @@ -1876,7 +1912,7 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) std::string name = sexpr.getValue(); checkUserSymbol(name); // ensure expr is a closed subterm - if (expr.hasFreeVariable()) + if (expr.getExpr().hasFreeVariable()) { std::stringstream ss; ss << ":named annotations can only name terms that are closed"; @@ -1885,19 +1921,17 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) // check that sexpr is a fresh function symbol, and reserve it reserveSymbolAtAssertionLevel(name); // define it - Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED); + api::Term func = bindVar(name, expr.getSort(), ExprManager::VAR_FLAG_DEFINED); // remember the last term to have been given a :named attribute setLastNamedTerm(expr, name); return func; } -Expr Smt2::mkAnd(const std::vector<Expr>& es) +api::Term Smt2::mkAnd(const std::vector<api::Term>& es) { - ExprManager* em = getExprManager(); - if (es.size() == 0) { - return em->mkConst(true); + return d_solver->mkTrue(); } else if (es.size() == 1) { @@ -1905,7 +1939,7 @@ Expr Smt2::mkAnd(const std::vector<Expr>& es) } else { - return em->mkExpr(kind::AND, es); + return d_solver->mkTerm(api::AND, es); } } |