diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2035 |
1 files changed, 1281 insertions, 754 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fa995a00a..9b79b5c45 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2,10 +2,10 @@ /*! \file cvc4cpp.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** @@ -34,23 +34,29 @@ #include "api/cvc4cpp.h" #include <cstring> +#include <regex> #include <sstream> #include "base/check.h" #include "base/configuration.h" +#include "expr/dtype.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" #include "expr/kind.h" #include "expr/metakind.h" +#include "expr/node.h" #include "expr/node_manager.h" #include "expr/sequence.h" #include "expr/type.h" +#include "expr/type_node.h" #include "options/main_options.h" #include "options/options.h" #include "options/smt_options.h" +#include "proof/unsat_core.h" #include "smt/model.h" #include "smt/smt_engine.h" +#include "smt/smt_mode.h" #include "theory/logic_info.h" #include "theory/theory_model.h" #include "util/random.h" @@ -76,6 +82,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {DISTINCT, CVC4::Kind::DISTINCT}, {CONSTANT, CVC4::Kind::VARIABLE}, {VARIABLE, CVC4::Kind::BOUND_VARIABLE}, + {SEXPR, CVC4::Kind::SEXPR}, {LAMBDA, CVC4::Kind::LAMBDA}, {WITNESS, CVC4::Kind::WITNESS}, /* Boolean ------------------------------------------------------------- */ @@ -250,6 +257,23 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {IDEN, CVC4::Kind::IDEN}, {COMPREHENSION, CVC4::Kind::COMPREHENSION}, {CHOOSE, CVC4::Kind::CHOOSE}, + {IS_SINGLETON, CVC4::Kind::IS_SINGLETON}, + /* Bags ---------------------------------------------------------------- */ + {UNION_MAX, CVC4::Kind::UNION_MAX}, + {UNION_DISJOINT, CVC4::Kind::UNION_DISJOINT}, + {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN}, + {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT}, + {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE}, + {SUBBAG, CVC4::Kind::SUBBAG}, + {BAG_COUNT, CVC4::Kind::BAG_COUNT}, + {DUPLICATE_REMOVAL, CVC4::Kind::DUPLICATE_REMOVAL}, + {MK_BAG, CVC4::Kind::MK_BAG}, + {EMPTYBAG, CVC4::Kind::EMPTYBAG}, + {BAG_CARD, CVC4::Kind::BAG_CARD}, + {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE}, + {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON}, + {BAG_FROM_SET, CVC4::Kind::BAG_FROM_SET}, + {BAG_TO_SET, CVC4::Kind::BAG_TO_SET}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -305,6 +329,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX}, {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE}, {SEQ_UNIT, CVC4::Kind::SEQ_UNIT}, + {SEQ_NTH, CVC4::Kind::SEQ_NTH}, /* Quantifiers --------------------------------------------------------- */ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, @@ -538,6 +563,23 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::IDEN, IDEN}, {CVC4::Kind::COMPREHENSION, COMPREHENSION}, {CVC4::Kind::CHOOSE, CHOOSE}, + {CVC4::Kind::IS_SINGLETON, IS_SINGLETON}, + /* Bags ------------------------------------------------------------ */ + {CVC4::Kind::UNION_MAX, UNION_MAX}, + {CVC4::Kind::UNION_DISJOINT, UNION_DISJOINT}, + {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN}, + {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT}, + {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE}, + {CVC4::Kind::SUBBAG, SUBBAG}, + {CVC4::Kind::BAG_COUNT, BAG_COUNT}, + {CVC4::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL}, + {CVC4::Kind::MK_BAG, MK_BAG}, + {CVC4::Kind::EMPTYBAG, EMPTYBAG}, + {CVC4::Kind::BAG_CARD, BAG_CARD}, + {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE}, + {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, + {CVC4::Kind::BAG_FROM_SET, BAG_FROM_SET}, + {CVC4::Kind::BAG_TO_SET, BAG_TO_SET}, /* Strings --------------------------------------------------------- */ {CVC4::Kind::STRING_CONCAT, STRING_CONCAT}, {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, @@ -574,12 +616,15 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_OPT, REGEXP_OPT}, {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE}, {CVC4::Kind::REGEXP_REPEAT, REGEXP_REPEAT}, + {CVC4::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT}, {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP}, + {CVC4::Kind::REGEXP_LOOP_OP, REGEXP_LOOP}, {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, {CVC4::Kind::SEQ_UNIT, SEQ_UNIT}, + {CVC4::Kind::SEQ_NTH, SEQ_NTH}, /* Quantifiers ----------------------------------------------------- */ {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, @@ -642,7 +687,15 @@ uint32_t minArity(Kind k) { Assert(isDefinedKind(k)); Assert(isDefinedIntKind(extToIntKind(k))); - return CVC4::ExprManager::minArity(extToIntKind(k)); + uint32_t min = CVC4::ExprManager::minArity(extToIntKind(k)); + + // At the API level, we treat functions/constructors/selectors/testers as + // normal terms instead of making them part of the operator + if (isApplyKind(extToIntKind(k))) + { + min++; + } + return min; } uint32_t maxArity(Kind k) @@ -651,9 +704,8 @@ uint32_t maxArity(Kind k) Assert(isDefinedIntKind(extToIntKind(k))); uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k)); - // special cases for API level - // higher-order logic perspective at API - // functions/constructors/selectors/testers are terms + // At the API level, we treat functions/constructors/selectors/testers as + // normal terms instead of making them part of the operator if (isApplyKind(extToIntKind(k)) && max != std::numeric_limits<uint32_t>::max()) // be careful not to // overflow @@ -710,10 +762,35 @@ class CVC4ApiExceptionStream std::stringstream d_stream; }; +class CVC4ApiRecoverableExceptionStream +{ + public: + CVC4ApiRecoverableExceptionStream() {} + /* Note: This needs to be explicitly set to 'noexcept(false)' since it is + * a destructor that throws an exception and in C++11 all destructors + * default to noexcept(true) (else this triggers a call to std::terminate). */ + ~CVC4ApiRecoverableExceptionStream() noexcept(false) + { + if (!std::uncaught_exception()) + { + throw CVC4ApiRecoverableException(d_stream.str()); + } + } + + std::ostream& ostream() { return d_stream; } + + private: + std::stringstream d_stream; +}; + #define CVC4_API_CHECK(cond) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() +#define CVC4_API_RECOVERABLE_CHECK(cond) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream() + #define CVC4_API_CHECK_NOT_NULL \ CVC4_API_CHECK(!isNullHelper()) \ << "Invalid call to '" << __PRETTY_FUNCTION__ \ @@ -765,6 +842,10 @@ class CVC4ApiExceptionStream { #define CVC4_API_SOLVER_TRY_CATCH_END \ } \ + catch (const CVC4::RecoverableModalException& e) \ + { \ + throw CVC4ApiRecoverableException(e.getMessage()); \ + } \ catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \ catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } @@ -865,13 +946,26 @@ std::ostream& operator<<(std::ostream& out, const Result& r) /* -------------------------------------------------------------------------- */ Sort::Sort(const Solver* slv, const CVC4::Type& t) - : d_solver(slv), d_type(new CVC4::Type(t)) + : d_solver(slv), d_type(new CVC4::TypeNode(TypeNode::fromType(t))) +{ +} +Sort::Sort(const Solver* slv, const CVC4::TypeNode& t) + : d_solver(slv), d_type(new CVC4::TypeNode(t)) { } -Sort::Sort() : d_solver(nullptr), d_type(new CVC4::Type()) {} +Sort::Sort() : d_solver(nullptr), d_type(new CVC4::TypeNode()) {} -Sort::~Sort() {} +Sort::~Sort() +{ + if (d_solver != nullptr) + { + // Ensure that the correct node manager is in scope when the node is + // destroyed. + NodeManagerScope scope(d_solver->getNodeManager()); + d_type.reset(); + } +} /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -916,7 +1010,7 @@ bool Sort::isDatatype() const { return d_type->isDatatype(); } bool Sort::isParametricDatatype() const { if (!d_type->isDatatype()) return false; - return DatatypeType(*d_type).isParametric(); + return d_type->isParametricDatatype(); } bool Sort::isConstructor() const { return d_type->isConstructor(); } @@ -935,6 +1029,8 @@ bool Sort::isArray() const { return d_type->isArray(); } bool Sort::isSet() const { return d_type->isSet(); } +bool Sort::isBag() const { return d_type->isBag(); } + bool Sort::isSequence() const { return d_type->isSequence(); } bool Sort::isUninterpretedSort() const { return d_type->isSort(); } @@ -954,52 +1050,91 @@ bool Sort::isComparableTo(Sort s) const Datatype Sort::getDatatype() const { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK(isDatatype()) << "Expected datatype sort."; - return Datatype(d_solver, DatatypeType(*d_type).getDatatype()); + return Datatype(d_solver, d_type->getDType()); } Sort Sort::instantiate(const std::vector<Sort>& params) const { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK(isParametricDatatype() || isSortConstructor()) << "Expected parametric datatype or sort constructor sort."; - std::vector<Type> tparams; - for (const Sort& s : params) - { - tparams.push_back(*s.d_type.get()); - } + std::vector<CVC4::TypeNode> tparams = sortVectorToTypeNodes(params); if (d_type->isDatatype()) { - return Sort(d_solver, DatatypeType(*d_type).instantiate(tparams)); + return Sort(d_solver, d_type->instantiateParametricDatatype(tparams)); } Assert(d_type->isSortConstructor()); - return Sort(d_solver, SortConstructorType(*d_type).instantiate(tparams)); + return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams)); } -std::string Sort::toString() const { return d_type->toString(); } +std::string Sort::toString() const +{ + if (d_solver != nullptr) + { + NodeManagerScope scope(d_solver->getNodeManager()); + return d_type->toString(); + } + return d_type->toString(); +} // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Type Sort::getType(void) const { return *d_type; } +CVC4::Type Sort::getType(void) const +{ + if (d_type->isNull()) return Type(); + NodeManagerScope scope(d_solver->getNodeManager()); + return d_type->toType(); +} +const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; } /* Constructor sort ------------------------------------------------------- */ size_t Sort::getConstructorArity() const { - CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this); - return ConstructorType(*d_type).getArity(); + CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + return d_type->getNumChildren() - 1; } std::vector<Sort> Sort::getConstructorDomainSorts() const { - CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this); - std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes(); - return typeVectorToSorts(d_solver, types); + CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + return typeNodeVectorToSorts(d_solver, d_type->getArgTypes()); } Sort Sort::getConstructorCodomainSort() const { - CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this); - return Sort(d_solver, ConstructorType(*d_type).getRangeType()); + CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + return Sort(d_solver, d_type->getConstructorRangeType()); +} + +/* Selector sort ------------------------------------------------------- */ + +Sort Sort::getSelectorDomainSort() const +{ + CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this); + return Sort(d_solver, d_type->getSelectorDomainType()); +} + +Sort Sort::getSelectorCodomainSort() const +{ + CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this); + return Sort(d_solver, d_type->getSelectorRangeType()); +} + +/* Tester sort ------------------------------------------------------- */ + +Sort Sort::getTesterDomainSort() const +{ + CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this); + return Sort(d_solver, d_type->getTesterDomainType()); +} + +Sort Sort::getTesterCodomainSort() const +{ + CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this); + return d_solver->getBooleanSort(); } /* Function sort ------------------------------------------------------- */ @@ -1007,20 +1142,19 @@ Sort Sort::getConstructorCodomainSort() const size_t Sort::getFunctionArity() const { CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this); - return FunctionType(*d_type).getArity(); + return d_type->getNumChildren() - 1; } std::vector<Sort> Sort::getFunctionDomainSorts() const { CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this); - std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes(); - return typeVectorToSorts(d_solver, types); + return typeNodeVectorToSorts(d_solver, d_type->getArgTypes()); } Sort Sort::getFunctionCodomainSort() const { CVC4_API_CHECK(isFunction()) << "Not a function sort" << (*this); - return Sort(d_solver, FunctionType(*d_type).getRangeType()); + return Sort(d_solver, d_type->getRangeType()); } /* Array sort ---------------------------------------------------------- */ @@ -1028,13 +1162,13 @@ Sort Sort::getFunctionCodomainSort() const Sort Sort::getArrayIndexSort() const { CVC4_API_CHECK(isArray()) << "Not an array sort."; - return Sort(d_solver, ArrayType(*d_type).getIndexType()); + return Sort(d_solver, d_type->getArrayIndexType()); } Sort Sort::getArrayElementSort() const { CVC4_API_CHECK(isArray()) << "Not an array sort."; - return Sort(d_solver, ArrayType(*d_type).getConstituentType()); + return Sort(d_solver, d_type->getArrayConstituentType()); } /* Set sort ------------------------------------------------------------ */ @@ -1042,15 +1176,23 @@ Sort Sort::getArrayElementSort() const Sort Sort::getSetElementSort() const { CVC4_API_CHECK(isSet()) << "Not a set sort."; - return Sort(d_solver, SetType(*d_type).getElementType()); + return Sort(d_solver, d_type->getSetElementType()); } -/* Set sort ------------------------------------------------------------ */ +/* Bag sort ------------------------------------------------------------ */ + +Sort Sort::getBagElementSort() const +{ + CVC4_API_CHECK(isBag()) << "Not a bag sort."; + return Sort(d_solver, d_type->getBagElementType()); +} + +/* Sequence sort ------------------------------------------------------- */ Sort Sort::getSequenceElementSort() const { CVC4_API_CHECK(isSequence()) << "Not a sequence sort."; - return Sort(d_solver, SequenceType(*d_type).getElementType()); + return Sort(d_solver, d_type->getSequenceElementType()); } /* Uninterpreted sort -------------------------------------------------- */ @@ -1058,20 +1200,28 @@ Sort Sort::getSequenceElementSort() const std::string Sort::getUninterpretedSortName() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - return SortType(*d_type).getName(); + return d_type->getName(); } bool Sort::isUninterpretedSortParameterized() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - return SortType(*d_type).isParameterized(); + // This method is not implemented in the NodeManager, since whether a + // uninterpreted sort is parametrized is irrelevant for solving. + return d_type->getNumChildren() > 0; } std::vector<Sort> Sort::getUninterpretedSortParamSorts() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - std::vector<CVC4::Type> types = SortType(*d_type).getParamTypes(); - return typeVectorToSorts(d_solver, types); + // This method is not implemented in the NodeManager, since whether a + // uninterpreted sort is parametrized is irrelevant for solving. + std::vector<TypeNode> params; + for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++) + { + params.push_back((*d_type)[i]); + } + return typeNodeVectorToSorts(d_solver, params); } /* Sort constructor sort ----------------------------------------------- */ @@ -1079,13 +1229,13 @@ std::vector<Sort> Sort::getUninterpretedSortParamSorts() const std::string Sort::getSortConstructorName() const { CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; - return SortConstructorType(*d_type).getName(); + return d_type->getName(); } size_t Sort::getSortConstructorArity() const { CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; - return SortConstructorType(*d_type).getArity(); + return d_type->getSortConstructorArity(); } /* Bit-vector sort ----------------------------------------------------- */ @@ -1093,7 +1243,7 @@ size_t Sort::getSortConstructorArity() const uint32_t Sort::getBVSize() const { CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort."; - return BitVectorType(*d_type).getSize(); + return d_type->getBitVectorSize(); } /* Floating-point sort ------------------------------------------------- */ @@ -1101,13 +1251,13 @@ uint32_t Sort::getBVSize() const uint32_t Sort::getFPExponentSize() const { CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; - return FloatingPointType(*d_type).getExponentSize(); + return d_type->getFloatingPointExponentSize(); } uint32_t Sort::getFPSignificandSize() const { CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; - return FloatingPointType(*d_type).getSignificandSize(); + return d_type->getFloatingPointSignificandSize(); } /* Datatype sort ------------------------------------------------------- */ @@ -1115,14 +1265,14 @@ uint32_t Sort::getFPSignificandSize() const std::vector<Sort> Sort::getDatatypeParamSorts() const { CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; - std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes(); - return typeVectorToSorts(d_solver, types); + std::vector<CVC4::TypeNode> typeNodes = d_type->getParamTypes(); + return typeNodeVectorToSorts(d_solver, typeNodes); } size_t Sort::getDatatypeArity() const { CVC4_API_CHECK(isDatatype()) << "Not a datatype sort."; - return DatatypeType(*d_type).getArity(); + return d_type->getNumChildren() - 1; } /* Tuple sort ---------------------------------------------------------- */ @@ -1130,14 +1280,14 @@ size_t Sort::getDatatypeArity() const size_t Sort::getTupleLength() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - return DatatypeType(*d_type).getTupleLength(); + return d_type->getTupleLength(); } std::vector<Sort> Sort::getTupleSorts() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes(); - return typeVectorToSorts(d_solver, types); + std::vector<CVC4::TypeNode> typeNodes = d_type->getTupleTypes(); + return typeNodeVectorToSorts(d_solver, typeNodes); } /* --------------------------------------------------------------------- */ @@ -1150,26 +1300,40 @@ std::ostream& operator<<(std::ostream& out, const Sort& s) size_t SortHashFunction::operator()(const Sort& s) const { - return TypeHashFunction()(*s.d_type); + return TypeNodeHashFunction()(*s.d_type); } /* -------------------------------------------------------------------------- */ /* Op */ /* -------------------------------------------------------------------------- */ -Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {} +Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC4::Node()) {} Op::Op(const Solver* slv, const Kind k) - : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr()) + : d_solver(slv), d_kind(k), d_node(new CVC4::Node()) { } Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e) - : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr(e)) + : d_solver(slv), d_kind(k), d_node(new CVC4::Node(Node::fromExpr(e))) { } -Op::~Op() {} +Op::Op(const Solver* slv, const Kind k, const CVC4::Node& n) + : d_solver(slv), d_kind(k), d_node(new CVC4::Node(n)) +{ +} + +Op::~Op() +{ + if (d_solver != nullptr) + { + // Ensure that the correct node manager is in scope when the type node is + // destroyed. + NodeManagerScope scope(d_solver->getNodeManager()); + d_node.reset(); + } +} /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -1179,23 +1343,23 @@ Op::~Op() {} bool Op::isNullHelper() const { - return (d_expr->isNull() && (d_kind == NULL_EXPR)); + return (d_node->isNull() && (d_kind == NULL_EXPR)); } -bool Op::isIndexedHelper() const { return !d_expr->isNull(); } +bool Op::isIndexedHelper() const { return !d_node->isNull(); } /* Public methods */ bool Op::operator==(const Op& t) const { - if (d_expr->isNull() && t.d_expr->isNull()) + if (d_node->isNull() && t.d_node->isNull()) { return (d_kind == t.d_kind); } - else if (d_expr->isNull() || t.d_expr->isNull()) + else if (d_node->isNull() || t.d_node->isNull()) { return false; } - return (d_kind == t.d_kind) && (*d_expr == *t.d_expr); + return (d_kind == t.d_kind) && (*d_node == *t.d_node); } bool Op::operator!=(const Op& t) const { return !(*this == t); } @@ -1214,22 +1378,22 @@ template <> std::string Op::getIndices() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; std::string i; - Kind k = intToExtKind(d_expr->getKind()); + Kind k = intToExtKind(d_node->getKind()); if (k == DIVISIBLE) { // DIVISIBLE returns a string index to support // arbitrary precision integers - CVC4::Integer _int = d_expr->getConst<Divisible>().k; + CVC4::Integer _int = d_node->getConst<Divisible>().k; i = _int.toString(); } else if (k == RECORD_UPDATE) { - i = d_expr->getConst<RecordUpdate>().getField(); + i = d_node->getConst<RecordUpdate>().getField(); } else { @@ -1244,37 +1408,40 @@ template <> uint32_t Op::getIndices() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; uint32_t i = 0; - Kind k = intToExtKind(d_expr->getKind()); + Kind k = intToExtKind(d_node->getKind()); switch (k) { case BITVECTOR_REPEAT: - i = d_expr->getConst<BitVectorRepeat>().d_repeatAmount; + i = d_node->getConst<BitVectorRepeat>().d_repeatAmount; break; case BITVECTOR_ZERO_EXTEND: - i = d_expr->getConst<BitVectorZeroExtend>().d_zeroExtendAmount; + i = d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount; break; case BITVECTOR_SIGN_EXTEND: - i = d_expr->getConst<BitVectorSignExtend>().d_signExtendAmount; + i = d_node->getConst<BitVectorSignExtend>().d_signExtendAmount; break; case BITVECTOR_ROTATE_LEFT: - i = d_expr->getConst<BitVectorRotateLeft>().d_rotateLeftAmount; + i = d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount; break; case BITVECTOR_ROTATE_RIGHT: - i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount; + i = d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount; break; - case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break; - case IAND: i = d_expr->getConst<IntAnd>().d_size; break; + case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break; + case IAND: i = d_node->getConst<IntAnd>().d_size; break; case FLOATINGPOINT_TO_UBV: - i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size; + i = d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size; break; case FLOATINGPOINT_TO_SBV: - i = d_expr->getConst<FloatingPointToSBV>().bvs.d_size; + i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size; + break; + case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break; + case REGEXP_REPEAT: + i = d_node->getConst<RegExpRepeat>().d_repeatAmount; break; - case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break; default: CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" << " kind " << kindToString(k); @@ -1286,52 +1453,63 @@ template <> std::pair<uint32_t, uint32_t> Op::getIndices() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; std::pair<uint32_t, uint32_t> indices; - Kind k = intToExtKind(d_expr->getKind()); + Kind k = intToExtKind(d_node->getKind()); // using if/else instead of case statement because want local variables if (k == BITVECTOR_EXTRACT) { - CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>(); + CVC4::BitVectorExtract ext = d_node->getConst<BitVectorExtract>(); indices = std::make_pair(ext.d_high, ext.d_low); } else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) { CVC4::FloatingPointToFPIEEEBitVector ext = - d_expr->getConst<FloatingPointToFPIEEEBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + d_node->getConst<FloatingPointToFPIEEEBitVector>(); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { CVC4::FloatingPointToFPFloatingPoint ext = - d_expr->getConst<FloatingPointToFPFloatingPoint>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + d_node->getConst<FloatingPointToFPFloatingPoint>(); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { - CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>(); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { CVC4::FloatingPointToFPSignedBitVector ext = - d_expr->getConst<FloatingPointToFPSignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + d_node->getConst<FloatingPointToFPSignedBitVector>(); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { CVC4::FloatingPointToFPUnsignedBitVector ext = - d_expr->getConst<FloatingPointToFPUnsignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + d_node->getConst<FloatingPointToFPUnsignedBitVector>(); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { CVC4::FloatingPointToFPGeneric ext = - d_expr->getConst<FloatingPointToFPGeneric>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + d_node->getConst<FloatingPointToFPGeneric>(); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); + } + else if (k == REGEXP_LOOP) + { + CVC4::RegExpLoop ext = d_node->getConst<RegExpLoop>(); + indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc); } else { @@ -1344,21 +1522,31 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const std::string Op::toString() const { CVC4_API_CHECK_NOT_NULL; - if (d_expr->isNull()) + if (d_node->isNull()) { return kindToString(d_kind); } else { - CVC4_API_CHECK(!d_expr->isNull()) + CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression"; - return d_expr->toString(); + if (d_solver != nullptr) + { + NodeManagerScope scope(d_solver->getNodeManager()); + return d_node->toString(); + } + return d_node->toString(); } } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Expr Op::getExpr(void) const { return *d_expr; } +CVC4::Expr Op::getExpr(void) const +{ + if (d_node->isNull()) return Expr(); + NodeManagerScope scope(d_solver->getNodeManager()); + return d_node->toExpr(); +} std::ostream& operator<<(std::ostream& out, const Op& t) { @@ -1370,7 +1558,7 @@ size_t OpHashFunction::operator()(const Op& t) const { if (t.isIndexedHelper()) { - return ExprHashFunction()(*t.d_expr); + return ExprHashFunction()(t.d_node->toExpr()); } else { @@ -1382,19 +1570,37 @@ size_t OpHashFunction::operator()(const Op& t) const /* Term */ /* -------------------------------------------------------------------------- */ -Term::Term() : d_solver(nullptr), d_expr(new CVC4::Expr()) {} +Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {} -Term::Term(const Solver* slv, const CVC4::Expr& e) - : d_solver(slv), d_expr(new CVC4::Expr(e)) +Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv) { + // Ensure that we create the node in the correct node manager. + NodeManagerScope scope(d_solver->getNodeManager()); + d_node.reset(new CVC4::Node(e)); } -Term::~Term() {} +Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv) +{ + // Ensure that we create the node in the correct node manager. + NodeManagerScope scope(d_solver->getNodeManager()); + d_node.reset(new CVC4::Node(n)); +} + +Term::~Term() +{ + if (d_solver != nullptr) + { + // Ensure that the correct node manager is in scope when the node is + // destroyed. + NodeManagerScope scope(d_solver->getNodeManager()); + d_node.reset(); + } +} bool Term::isNullHelper() const { /* Split out to avoid nested API calls (problematic with API tracing). */ - return d_expr->isNull(); + return d_node->isNull(); } Kind Term::getKindHelper() const @@ -1403,9 +1609,9 @@ Kind Term::getKindHelper() const // (string) versions back to sequence. All operators where this is // necessary are such that their first child is of sequence type, which // we check here. - if (getNumChildren() > 0 && (*this)[0].getSort().isSequence()) + if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence()) { - switch (d_expr->getKind()) + switch (d_node->getKind()) { case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; @@ -1424,56 +1630,78 @@ Kind Term::getKindHelper() const break; } } + // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to + // INTERNAL_KIND. + if(isCastedReal()) + { + return CONST_RATIONAL; + } + return intToExtKind(d_node->getKind()); +} - return intToExtKind(d_expr->getKind()); +bool Term::isCastedReal() const +{ + if(d_node->getKind() == kind::CAST_TO_REAL) + { + return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger(); + } + return false; } -bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } +bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; } -bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } +bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; } -bool Term::operator<(const Term& t) const { return *d_expr < *t.d_expr; } +bool Term::operator<(const Term& t) const { return *d_node < *t.d_node; } -bool Term::operator>(const Term& t) const { return *d_expr > *t.d_expr; } +bool Term::operator>(const Term& t) const { return *d_node > *t.d_node; } -bool Term::operator<=(const Term& t) const { return *d_expr <= *t.d_expr; } +bool Term::operator<=(const Term& t) const { return *d_node <= *t.d_node; } -bool Term::operator>=(const Term& t) const { return *d_expr >= *t.d_expr; } +bool Term::operator>=(const Term& t) const { return *d_node >= *t.d_node; } size_t Term::getNumChildren() const { CVC4_API_CHECK_NOT_NULL; // special case for apply kinds - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) + { + return d_node->getNumChildren() + 1; + } + if(isCastedReal()) { - return d_expr->getNumChildren() + 1; + return 0; } - return d_expr->getNumChildren(); + return d_node->getNumChildren(); } Term Term::operator[](size_t index) const { CVC4_API_CHECK_NOT_NULL; + + // check the index within the number of children + CVC4_API_CHECK(index < getNumChildren()) << "index out of bound"; + // special cases for apply kinds - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { - CVC4_API_CHECK(d_expr->hasOperator()) + CVC4_API_CHECK(d_node->hasOperator()) << "Expected apply kind to have operator when accessing child of Term"; if (index == 0) { // return the operator - return Term(d_solver, d_expr->getOperator()); + return Term(d_solver, d_node->getOperator().toExpr()); } // otherwise we are looking up child at (index-1) index--; } - return Term(d_solver, (*d_expr)[index]); + return Term(d_solver, (*d_node)[index].toExpr()); } uint64_t Term::getId() const { CVC4_API_CHECK_NOT_NULL; - return d_expr->getId(); + return d_node->getId(); } Kind Term::getKind() const @@ -1485,7 +1713,8 @@ Kind Term::getKind() const Sort Term::getSort() const { CVC4_API_CHECK_NOT_NULL; - return Sort(d_solver, d_expr->getType()); + NodeManagerScope scope(d_solver->getNodeManager()); + return Sort(d_solver, d_node->getType()); } Term Term::substitute(Term e, Term replacement) const @@ -1497,7 +1726,8 @@ Term Term::substitute(Term e, Term replacement) const << "Expected non-null term as replacement in substitute"; CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort())) << "Expecting terms of comparable sort in substitute"; - return Term(d_solver, d_expr->substitute(e.getExpr(), replacement.getExpr())); + return Term(d_solver, + d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))); } Term Term::substitute(const std::vector<Term> es, @@ -1515,21 +1745,26 @@ Term Term::substitute(const std::vector<Term> es, CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort())) << "Expecting terms of comparable sort in substitute"; } + + std::vector<Node> nodes = termVectorToNodes(es); + std::vector<Node> nodeReplacements = termVectorToNodes(replacements); return Term(d_solver, - d_expr->substitute(termVectorToExprs(es), - termVectorToExprs(replacements))); + d_node->substitute(nodes.begin(), + nodes.end(), + nodeReplacements.begin(), + nodeReplacements.end())); } bool Term::hasOp() const { CVC4_API_CHECK_NOT_NULL; - return d_expr->hasOperator(); + return d_node->hasOperator(); } Op Term::getOp() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(d_expr->hasOperator()) + CVC4_API_CHECK(d_node->hasOperator()) << "Expecting Term to have an Op when calling getOp()"; // special cases for parameterized operators that are not indexed operators @@ -1537,51 +1772,45 @@ Op Term::getOp() const // indexed operators are stored in Ops // whereas functions and datatype operators are terms, and the Op // is one of the APPLY_* kinds - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { - return Op(d_solver, intToExtKind(d_expr->getKind())); + return Op(d_solver, intToExtKind(d_node->getKind())); } - else if (d_expr->isParameterized()) + else if (d_node->getMetaKind() == kind::metakind::PARAMETERIZED) { // it's an indexed operator // so we should return the indexed op - CVC4::Expr op = d_expr->getOperator(); - return Op(d_solver, intToExtKind(d_expr->getKind()), op); + CVC4::Node op = d_node->getOperator(); + return Op(d_solver, intToExtKind(d_node->getKind()), op); } // Notice this is the only case where getKindHelper is used, since the - // cases above do have special cases for intToExtKind. + // cases above do not have special cases for intToExtKind. return Op(d_solver, getKindHelper()); } bool Term::isNull() const { return isNullHelper(); } -bool Term::isConst() const -{ - CVC4_API_CHECK_NOT_NULL; - return d_expr->isConst(); -} - Term Term::getConstArrayBase() const { CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager())); CVC4_API_CHECK_NOT_NULL; // CONST_ARRAY kind maps to STORE_ALL internal kind - CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL) + CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL) << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; - return Term(d_solver, d_expr->getConst<ArrayStoreAll>().getValue().toExpr()); + return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue()); } std::vector<Term> Term::getConstSequenceElements() const { CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::CONST_SEQUENCE) + CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE) << "Expecting a CONST_SEQUENCE Term when calling " "getConstSequenceElements()"; - const std::vector<Node>& elems = d_expr->getConst<Sequence>().getVec(); + const std::vector<Node>& elems = d_node->getConst<Sequence>().getVec(); std::vector<Term> terms; for (const Node& t : elems) { - terms.push_back(Term(d_solver, t.toExpr())); + terms.push_back(Term(d_solver, t)); } return terms; } @@ -1591,11 +1820,11 @@ Term Term::notTerm() const CVC4_API_CHECK_NOT_NULL; try { - Expr res = d_expr->notExpr(); + Node res = d_node->notNode(); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1607,11 +1836,11 @@ Term Term::andTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->andExpr(*t.d_expr); + Node res = d_node->andNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1623,11 +1852,11 @@ Term Term::orTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->orExpr(*t.d_expr); + Node res = d_node->orNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1639,11 +1868,11 @@ Term Term::xorTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->xorExpr(*t.d_expr); + Node res = d_node->xorNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1655,11 +1884,11 @@ Term Term::eqTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->eqExpr(*t.d_expr); + Node res = d_node->eqNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1671,11 +1900,11 @@ Term Term::impTerm(const Term& t) const CVC4_API_ARG_CHECK_NOT_NULL(t); try { - Expr res = d_expr->impExpr(*t.d_expr); + Node res = d_node->impNode(*t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } @@ -1688,37 +1917,45 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const CVC4_API_ARG_CHECK_NOT_NULL(else_t); try { - Expr res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr); + Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node); (void)res.getType(true); /* kick off type checking */ return Term(d_solver, res); } - catch (const CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingExceptionPrivate& e) { throw CVC4ApiException(e.getMessage()); } } -std::string Term::toString() const { return d_expr->toString(); } +std::string Term::toString() const +{ + if (d_solver != nullptr) + { + NodeManagerScope scope(d_solver->getNodeManager()); + return d_node->toString(); + } + return d_node->toString(); +} Term::const_iterator::const_iterator() - : d_solver(nullptr), d_orig_expr(nullptr), d_pos(0) + : d_solver(nullptr), d_origNode(nullptr), d_pos(0) { } Term::const_iterator::const_iterator(const Solver* slv, - const std::shared_ptr<CVC4::Expr>& e, + const std::shared_ptr<CVC4::Node>& n, uint32_t p) - : d_solver(slv), d_orig_expr(e), d_pos(p) + : d_solver(slv), d_origNode(n), d_pos(p) { } Term::const_iterator::const_iterator(const const_iterator& it) - : d_solver(nullptr), d_orig_expr(nullptr) + : d_solver(nullptr), d_origNode(nullptr) { - if (it.d_orig_expr != nullptr) + if (it.d_origNode != nullptr) { d_solver = it.d_solver; - d_orig_expr = it.d_orig_expr; + d_origNode = it.d_origNode; d_pos = it.d_pos; } } @@ -1726,18 +1963,18 @@ Term::const_iterator::const_iterator(const const_iterator& it) Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it) { d_solver = it.d_solver; - d_orig_expr = it.d_orig_expr; + d_origNode = it.d_origNode; d_pos = it.d_pos; return *this; } bool Term::const_iterator::operator==(const const_iterator& it) const { - if (d_orig_expr == nullptr || it.d_orig_expr == nullptr) + if (d_origNode == nullptr || it.d_origNode == nullptr) { return false; } - return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr) + return (d_solver == it.d_solver && *d_origNode == *it.d_origNode) && (d_pos == it.d_pos); } @@ -1748,14 +1985,14 @@ bool Term::const_iterator::operator!=(const const_iterator& it) const Term::const_iterator& Term::const_iterator::operator++() { - Assert(d_orig_expr != nullptr); + Assert(d_origNode != nullptr); ++d_pos; return *this; } Term::const_iterator Term::const_iterator::operator++(int) { - Assert(d_orig_expr != nullptr); + Assert(d_origNode != nullptr); const_iterator it = *this; ++d_pos; return it; @@ -1763,14 +2000,14 @@ Term::const_iterator Term::const_iterator::operator++(int) Term Term::const_iterator::operator*() const { - Assert(d_orig_expr != nullptr); + Assert(d_origNode != nullptr); // this term has an extra child (mismatch between API and internal structure) // the extra child will be the first child - bool extra_child = isApplyKind(d_orig_expr->getKind()); + bool extra_child = isApplyKind(d_origNode->getKind()); if (!d_pos && extra_child) { - return Term(d_solver, d_orig_expr->getOperator()); + return Term(d_solver, d_origNode->getOperator()); } else { @@ -1781,35 +2018,47 @@ Term Term::const_iterator::operator*() const --idx; } Assert(idx >= 0); - return Term(d_solver, (*d_orig_expr)[idx]); + return Term(d_solver, (*d_origNode)[idx]); } } Term::const_iterator Term::begin() const { - return Term::const_iterator(d_solver, d_expr, 0); + return Term::const_iterator(d_solver, d_node, 0); } Term::const_iterator Term::end() const { - int endpos = d_expr->getNumChildren(); + int endpos = d_node->getNumChildren(); // special cases for APPLY_* // the API differs from the internal structure // the API takes a "higher-order" perspective and the applied // function or datatype constructor/selector/tester is a Term // which means it needs to be one of the children, even though // internally it is not - if (isApplyKind(d_expr->getKind())) + if (isApplyKind(d_node->getKind())) { // one more child if this is a UF application (count the UF as a child) ++endpos; } - return Term::const_iterator(d_solver, d_expr, endpos); + return Term::const_iterator(d_solver, d_node, endpos); +} + +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Expr Term::getExpr(void) const +{ + if (d_node->isNull()) + { + return Expr(); + } + NodeManagerScope scope(d_solver->getNodeManager()); + return d_node->toExpr(); } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Expr Term::getExpr(void) const { return *d_expr; } +const CVC4::Node& Term::getNode(void) const { return *d_node; } std::ostream& operator<<(std::ostream& out, const Term& t) { @@ -1855,7 +2104,7 @@ std::ostream& operator<<( size_t TermHashFunction::operator()(const Term& t) const { - return ExprHashFunction()(*t.d_expr); + return NodeHashFunction()(*t.d_node); } /* -------------------------------------------------------------------------- */ @@ -1871,12 +2120,22 @@ DatatypeConstructorDecl::DatatypeConstructorDecl() DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv, const std::string& name) - : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name)) + : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(name)) { } +DatatypeConstructorDecl::~DatatypeConstructorDecl() +{ + if (d_ctor != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_ctor.reset(); + } +} void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort) { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null range sort for selector"; d_ctor->addArg(name, *sort.d_type); @@ -1884,7 +2143,8 @@ void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort) void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) { - d_ctor->addArg(name, DatatypeSelfType()); + NodeManagerScope scope(d_solver->getNodeManager()); + d_ctor->addArgSelf(name); } std::string DatatypeConstructorDecl::toString() const @@ -1896,8 +2156,8 @@ std::string DatatypeConstructorDecl::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::DatatypeConstructor& -DatatypeConstructorDecl::getDatatypeConstructor(void) const +const CVC4::DTypeConstructor& DatatypeConstructorDecl::getDatatypeConstructor( + void) const { return *d_ctor; } @@ -1923,8 +2183,7 @@ DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {} DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, bool isCoDatatype) - : d_solver(slv), - d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype)) + : d_solver(slv), d_dtype(new CVC4::DType(name, isCoDatatype)) { } @@ -1933,10 +2192,8 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, Sort param, bool isCoDatatype) : d_solver(slv), - d_dtype(new CVC4::Datatype(slv->getExprManager(), - name, - std::vector<Type>{*param.d_type}, - isCoDatatype)) + d_dtype(new CVC4::DType( + name, std::vector<TypeNode>{*param.d_type}, isCoDatatype)) { } @@ -1946,23 +2203,28 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, bool isCoDatatype) : d_solver(slv) { - std::vector<Type> tparams; - for (const Sort& p : params) - { - tparams.push_back(*p.d_type); - } - d_dtype = std::shared_ptr<CVC4::Datatype>( - new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype)); + std::vector<TypeNode> tparams = sortVectorToTypeNodes(params); + d_dtype = std::shared_ptr<CVC4::DType>( + new CVC4::DType(name, tparams, isCoDatatype)); } bool DatatypeDecl::isNullHelper() const { return !d_dtype; } -DatatypeDecl::~DatatypeDecl() {} +DatatypeDecl::~DatatypeDecl() +{ + if (d_dtype != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_dtype.reset(); + } +} void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) { + NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK_NOT_NULL; - d_dtype->addConstructor(*ctor.d_ctor); + d_dtype->addConstructor(ctor.d_ctor); } size_t DatatypeDecl::getNumConstructors() const @@ -1995,7 +2257,7 @@ bool DatatypeDecl::isNull() const { return isNullHelper(); } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } +CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; } std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) { @@ -2008,13 +2270,21 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {} DatatypeSelector::DatatypeSelector(const Solver* slv, - const CVC4::DatatypeConstructorArg& stor) - : d_solver(slv), d_stor(new CVC4::DatatypeConstructorArg(stor)) + const CVC4::DTypeSelector& stor) + : d_solver(slv), d_stor(new CVC4::DTypeSelector(stor)) { CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector"; } -DatatypeSelector::~DatatypeSelector() {} +DatatypeSelector::~DatatypeSelector() +{ + if (d_stor != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_stor.reset(); + } +} std::string DatatypeSelector::getName() const { return d_stor->getName(); } @@ -2038,8 +2308,7 @@ std::string DatatypeSelector::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg( - void) const +CVC4::DTypeSelector DatatypeSelector::getDatatypeConstructorArg(void) const { return *d_stor; } @@ -2057,14 +2326,22 @@ DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr) } DatatypeConstructor::DatatypeConstructor(const Solver* slv, - const CVC4::DatatypeConstructor& ctor) - : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(ctor)) + const CVC4::DTypeConstructor& ctor) + : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(ctor)) { CVC4_API_CHECK(d_ctor->isResolved()) << "Expected resolved datatype constructor"; } -DatatypeConstructor::~DatatypeConstructor() {} +DatatypeConstructor::~DatatypeConstructor() +{ + if (d_ctor != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_ctor.reset(); + } +} std::string DatatypeConstructor::getName() const { return d_ctor->getName(); } @@ -2074,6 +2351,30 @@ Term DatatypeConstructor::getConstructorTerm() const return ctor; } +Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const +{ + NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_CHECK(d_ctor->isResolved()) + << "Expected resolved datatype constructor"; + CVC4_API_CHECK(retSort.isDatatype()) + << "Cannot get specialized constructor type for non-datatype type " + << retSort; + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + + NodeManager* nm = d_solver->getNodeManager(); + Node ret = + nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType( + d_ctor->getSpecializedConstructorType(*retSort.d_type))), + d_ctor->getConstructor()); + (void)ret.getType(true); /* kick off type checking */ + // apply type ascription to the operator + Term sctor = api::Term(d_solver, ret); + return sctor; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term DatatypeConstructor::getTesterTerm() const { Term tst = Term(d_solver, d_ctor->getTester()); @@ -2117,20 +2418,19 @@ DatatypeConstructor::const_iterator DatatypeConstructor::end() const } DatatypeConstructor::const_iterator::const_iterator( - const Solver* slv, const CVC4::DatatypeConstructor& ctor, bool begin) + const Solver* slv, const CVC4::DTypeConstructor& ctor, bool begin) { d_solver = slv; - d_int_stors = ctor.getArgs(); + d_int_stors = &ctor.getArgs(); - const std::vector<CVC4::DatatypeConstructorArg>* sels = - static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>( - d_int_stors); - for (const auto& s : *sels) + const std::vector<std::shared_ptr<CVC4::DTypeSelector>>& sels = + ctor.getArgs(); + for (const std::shared_ptr<CVC4::DTypeSelector>& s : sels) { /* Can not use emplace_back here since constructor is private. */ - d_stors.push_back(DatatypeSelector(d_solver, s)); + d_stors.push_back(DatatypeSelector(d_solver, *s.get())); } - d_idx = begin ? 0 : sels->size(); + d_idx = begin ? 0 : sels.size(); } DatatypeConstructor::const_iterator::const_iterator() @@ -2195,7 +2495,7 @@ std::string DatatypeConstructor::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor( +const CVC4::DTypeConstructor& DatatypeConstructor::getDatatypeConstructor( void) const { return *d_ctor; @@ -2215,8 +2515,18 @@ DatatypeSelector DatatypeConstructor::getSelectorForName( break; } } - CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor " - << getName() << " exists"; + if (!foundSel) + { + std::stringstream snames; + snames << "{ "; + for (size_t i = 0, ncons = getNumSelectors(); i < ncons; i++) + { + snames << (*d_ctor)[i].getName() << " "; + } + snames << "} "; + CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor " + << getName() << " exists among " << snames.str(); + } return DatatypeSelector(d_solver, (*d_ctor)[index]); } @@ -2228,15 +2538,23 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) /* Datatype ----------------------------------------------------------------- */ -Datatype::Datatype(const Solver* slv, const CVC4::Datatype& dtype) - : d_solver(slv), d_dtype(new CVC4::Datatype(dtype)) +Datatype::Datatype(const Solver* slv, const CVC4::DType& dtype) + : d_solver(slv), d_dtype(new CVC4::DType(dtype)) { CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype"; } Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {} -Datatype::~Datatype() {} +Datatype::~Datatype() +{ + if (d_dtype != nullptr) + { + // ensure proper node manager is in scope + NodeManagerScope scope(d_solver->getNodeManager()); + d_dtype.reset(); + } +} DatatypeConstructor Datatype::operator[](size_t idx) const { @@ -2295,7 +2613,7 @@ Datatype::const_iterator Datatype::end() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; } +const CVC4::DType& Datatype::getDatatype(void) const { return *d_dtype; } DatatypeConstructor Datatype::getConstructorForName( const std::string& name) const @@ -2311,24 +2629,34 @@ DatatypeConstructor Datatype::getConstructorForName( break; } } - CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype " - << getName() << " exists"; + if (!foundCons) + { + std::stringstream snames; + snames << "{ "; + for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + snames << (*d_dtype)[i].getName() << " "; + } + snames << "}"; + CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype " + << getName() << " exists, among " << snames.str(); + } return DatatypeConstructor(d_solver, (*d_dtype)[index]); } Datatype::const_iterator::const_iterator(const Solver* slv, - const CVC4::Datatype& dtype, + const CVC4::DType& dtype, bool begin) - : d_solver(slv), d_int_ctors(dtype.getConstructors()) + : d_solver(slv), d_int_ctors(&dtype.getConstructors()) { - const std::vector<CVC4::DatatypeConstructor>* cons = - static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors); - for (const auto& c : *cons) + const std::vector<std::shared_ptr<DTypeConstructor>>& cons = + dtype.getConstructors(); + for (const std::shared_ptr<DTypeConstructor>& c : cons) { /* Can not use emplace_back here since constructor is private. */ - d_ctors.push_back(DatatypeConstructor(d_solver, c)); + d_ctors.push_back(DatatypeConstructor(d_solver, *c.get())); } - d_idx = begin ? 0 : cons->size(); + d_idx = begin ? 0 : cons.size(); } Datatype::const_iterator::const_iterator() @@ -2384,6 +2712,18 @@ bool Datatype::const_iterator::operator!=( /* -------------------------------------------------------------------------- */ /* Grammar */ /* -------------------------------------------------------------------------- */ + +Grammar::Grammar() + : d_solver(nullptr), + d_sygusVars(), + d_ntSyms(), + d_ntsToTerms(0), + d_allowConst(), + d_allowVars(), + d_isResolved(false) +{ +} + Grammar::Grammar(const Solver* slv, const std::vector<Term>& sygusVars, const std::vector<Term>& ntSymbols) @@ -2411,7 +2751,7 @@ void Grammar::addRule(Term ntSymbol, Term rule) d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol) << "ntSymbol to be one of the non-terminal symbols given in the " "predeclaration"; - CVC4_API_CHECK(ntSymbol.d_expr->getType() == rule.d_expr->getType()) + CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType()) << "Expected ntSymbol and rule to have the same sort"; d_ntsToTerms[ntSymbol].push_back(rule); @@ -2432,7 +2772,7 @@ void Grammar::addRules(Term ntSymbol, std::vector<Term> rules) CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !rules[i].isNull(), "parameter rule", rules[i], i) << "non-null term"; - CVC4_API_CHECK(ntSymbol.d_expr->getType() == rules[i].d_expr->getType()) + CVC4_API_CHECK(ntSymbol.d_node->getType() == rules[i].d_node->getType()) << "Expected ntSymbol and rule at index " << i << " to have the same sort"; } @@ -2467,6 +2807,78 @@ void Grammar::addAnyVariable(Term ntSymbol) d_allowVars.insert(ntSymbol); } +/** + * this function concatinates the outputs of calling f on each element between + * first and last, seperated by sep. + * @param first the beginning of the range + * @param last the end of the range + * @param f the function to call on each element in the range, its output must + * be overloaded for operator<< + * @param sep the string to add between successive calls to f + */ +template <typename Iterator, typename Function> +std::string join(Iterator first, Iterator last, Function f, std::string sep) +{ + std::stringstream ss; + Iterator i = first; + + if (i != last) + { + ss << f(*i); + ++i; + } + + while (i != last) + { + ss << sep << f(*i); + ++i; + } + + return ss.str(); +} + +std::string Grammar::toString() const +{ + std::stringstream ss; + ss << " (" // pre-declaration + << join( + d_ntSyms.cbegin(), + d_ntSyms.cend(), + [](const Term& t) { + std::stringstream s; + s << '(' << t << ' ' << t.getSort() << ')'; + return s.str(); + }, + " ") + << ")\n (" // grouped rule listing + << join( + d_ntSyms.cbegin(), + d_ntSyms.cend(), + [this](const Term& t) { + bool allowConst = d_allowConst.find(t) != d_allowConst.cend(), + allowVars = d_allowVars.find(t) != d_allowVars.cend(); + const std::vector<Term>& rules = d_ntsToTerms.at(t); + std::stringstream s; + s << '(' << t << ' ' << t.getSort() << " (" + << (allowConst ? "(Constant " + t.getSort().toString() + ")" + : "") + << (allowConst && allowVars ? " " : "") + << (allowVars ? "(Var " + t.getSort().toString() + ")" : "") + << ((allowConst || allowVars) && !rules.empty() ? " " : "") + << join( + rules.cbegin(), + rules.cend(), + [](const Term& rule) { return rule.toString(); }, + " ") + << "))"; + return s.str(); + }, + "\n ") + << ')'; + + return ss.str(); +} + Sort Grammar::resolve() { d_isResolved = true; @@ -2487,11 +2899,11 @@ Sort Grammar::resolve() // make the unresolved type, used for referencing the final version of // the ntsymbol's datatype ntsToUnres[ntsymbol] = - Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString())); + Sort(d_solver, d_solver->getNodeManager()->mkSort(ntsymbol.toString())); } - std::vector<CVC4::Datatype> datatypes; - std::set<Type> unresTypes; + std::vector<CVC4::DType> datatypes; + std::set<TypeNode> unresTypes; datatypes.reserve(d_ntSyms.size()); @@ -2508,12 +2920,12 @@ Sort Grammar::resolve() if (d_allowVars.find(ntSym) != d_allowVars.cend()) { addSygusConstructorVariables(dtDecl, - Sort(d_solver, ntSym.d_expr->getType())); + Sort(d_solver, ntSym.d_node->getType())); } bool aci = d_allowConst.find(ntSym) != d_allowConst.end(); - Type btt = ntSym.d_expr->getType(); - dtDecl.d_dtype->setSygus(btt, *bvl.d_expr, aci, false); + TypeNode btt = ntSym.d_node->getType(); + dtDecl.d_dtype->setSygus(btt, *bvl.d_node, aci, false); // We can be in a case where the only rule specified was (Variable T) // and there are no variables of type T, in which case this is a bogus @@ -2526,9 +2938,9 @@ Sort Grammar::resolve() unresTypes.insert(*ntsToUnres[ntSym].d_type); } - std::vector<DatatypeType> datatypeTypes = - d_solver->getExprManager()->mkMutualDatatypeTypes( - datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector<TypeNode> datatypeTypes = + d_solver->getNodeManager()->mkMutualDatatypeTypes( + datatypes, unresTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); // return is the first datatype return Sort(d_solver, datatypeTypes[0]); @@ -2558,12 +2970,13 @@ void Grammar::addSygusConstructorTerm( d_solver->getExprManager()->mkExpr( CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args))); // its operator is a lambda - op = Term(d_solver, - d_solver->getExprManager()->mkExpr(CVC4::kind::LAMBDA, - {*lbvl.d_expr, *op.d_expr})); + op = Term( + d_solver, + d_solver->getExprManager()->mkExpr( + CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()})); } - dt.d_dtype->addSygusConstructor( - *op.d_expr, ssCName.str(), sortVectorToTypes(cargs)); + std::vector<TypeNode> cargst = sortVectorToTypeNodes(cargs); + dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst); } Term Grammar::purifySygusGTerm( @@ -2578,38 +2991,40 @@ Term Grammar::purifySygusGTerm( { Term ret = Term(d_solver, - d_solver->getExprManager()->mkBoundVar(term.d_expr->getType())); + d_solver->getNodeManager()->mkBoundVar(term.d_node->getType())); args.push_back(ret); cargs.push_back(itn->second); return ret; } std::vector<Term> pchildren; bool childChanged = false; - for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++) + for (unsigned i = 0, nchild = term.d_node->getNumChildren(); i < nchild; i++) { Term ptermc = purifySygusGTerm( - Term(d_solver, (*term.d_expr)[i]), args, cargs, ntsToUnres); + Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres); pchildren.push_back(ptermc); - childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i]; + childChanged = + childChanged || ptermc.d_node->toExpr() != (term.d_node->toExpr())[i]; } if (!childChanged) { return term; } - Expr nret; + Node nret; - if (term.d_expr->isParameterized()) + if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED) { // it's an indexed operator so we should provide the op - nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(), - term.d_expr->getOperator(), - termVectorToExprs(pchildren)); + NodeBuilder<> nb(term.d_node->getKind()); + nb << term.d_node->getOperator(); + nb.append(termVectorToNodes(pchildren)); + nret = nb.constructNode(); } else { - nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(), - termVectorToExprs(pchildren)); + nret = d_solver->getNodeManager()->mkNode(term.d_node->getKind(), + termVectorToNodes(pchildren)); } return Term(d_solver, nret); @@ -2622,17 +3037,21 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++) { Term v = d_sygusVars[i]; - if (v.d_expr->getType() == *sort.d_type) + if (v.d_node->getType() == *sort.d_type) { std::stringstream ss; ss << v; - std::vector<Sort> cargs; - dt.d_dtype->addSygusConstructor( - *v.d_expr, ss.str(), sortVectorToTypes(cargs)); + std::vector<TypeNode> cargs; + dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs); } } } +std::ostream& operator<<(std::ostream& out, const Grammar& g) +{ + return out << g.toString(); +} + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ @@ -2641,24 +3060,24 @@ const static std:: unordered_map<RoundingMode, CVC4::RoundingMode, RoundingModeHashFunction> s_rmodes{ {ROUND_NEAREST_TIES_TO_EVEN, - CVC4::RoundingMode::roundNearestTiesToEven}, - {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive}, - {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative}, - {ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero}, + CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, + {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_ZERO, CVC4::RoundingMode::ROUND_TOWARD_ZERO}, {ROUND_NEAREST_TIES_TO_AWAY, - CVC4::RoundingMode::roundNearestTiesToAway}, + CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, }; const static std::unordered_map<CVC4::RoundingMode, RoundingMode, CVC4::RoundingModeHashFunction> s_rmodes_internal{ - {CVC4::RoundingMode::roundNearestTiesToEven, + {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN, ROUND_NEAREST_TIES_TO_EVEN}, - {CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE}, - {CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE}, - {CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO}, - {CVC4::RoundingMode::roundNearestTiesToAway, + {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE}, + {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE}, + {CVC4::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO}, + {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY, ROUND_NEAREST_TIES_TO_AWAY}, }; @@ -2691,23 +3110,28 @@ Solver::~Solver() {} template <typename T> Term Solver::mkValHelper(T t) const { - Expr res = d_exprMgr->mkConst(t); + NodeManagerScope scope(getNodeManager()); + Node res = getNodeManager()->mkConst(t); (void)res.getType(true); /* kick off type checking */ return Term(this, res); } Term Solver::mkRealFromStrHelper(const std::string& s) const { - /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP - * throws an std::invalid_argument exception. For consistency, we treat it - * as invalid. */ - CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) - << "a string representing an integer, real or rational value."; - - CVC4::Rational r = s.find('/') != std::string::npos - ? CVC4::Rational(s) - : CVC4::Rational::fromDecimal(s); - return mkValHelper<CVC4::Rational>(r); + try + { + CVC4::Rational r = s.find('/') != std::string::npos + ? CVC4::Rational(s) + : CVC4::Rational::fromDecimal(s); + return mkValHelper<CVC4::Rational>(r); + } + catch (const std::invalid_argument& e) + { + std::stringstream message; + message << "Cannot construct Real or Int from string argument '" << s << "'" + << std::endl; + throw std::invalid_argument(message.str()); + } } Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const @@ -2760,15 +3184,28 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos && s.size() <= 5 && s.size() > 0) - << "Unexpected string for hexidecimal character " << s; + << "Unexpected string for hexadecimal character " << s; uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16)); CVC4_API_CHECK(val < String::num_codes()) - << "Not a valid code point for hexidecimal character " << s; + << "Not a valid code point for hexadecimal character " << s; std::vector<unsigned> cpts; cpts.push_back(val); return mkValHelper<CVC4::String>(CVC4::String(cpts)); } +Term Solver::getValueHelper(Term term) const +{ + Node value = d_smtEngine->getValue(*term.d_node); + Term res = Term(this, value); + // May need to wrap in real cast so that user know this is a real. + TypeNode tn = (*term.d_node).getType(); + if (!tn.isInteger() && value.getType().isInteger()) + { + return ensureRealSort(res); + } + return res; +} + Term Solver::mkTermFromKind(Kind kind) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -2796,6 +3233,7 @@ Term Solver::mkTermFromKind(Kind kind) const Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = children.size(); i < size; ++i) { @@ -2816,7 +3254,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const if (echildren.size() > 2) { if (kind == INTS_DIVISION || kind == XOR || kind == MINUS - || kind == DIVISION || kind == BITVECTOR_XNOR || kind == HO_APPLY) + || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF) { // left-associative, but CVC4 internally only supports 2 args res = d_exprMgr->mkLeftAssociative(k, echildren); @@ -2854,7 +3292,23 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const { // default case, same as above checkMkTerm(kind, children.size()); - res = d_exprMgr->mkExpr(k, echildren); + if (kind == api::SINGLETON) + { + // the type of the term is the same as the type of the internal node + // see Term::getSort() + TypeNode type = children[0].d_node->getType(); + // Internally NodeManager::mkSingleton needs a type argument + // to construct a singleton, since there is no difference between + // integers and reals (both are Rationals). + // At the API, mkReal and mkInteger are different and therefore the + // element type can be used safely here. + Node singleton = getNodeManager()->mkSingleton(type, *children[0].d_node); + res = Term(this, singleton).getExpr(); + } + else + { + res = d_exprMgr->mkExpr(k, echildren); + } } (void)res.getType(true); /* kick off type checking */ @@ -2863,12 +3317,13 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const } std::vector<Sort> Solver::mkDatatypeSortsInternal( - std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - std::vector<CVC4::Datatype> datatypes; + std::vector<CVC4::DType> datatypes; for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver, @@ -2887,14 +3342,11 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal( { CVC4_API_SOLVER_CHECK_SORT(sort); } - std::set<Type> utypes = sortSetToTypes(unresolvedSorts); - std::vector<CVC4::DatatypeType> dtypes = - d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes); - std::vector<Sort> retTypes; - for (CVC4::DatatypeType t : dtypes) - { - retTypes.push_back(Sort(this, t)); - } + + std::set<TypeNode> utypes = sortSetToTypeNodes(unresolvedSorts); + std::vector<CVC4::TypeNode> dtypes = + getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes); + std::vector<Sort> retTypes = typeNodeVectorToSorts(this, dtypes); return retTypes; CVC4_API_SOLVER_TRY_CATCH_END; @@ -2910,7 +3362,7 @@ std::vector<Type> Solver::sortVectorToTypes( for (const Sort& s : sorts) { CVC4_API_SOLVER_CHECK_SORT(s); - res.push_back(*s.d_type); + res.push_back(s.d_type->toType()); } return res; } @@ -2922,7 +3374,7 @@ std::vector<Expr> Solver::termVectorToExprs( for (const Term& t : terms) { CVC4_API_SOLVER_CHECK_TERM(t); - res.push_back(*t.d_expr); + res.push_back(t.d_node->toExpr()); } return res; } @@ -2949,55 +3401,71 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << " children (the one under construction has " << nchildren << ")"; } +/* Solver Configuration */ +/* -------------------------------------------------------------------------- */ + +bool Solver::supportsFloatingPoint() const +{ + return Configuration::isBuiltWithSymFPU(); +} + /* Sorts Handling */ /* -------------------------------------------------------------------------- */ Sort Solver::getNullSort(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, Type()); + return Sort(this, TypeNode()); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::getBooleanSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->booleanType()); + return Sort(this, getNodeManager()->booleanType()); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::getIntegerSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->integerType()); + return Sort(this, getNodeManager()->integerType()); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::getRealSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->realType()); + return Sort(this, getNodeManager()->realType()); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::getRegExpSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->regExpType()); + return Sort(this, getNodeManager()->regExpType()); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::getStringSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->stringType()); + return Sort(this, getNodeManager()->stringType()); CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::getRoundingmodeSort(void) const +Sort Solver::getRoundingModeSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->roundingModeType()); + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; + return Sort(this, getNodeManager()->roundingModeType()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3005,6 +3473,7 @@ Sort Solver::getRoundingmodeSort(void) const Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort) << "non-null index sort"; @@ -3013,42 +3482,47 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const CVC4_API_SOLVER_CHECK_SORT(indexSort); CVC4_API_SOLVER_CHECK_SORT(elemSort); - return Sort(this, - d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type)); + return Sort( + this, getNodeManager()->mkArrayType(*indexSort.d_type, *elemSort.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkBitVectorSort(uint32_t size) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; - return Sort(this, d_exprMgr->mkBitVectorType(size)); + return Sort(this, getNodeManager()->mkBitVectorType(size)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; - return Sort(this, d_exprMgr->mkFloatingPointType(exp, sig)); + return Sort(this, getNodeManager()->mkFloatingPointType(exp, sig)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(this == dtypedecl.d_solver) << "Given datatype declaration is not associated with this solver"; CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) << "a datatype declaration with at least one constructor"; - return Sort(this, d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype)); + return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl.d_dtype)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3056,18 +3530,24 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const std::vector<Sort> Solver::mkDatatypeSorts( std::vector<DatatypeDecl>& dtypedecls) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::set<Sort> unresolvedSorts; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); + CVC4_API_SOLVER_TRY_CATCH_END; } -std::vector<Sort> Solver::mkDatatypeSorts(std::vector<DatatypeDecl>& dtypedecls, - std::set<Sort>& unresolvedSorts) const +std::vector<Sort> Solver::mkDatatypeSorts( + const std::vector<DatatypeDecl>& dtypedecls, + const std::set<Sort>& unresolvedSorts) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); + CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) << "non-null codomain sort"; @@ -3079,14 +3559,15 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const << "first-class sort as codomain sort for function sort"; Assert(!codomain.isFunction()); /* A function sort is not first-class. */ - return Sort(this, - d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type)); + return Sort( + this, getNodeManager()->mkFunctionType(*domain.d_type, *codomain.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for function sort"; @@ -3109,22 +3590,26 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const << "first-class sort as codomain sort for function sort"; Assert(!codomain.isFunction()); /* A function sort is not first-class. */ - std::vector<Type> argTypes = sortVectorToTypes(sorts); - return Sort(this, d_exprMgr->mkFunctionType(argTypes, *codomain.d_type)); + std::vector<TypeNode> argTypes = sortVectorToTypeNodes(sorts); + return Sort(this, + getNodeManager()->mkFunctionType(argTypes, *codomain.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkParamSort(const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, - d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER)); + return Sort( + this, + getNodeManager()->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for predicate sort"; @@ -3140,9 +3625,9 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const sorts[i].isFirstClass(), "parameter sort", sorts[i], i) << "first-class sort as parameter sort for predicate sort"; } - std::vector<Type> types = sortVectorToTypes(sorts); + std::vector<TypeNode> types = sortVectorToTypeNodes(sorts); - return Sort(this, d_exprMgr->mkPredicateType(types)); + return Sort(this, getNodeManager()->mkPredicateType(types)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3150,6 +3635,7 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const Sort Solver::mkRecordSort( const std::vector<std::pair<std::string, Sort>>& fields) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::vector<std::pair<std::string, Type>> f; size_t i = 0; @@ -3162,58 +3648,76 @@ Sort Solver::mkRecordSort( this == p.second.d_solver, "parameter sort", p.second, i) << "sort associated to this solver object"; i += 1; - f.emplace_back(p.first, *p.second.d_type); + f.emplace_back(p.first, p.second.d_type->toType()); } - return Sort(this, d_exprMgr->mkRecordType(Record(f))); + return Sort(this, getNodeManager()->mkRecordType(Record(f))); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkSetSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; CVC4_API_SOLVER_CHECK_SORT(elemSort); - return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type)); + return Sort(this, getNodeManager()->mkSetType(*elemSort.d_type)); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Sort Solver::mkBagSort(Sort elemSort) const +{ + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) + << "non-null element sort"; + CVC4_API_SOLVER_CHECK_SORT(elemSort); + + return Sort(this, getNodeManager()->mkBagType(*elemSort.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkSequenceSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; CVC4_API_SOLVER_CHECK_SORT(elemSort); - return Sort(this, d_exprMgr->mkSequenceType(*elemSort.d_type)); + return Sort(this, getNodeManager()->mkSequenceType(*elemSort.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkUninterpretedSort(const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return Sort(this, d_exprMgr->mkSort(symbol)); + return Sort(this, getNodeManager()->mkSort(symbol)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; - return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity)); + return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity)); CVC4_API_SOLVER_TRY_CATCH_END; } Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = sorts.size(); i < size; ++i) { @@ -3227,9 +3731,8 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) << "non-function-like sort as parameter sort for tuple sort"; } - std::vector<Type> types = sortVectorToTypes(sorts); - - return Sort(this, d_exprMgr->mkTupleType(types)); + std::vector<TypeNode> typeNodes = sortVectorToTypeNodes(sorts); + return Sort(this, getNodeManager()->mkTupleType(typeNodes)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3270,76 +3773,66 @@ Term Solver::mkPi() const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(const char* s) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - - return mkRealFromStrHelper(std::string(s)); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(const std::string& s) const +Term Solver::mkInteger(const std::string& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkRealFromStrHelper(s); + CVC4_API_ARG_CHECK_EXPECTED(std::regex_match(s, std::regex("-?\\d+")), s) + << " an integer "; + Term integer = mkRealFromStrHelper(s); + CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s) + << " an integer"; + return integer; CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(int32_t val) const +Term Solver::mkInteger(int64_t val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + Term integer = mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + Assert(integer.getSort() == getIntegerSort()); + return integer; CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(int64_t val) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(uint32_t val) const +Term Solver::mkReal(const std::string& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP + * throws an std::invalid_argument exception. For consistency, we treat it + * as invalid. */ + CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) + << "a string representing a real or rational value."; + Term rational = mkRealFromStrHelper(s); + return ensureRealSort(rational); CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(uint64_t val) const +Term Solver::ensureRealSort(const Term t) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); - CVC4_API_SOLVER_TRY_CATCH_END; + CVC4_API_ARG_CHECK_EXPECTED( + t.getSort() == getIntegerSort() || t.getSort() == getRealSort(), + " an integer or real term"); + if (t.getSort() == getIntegerSort()) + { + Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node); + return Term(this, n); + } + return t; } -Term Solver::mkReal(int32_t num, int32_t den) const +Term Solver::mkReal(int64_t val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + return ensureRealSort(rational); CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(int64_t num, int64_t den) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(uint32_t num, uint32_t den) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(uint64_t num, uint64_t den) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + return ensureRealSort(rational); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3375,29 +3868,36 @@ Term Solver::mkEmptySet(Sort s) const CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s) << "set sort associated to this solver object"; - return mkValHelper<CVC4::EmptySet>( - CVC4::EmptySet(TypeNode::fromType(*s.d_type))); + return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkSepNil(Sort sort) const +Term Solver::mkEmptyBag(Sort s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - CVC4_API_SOLVER_CHECK_SORT(sort); + CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isBag(), s) + << "null sort or bag sort"; - Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); + CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s) + << "bag sort associated to this solver object"; + + return mkValHelper<CVC4::EmptyBag>(CVC4::EmptyBag(*s.d_type)); CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkString(const char* s, bool useEscSequences) const +Term Solver::mkSepNil(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences)); + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); + + Node res = + getNodeManager()->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3429,14 +3929,6 @@ Term Solver::mkChar(const std::string& s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkChar(const char* s) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - return mkCharFromStrHelper(std::string(s)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkEmptySequence(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3444,8 +3936,7 @@ Term Solver::mkEmptySequence(Sort sort) const CVC4_API_SOLVER_CHECK_SORT(sort); std::vector<Node> seq; - Expr res = - d_exprMgr->mkConst(Sequence(TypeNode::fromType(*sort.d_type), seq)); + Expr res = d_exprMgr->mkConst(Sequence(*sort.d_type, seq)); return Term(this, res); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3457,8 +3948,8 @@ Term Solver::mkUniverseSet(Sort sort) const CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - Expr res = - d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET); + Node res = getNodeManager()->mkNullaryOperator(*sort.d_type, + CVC4::kind::UNIVERSE_SET); // TODO(#2771): Reenable? // (void)res->getType(true); /* kick off type checking */ return Term(this, res); @@ -3473,16 +3964,6 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkBitVector(const char* s, uint32_t base) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - - return mkBVFromStrHelper(std::string(s), base); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkBitVector(const std::string& s, uint32_t base) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3490,15 +3971,9 @@ Term Solver::mkBitVector(const std::string& s, uint32_t base) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - return mkBVFromStrHelper(size, s, base); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const +Term Solver::mkBitVector(uint32_t size, + const std::string& s, + uint32_t base) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkBVFromStrHelper(size, s, base); @@ -3514,10 +3989,17 @@ Term Solver::mkConstArray(Sort sort, Term val) const CVC4_API_SOLVER_CHECK_SORT(sort); CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_CHECK(sort.isArray()) << "Not an array sort."; - CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort())) + CVC4_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort())) << "Value does not match element sort."; - Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll( - TypeNode::fromType(*sort.d_type), Node::fromExpr(*val.d_expr))); + // handle the special case of (CAST_TO_REAL n) where n is an integer + Node n = *val.d_node; + if (val.isCastedReal()) + { + // this is safe because the constant array stores its type + n = n[0]; + } + Term res = mkValHelper<CVC4::ArrayStoreAll>( + CVC4::ArrayStoreAll(*sort.d_type, n)); return res; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3585,6 +4067,8 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const Term Solver::mkRoundingMode(RoundingMode rm) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3596,7 +4080,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const CVC4_API_SOLVER_CHECK_SORT(sort); return mkValHelper<CVC4::UninterpretedConstant>( - CVC4::UninterpretedConstant(TypeNode::fromType(*sort.d_type), index)); + CVC4::UninterpretedConstant(*sort.d_type, index)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3609,7 +4093,7 @@ Term Solver::mkAbstractValue(const std::string& index) const CVC4::Integer idx(index, 10); CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) << "a string representing an integer > 0"; - return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(idx))); + return Term(this, getNodeManager()->mkConst(CVC4::AbstractValue(idx))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away CVC4_API_SOLVER_TRY_CATCH_END; @@ -3620,7 +4104,8 @@ Term Solver::mkAbstractValue(uint64_t index) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; - return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)))); + return Term(this, + getNodeManager()->mkConst(CVC4::AbstractValue(Integer(index)))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away CVC4_API_SOLVER_TRY_CATCH_END; @@ -3639,11 +4124,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term"; CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_ARG_CHECK_EXPECTED( - val.getSort().isBitVector() && val.d_expr->isConst(), val) + val.getSort().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; return mkValHelper<CVC4::FloatingPoint>( - CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>())); + CVC4::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>())); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3653,12 +4138,26 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const Term Solver::mkConst(Sort sort, const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type) - : d_exprMgr->mkVar(symbol, *sort.d_type); + Expr res = d_exprMgr->mkVar(symbol, sort.d_type->toType()); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::mkConst(Sort sort) const +{ + NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); + + Expr res = d_exprMgr->mkVar(sort.d_type->toType()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3674,8 +4173,9 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type) - : d_exprMgr->mkBoundVar(symbol, *sort.d_type); + Expr res = symbol.empty() + ? d_exprMgr->mkBoundVar(sort.d_type->toType()) + : d_exprMgr->mkBoundVar(symbol, sort.d_type->toType()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3688,6 +4188,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( const std::string& name) { + NodeManagerScope scope(getNodeManager()); return DatatypeConstructorDecl(this, name); } @@ -3696,6 +4197,7 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { + NodeManagerScope scope(getNodeManager()); return DatatypeDecl(this, name, isCoDatatype); } @@ -3703,6 +4205,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, Sort param, bool isCoDatatype) { + NodeManagerScope scope(getNodeManager()); return DatatypeDecl(this, name, param, isCoDatatype); } @@ -3710,6 +4213,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, const std::vector<Sort>& params, bool isCoDatatype) { + NodeManagerScope scope(getNodeManager()); return DatatypeDecl(this, name, params, isCoDatatype); } @@ -3725,33 +4229,12 @@ Term Solver::mkTerm(Kind kind) const Term Solver::mkTerm(Kind kind, Term child) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; - CVC4_API_SOLVER_CHECK_TERM(child); - checkMkTerm(kind, 1); - - Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); - - CVC4_API_SOLVER_TRY_CATCH_END; + return mkTermHelper(kind, std::vector<Term>{child}); } Term Solver::mkTerm(Kind kind, Term child1, Term child2) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - CVC4_API_SOLVER_CHECK_TERM(child1); - CVC4_API_SOLVER_CHECK_TERM(child2); - checkMkTerm(kind, 2); - - Expr res = - d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr); - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); - - CVC4_API_SOLVER_TRY_CATCH_END; + return mkTermHelper(kind, std::vector<Term>{child1, child2}); } Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const @@ -3767,21 +4250,20 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const Term Solver::mkTerm(Op op) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); + checkMkTerm(op.d_kind, 0); - Term res; - if (op.isIndexedHelper()) + if (!op.isIndexedHelper()) { - const CVC4::Kind int_kind = extToIntKind(op.d_kind); - res = Term(this, d_exprMgr->mkExpr(int_kind, *op.d_expr)); - } - else - { - res = mkTermFromKind(op.d_kind); + return mkTermFromKind(op.d_kind); } - (void)res.d_expr->getType(true); /* kick off type checking */ + const CVC4::Kind int_kind = extToIntKind(op.d_kind); + Term res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node)); + + (void)res.d_node->getType(true); /* kick off type checking */ return res; CVC4_API_SOLVER_TRY_CATCH_END; @@ -3789,88 +4271,35 @@ Term Solver::mkTerm(Op op) const Term Solver::mkTerm(Op op, Term child) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_SOLVER_CHECK_OP(op); - CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; - CVC4_API_SOLVER_CHECK_TERM(child); - - const CVC4::Kind int_kind = extToIntKind(op.d_kind); - Expr res; - if (op.isIndexedHelper()) - { - res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr); - } - else - { - res = d_exprMgr->mkExpr(int_kind, *child.d_expr); - } - - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); - - CVC4_API_SOLVER_TRY_CATCH_END; + return mkTermHelper(op, std::vector<Term>{child}); } Term Solver::mkTerm(Op op, Term child1, Term child2) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_SOLVER_CHECK_OP(op); - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - CVC4_API_SOLVER_CHECK_TERM(child1); - CVC4_API_SOLVER_CHECK_TERM(child2); - - const CVC4::Kind int_kind = extToIntKind(op.d_kind); - Expr res; - if (op.isIndexedHelper()) - { - res = - d_exprMgr->mkExpr(int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr); - } - else - { - res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr); - } - - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); - CVC4_API_SOLVER_TRY_CATCH_END; + return mkTermHelper(op, std::vector<Term>{child1, child2}); } Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_SOLVER_CHECK_OP(op); - CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; - CVC4_API_SOLVER_CHECK_TERM(child1); - CVC4_API_SOLVER_CHECK_TERM(child2); - CVC4_API_SOLVER_CHECK_TERM(child3); - - const CVC4::Kind int_kind = extToIntKind(op.d_kind); - Expr res; - if (op.isIndexedHelper()) - { - res = d_exprMgr->mkExpr( - int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); - } - else - { - res = d_exprMgr->mkExpr( - int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr); - } - - (void)res.getType(true); /* kick off type checking */ - return Term(this, res); - - CVC4_API_SOLVER_TRY_CATCH_END; + return mkTermHelper(op, std::vector<Term>{child1, child2, child3}); } Term Solver::mkTerm(Op op, const std::vector<Term>& children) const { + return mkTermHelper(op, children); +} + +Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const +{ + if (!op.isIndexedHelper()) + { + return mkTermHelper(op.d_kind, children); + } + + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); + checkMkTerm(op.d_kind, children.size()); for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -3882,16 +4311,12 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const } const CVC4::Kind int_kind = extToIntKind(op.d_kind); - std::vector<Expr> echildren = termVectorToExprs(children); - Expr res; - if (op.isIndexedHelper()) - { - res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren); - } - else - { - res = d_exprMgr->mkExpr(int_kind, echildren); - } + std::vector<Node> echildren = termVectorToNodes(children); + + NodeBuilder<> nb(int_kind); + nb << *op.d_node; + nb.append(echildren); + Node res = nb.constructNode(); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3902,10 +4327,11 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const Term Solver::mkTuple(const std::vector<Sort>& sorts, const std::vector<Term>& terms) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; - std::vector<CVC4::Expr> args; + std::vector<CVC4::Node> args; for (size_t i = 0, size = sorts.size(); i < size; i++) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( @@ -3914,14 +4340,15 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == sorts[i].d_solver, "child sort", sorts[i], i) << "child sort associated to this solver object"; - args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr); + args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); } Sort s = mkTupleSort(sorts); Datatype dt = s.getDatatype(); - Expr res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR), - *dt[0].getConstructorTerm().d_expr, - args); + NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR)); + nb << *dt[0].getConstructorTerm().d_node; + nb.append(args); + Node res = nb.constructNode(); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -3949,10 +4376,9 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const Op res; if (kind == RECORD_UPDATE) { - res = Op( - this, - kind, - *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get()); + res = Op(this, + kind, + *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_node); } else { @@ -3964,7 +4390,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const res = Op(this, kind, *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg))) - .d_expr.get()); + .d_node); } return res; @@ -3980,81 +4406,78 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const switch (kind) { case DIVISIBLE: - res = - Op(this, - kind, - *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get()); + res = Op(this, + kind, + *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_node); break; case BITVECTOR_REPEAT: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) - .d_expr.get()); + mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) + .d_node->toExpr()); break; case BITVECTOR_ZERO_EXTEND: res = Op(this, kind, *mkValHelper<CVC4::BitVectorZeroExtend>( CVC4::BitVectorZeroExtend(arg)) - .d_expr.get()); + .d_node); break; case BITVECTOR_SIGN_EXTEND: res = Op(this, kind, *mkValHelper<CVC4::BitVectorSignExtend>( CVC4::BitVectorSignExtend(arg)) - .d_expr.get()); + .d_node); break; case BITVECTOR_ROTATE_LEFT: res = Op(this, kind, *mkValHelper<CVC4::BitVectorRotateLeft>( CVC4::BitVectorRotateLeft(arg)) - .d_expr.get()); + .d_node); break; case BITVECTOR_ROTATE_RIGHT: res = Op(this, kind, *mkValHelper<CVC4::BitVectorRotateRight>( CVC4::BitVectorRotateRight(arg)) - .d_expr.get()); + .d_node); break; case INT_TO_BITVECTOR: - res = Op(this, - kind, - *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) - .d_expr.get()); + res = Op( + this, + kind, + *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)).d_node); break; case IAND: - res = Op(this, - kind, - *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_expr.get()); + res = + Op(this, kind, *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_node); break; case FLOATINGPOINT_TO_UBV: res = Op( this, kind, *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_SBV: res = Op( this, kind, *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg)) - .d_expr.get()); + .d_node); break; case TUPLE_UPDATE: - res = Op( - this, - kind, - *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get()); - break; - case REGEXP_REPEAT: res = Op(this, kind, - *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg)) - .d_expr.get()); + *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_node); + break; + case REGEXP_REPEAT: + res = + Op(this, + kind, + *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg)).d_node); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -4079,55 +4502,55 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const kind, *mkValHelper<CVC4::BitVectorExtract>( CVC4::BitVectorExtract(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: res = Op(this, kind, *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_FLOATINGPOINT: res = Op(this, kind, *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_REAL: res = Op(this, kind, *mkValHelper<CVC4::FloatingPointToFPReal>( CVC4::FloatingPointToFPReal(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: res = Op(this, kind, *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: res = Op(this, kind, *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) - .d_expr.get()); + .d_node); break; case FLOATINGPOINT_TO_FP_GENERIC: res = Op(this, kind, *mkValHelper<CVC4::FloatingPointToFPGeneric>( CVC4::FloatingPointToFPGeneric(arg1, arg2)) - .d_expr.get()); + .d_node); break; case REGEXP_LOOP: - res = Op(this, - kind, - *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2)) - .d_expr.get()); + res = Op( + this, + kind, + *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2)).d_node); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -4145,10 +4568,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const Term Solver::simplify(const Term& term) { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->simplify(*term.d_expr)); + return Term(this, d_smtEngine->simplify(term.d_node->toExpr())); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4164,7 +4588,7 @@ Result Solver::checkEntailed(Term term) const CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr); + CVC4::Result r = d_smtEngine->checkEntailed(*term.d_node); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4184,7 +4608,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector<Expr> exprs = termVectorToExprs(terms); + std::vector<Node> exprs = termVectorToNodes(terms); CVC4::Result r = d_smtEngine->checkEntailed(exprs); return Result(r); @@ -4202,7 +4626,7 @@ void Solver::assertFormula(Term term) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); - d_smtEngine->assertFormula(Node::fromExpr(*term.d_expr)); + d_smtEngine->assertFormula(*term.d_node); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4234,7 +4658,7 @@ Result Solver::checkSatAssuming(Term assumption) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4_API_SOLVER_CHECK_TERM(assumption); - CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr); + CVC4::Result r = d_smtEngine->checkSat(*assumption.d_node); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4255,7 +4679,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector<Expr> eassumptions = termVectorToExprs(assumptions); + std::vector<Node> eassumptions = termVectorToNodes(assumptions); CVC4::Result r = d_smtEngine->checkSat(eassumptions); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4281,7 +4705,7 @@ Sort Solver::declareDatatype( << "datatype constructor declaration associated to this solver object"; dtdecl.addConstructor(ctors[i]); } - return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype)); + return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl.d_dtype)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4306,13 +4730,13 @@ Term Solver::declareFun(const std::string& symbol, << "first-class sort as function codomain sort"; CVC4_API_SOLVER_CHECK_SORT(sort); Assert(!sort.isFunction()); /* A function sort is not first-class. */ - Type type = *sort.d_type; + TypeNode type = *sort.d_type; if (!sorts.empty()) { - std::vector<Type> types = sortVectorToTypes(sorts); - type = d_exprMgr->mkFunctionType(types, type); + std::vector<TypeNode> types = sortVectorToTypeNodes(sorts); + type = getNodeManager()->mkFunctionType(types, type); } - return Term(this, d_exprMgr->mkVar(symbol, type)); + return Term(this, d_exprMgr->mkVar(symbol, type.toType())); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4322,8 +4746,11 @@ Term Solver::declareFun(const std::string& symbol, Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol)); - return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity)); + if (arity == 0) + { + return Sort(this, getNodeManager()->mkSort(symbol)); + } + return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4339,19 +4766,19 @@ Term Solver::defineFun(const std::string& symbol, CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as codomain sort for function sort"; - std::vector<Type> domain_types; + std::vector<TypeNode> domain_types; for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) << "a bound variable"; - CVC4::Type t = bound_vars[i].d_expr->getType(); + CVC4::TypeNode t = bound_vars[i].d_node->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; @@ -4361,14 +4788,15 @@ Term Solver::defineFun(const std::string& symbol, CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; - Type type = *sort.d_type; + NodeManager* nm = getNodeManager(); + TypeNode type = *sort.d_type; if (!domain_types.empty()) { - type = d_exprMgr->mkFunctionType(domain_types, type); + type = nm->mkFunctionType(domain_types, type); } - Expr fun = d_exprMgr->mkVar(symbol, type); - std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr, global); + Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType())); + std::vector<Node> ebound_vars = termVectorToNodes(bound_vars); + d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4392,7 +4820,7 @@ Term Solver::defineFun(Term fun, this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) @@ -4417,8 +4845,8 @@ Term Solver::defineFun(Term fun, CVC4_API_SOLVER_CHECK_TERM(term); - std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr, global); + std::vector<Node> ebound_vars = termVectorToNodes(bound_vars); + d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4432,6 +4860,7 @@ Term Solver::defineFunRec(const std::string& symbol, Term term, bool global) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -4444,19 +4873,19 @@ Term Solver::defineFunRec(const std::string& symbol, CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as function codomain sort"; Assert(!sort.isFunction()); /* A function sort is not first-class. */ - std::vector<Type> domain_types; + std::vector<TypeNode> domain_types; for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) << "a bound variable"; - CVC4::Type t = bound_vars[i].d_expr->getType(); + CVC4::TypeNode t = bound_vars[i].d_node->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; @@ -4467,14 +4896,16 @@ Term Solver::defineFunRec(const std::string& symbol, << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; CVC4_API_SOLVER_CHECK_TERM(term); - Type type = *sort.d_type; + NodeManager* nm = getNodeManager(); + TypeNode type = *sort.d_type; if (!domain_types.empty()) { - type = d_exprMgr->mkFunctionType(domain_types, type); + type = nm->mkFunctionType(domain_types, type); } - Expr fun = d_exprMgr->mkVar(symbol, type); - std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr, global); + Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType())); + std::vector<Node> ebound_vars = termVectorToNodes(bound_vars); + d_smtEngine->defineFunctionRec( + fun, ebound_vars, term.d_node->toExpr(), global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4484,6 +4915,7 @@ Term Solver::defineFunRec(Term fun, Term term, bool global) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -4505,7 +4937,7 @@ Term Solver::defineFunRec(Term fun, this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bound_vars[i], i) @@ -4529,9 +4961,9 @@ Term Solver::defineFunRec(Term fun, } CVC4_API_SOLVER_CHECK_TERM(term); - std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); + std::vector<Node> ebound_vars = termVectorToNodes(bound_vars); d_smtEngine->defineFunctionRec( - *fun.d_expr, ebound_vars, *term.d_expr, global); + *fun.d_node, ebound_vars, *term.d_node, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4544,6 +4976,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, const std::vector<Term>& terms, bool global) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -4581,7 +5014,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, this == bvars[k].d_solver, "bound variable", bvars[k], k) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", bvars[k], k) @@ -4606,13 +5039,13 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, << "function or nullary symbol"; } } - std::vector<Expr> efuns = termVectorToExprs(funs); - std::vector<std::vector<Expr>> ebound_vars; + std::vector<Node> efuns = termVectorToNodes(funs); + std::vector<std::vector<Node>> ebound_vars; for (const auto& v : bound_vars) { - ebound_vars.push_back(termVectorToExprs(v)); + ebound_vars.push_back(termVectorToNodes(v)); } - std::vector<Expr> exprs = termVectorToExprs(terms); + std::vector<Node> exprs = termVectorToNodes(terms); d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4631,12 +5064,12 @@ void Solver::echo(std::ostream& out, const std::string& str) const std::vector<Term> Solver::getAssertions(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - std::vector<Expr> assertions = d_smtEngine->getAssertions(); + std::vector<Node> assertions = d_smtEngine->getAssertions(); /* Can not use * return std::vector<Term>(assertions.begin(), assertions.end()); * here since constructor is private */ std::vector<Term> res; - for (const Expr& e : assertions) + for (const Node& e : assertions) { res.push_back(Term(this, e)); } @@ -4645,26 +5078,6 @@ std::vector<Term> Solver::getAssertions(void) const } /** - * ( get-assignment ) - */ -std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceAssignments]) - << "Cannot get assignment unless assignment generation is enabled " - "(try --produce-assignments)"; - std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment(); - std::vector<std::pair<Term, Term>> res; - for (const auto& p : assignment) - { - res.emplace_back(Term(this, p.first), Term(this, p.second)); - } - return res; - CVC4_API_SOLVER_TRY_CATCH_END; -} - -/** * ( get-info <info_flag> ) */ std::string Solver::getInfo(const std::string& flag) const @@ -4701,18 +5114,17 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - == SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat assumptions unless in unsat mode."; - std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions(); + std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions(); /* Can not use * return std::vector<Term>(uassumptions.begin(), uassumptions.end()); * here since constructor is private */ std::vector<Term> res; - for (const Expr& e : uassumptions) + for (const Node& e : uassumptions) { - res.push_back(Term(this, e)); + res.push_back(Term(this, e.toExpr())); } return res; CVC4_API_SOLVER_TRY_CATCH_END; @@ -4728,15 +5140,14 @@ std::vector<Term> Solver::getUnsatCore(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - == SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat core unless in unsat mode."; UnsatCore core = d_smtEngine->getUnsatCore(); /* Can not use * return std::vector<Term>(core.begin(), core.end()); * here since constructor is private */ std::vector<Term> res; - for (const Expr& e : core) + for (const Node& e : core) { res.push_back(Term(this, e)); } @@ -4751,7 +5162,7 @@ Term Solver::getValue(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->getValue(*term.d_expr)); + return getValueHelper(term); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4762,12 +5173,11 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) - << "Cannot get value when in unsat mode."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Cannot get value unless after a SAT or unknown response."; std::vector<Term> res; for (size_t i = 0, n = terms.size(); i < n; ++i) { @@ -4775,12 +5185,45 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const this == terms[i].d_solver, "term", terms[i], i) << "term associated to this solver object"; /* Can not use emplace_back here since constructor is private. */ - res.push_back(Term(this, d_smtEngine->getValue(*terms[i].d_expr))); + res.push_back(getValueHelper(terms[i])); } return res; CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::getQuantifierElimination(api::Term q) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(q); + CVC4_API_SOLVER_CHECK_TERM(q); + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + return Term(this, + d_smtEngine->getQuantifierElimination(q.getNode(), true, true)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::getQuantifierEliminationDisjunct(api::Term q) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(q); + CVC4_API_SOLVER_CHECK_TERM(q); + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + return Term( + this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +void Solver::declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK( + d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + << "Cannot obtain separation logic expressions if not using the " + "separation logic theory."; + d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode()); + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::getSeparationHeap() const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4792,16 +5235,8 @@ Term Solver::getSeparationHeap() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) - << "Cannot get separtion heap term when in unsat mode."; - - theory::TheoryModel* m = - d_smtEngine->getAvailableModel("get separation logic heap and nil"); - Expr heap, nil; - bool hasHeapModel = m->getHeapModel(heap, nil); - CVC4_API_CHECK(hasHeapModel) - << "Failed to obtain heap term from theory model."; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only get separtion heap term after sat or unknown response."; return Term(this, d_smtEngine->getSepHeapExpr()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4817,17 +5252,9 @@ Term Solver::getSeparationNilTerm() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) - << "Cannot get separtion nil term when in unsat mode."; - - theory::TheoryModel* m = - d_smtEngine->getAvailableModel("get separation logic heap and nil"); - Expr heap, nil; - bool hasHeapModel = m->getHeapModel(heap, nil); - CVC4_API_CHECK(hasHeapModel) - << "Failed to obtain nil term from theory model."; - return Term(this, nil); + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only get separtion nil term after sat or unknown response."; + return Term(this, d_smtEngine->getSepNilExpr()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4854,39 +5281,103 @@ void Solver::pop(uint32_t nscopes) const bool Solver::getInterpolant(Term conj, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - Expr result; - bool success = d_smtEngine->getInterpol(*conj.d_expr, result); - if (success) { - output = Term(output.d_solver, result); + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + Node result; + bool success = d_smtEngine->getInterpol(*conj.d_node, result); + if (success) + { + output = Term(this, result); + } + return success; + CVC4_API_SOLVER_TRY_CATCH_END; +} + +bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + Node result; + bool success = + d_smtEngine->getInterpol(*conj.d_node, *g.resolve().d_type, result); + if (success) + { + output = Term(this, result); + } + return success; + CVC4_API_SOLVER_TRY_CATCH_END; +} + +bool Solver::getAbduct(Term conj, Term& output) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + Node result; + bool success = d_smtEngine->getAbduct(*conj.d_node, result); + if (success) + { + output = Term(this, result); } return success; CVC4_API_SOLVER_TRY_CATCH_END; } -bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const +bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - Expr result; - bool success = d_smtEngine->getInterpol(*conj.d_expr, gtype, result); + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + Node result; + bool success = + d_smtEngine->getAbduct(*conj.d_node, *g.resolve().d_type, result); if (success) { - output = Term(output.d_solver, result); + output = Term(this, result); } return success; CVC4_API_SOLVER_TRY_CATCH_END; } -void Solver::printModel(std::ostream& out) const +void Solver::blockModel() const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) - << "Cannot get value when in unsat mode."; - out << *d_smtEngine->getModel(); + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only block model after sat or unknown response."; + d_smtEngine->blockModel(); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +void Solver::blockModelValues(const std::vector<Term>& terms) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + << "Cannot get value unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Can only block model values after sat or unknown response."; + CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) + << "a non-empty set of terms"; + for (size_t i = 0, tsize = terms.size(); i < tsize; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !terms[i].isNull(), "term", terms[i], i) + << "a non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == terms[i].d_solver, "term", terms[i], i) + << "a term associated to this solver object"; + } + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + d_smtEngine->blockModelValues(termVectorToNodes(terms)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +void Solver::printInstantiations(std::ostream& out) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + d_smtEngine->printInstantiations(out); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4995,7 +5486,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const // in the theory. res = Term(this, d_exprMgr->mkExpr(extToIntKind(DIVISION), - *res.d_expr, + res.d_node->toExpr(), d_exprMgr->mkConst(CVC4::Rational(1)))); } Assert(res.getSort() == sort); @@ -5008,7 +5499,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const CVC4_API_ARG_CHECK_NOT_NULL(sort); CVC4_API_SOLVER_CHECK_SORT(sort); - Expr res = d_exprMgr->mkBoundVar(symbol, *sort.d_type); + Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ d_smtEngine->declareSygusVar(symbol, res, *sort.d_type); @@ -5023,7 +5514,7 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars, { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols) - << "non-empty vector"; + << "a non-empty vector"; for (size_t i = 0, n = boundVars.size(); i < n; ++i) { @@ -5031,30 +5522,30 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars, this == boundVars[i].d_solver, "bound variable", boundVars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + !boundVars[i].isNull(), "bound variable", boundVars[i], i) + << "a non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", boundVars[i], i) << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "parameter term", boundVars[i], i) - << "non-null term"; } for (size_t i = 0, n = ntSymbols.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == ntSymbols[i].d_solver, "term", ntSymbols[i], i) + this == ntSymbols[i].d_solver, "non-terminal", ntSymbols[i], i) << "term associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - ntSymbols[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", + !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i) + << "a non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, + "non-terminal", ntSymbols[i], i) << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i) - << "non-null term"; } return Grammar(this, boundVars, ntSymbols); @@ -5080,7 +5571,7 @@ Term Solver::synthInv(const std::string& symbol, const std::vector<Term>& boundVars) const { return synthFunHelper( - symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true); + symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true); } Term Solver::synthInv(const std::string& symbol, @@ -5088,7 +5579,7 @@ Term Solver::synthInv(const std::string& symbol, Grammar& g) const { return synthFunHelper( - symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true, &g); + symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true, &g); } Term Solver::synthFunHelper(const std::string& symbol, @@ -5100,47 +5591,43 @@ Term Solver::synthFunHelper(const std::string& symbol, CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(sort); - CVC4_API_ARG_CHECK_EXPECTED(sort.d_type->isFirstClass(), sort) - << "first-class sort as codomain sort for function sort"; - - std::vector<Type> varTypes; + std::vector<TypeNode> varTypes; for (size_t i = 0, n = boundVars.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == boundVars[i].d_solver, "bound variable", boundVars[i], i) << "bound variable associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + !boundVars[i].isNull(), "bound variable", boundVars[i], i) + << "a non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, "bound variable", boundVars[i], i) << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "parameter term", boundVars[i], i) - << "non-null term"; - varTypes.push_back(boundVars[i].d_expr->getType()); + varTypes.push_back(boundVars[i].d_node->getType()); } CVC4_API_SOLVER_CHECK_SORT(sort); if (g != nullptr) { - CVC4_API_CHECK(g->d_ntSyms[0].d_expr->getType() == *sort.d_type) + CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType() == *sort.d_type) << "Invalid Start symbol for Grammar g, Expected Start's sort to be " - << *sort.d_type; + << *sort.d_type << " but found " << g->d_ntSyms[0].d_node->getType(); } - Type funType = varTypes.empty() - ? *sort.d_type - : d_exprMgr->mkFunctionType(varTypes, *sort.d_type); + TypeNode funType = varTypes.empty() ? *sort.d_type + : getNodeManager()->mkFunctionType( + varTypes, *sort.d_type); - Expr fun = d_exprMgr->mkBoundVar(symbol, funType); + Node fun = getNodeManager()->mkBoundVar(symbol, funType); (void)fun.getType(true); /* kick off type checking */ - d_smtEngine->declareSynthFun(symbol, - fun, - g == nullptr ? funType : *g->resolve().d_type, - isInv, - termVectorToExprs(boundVars)); + std::vector<Node> bvns = termVectorToNodes(boundVars); + + d_smtEngine->declareSynthFun( + symbol, fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); return Term(this, fun); @@ -5150,13 +5637,14 @@ Term Solver::synthFunHelper(const std::string& symbol, void Solver::addSygusConstraint(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + NodeManagerScope scope(getNodeManager()); CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_EXPECTED( - term.d_expr->getType() == d_exprMgr->booleanType(), term) + term.d_node->getType() == getNodeManager()->booleanType(), term) << "boolean term"; - d_smtEngine->assertSygusConstraint(*term.d_expr); + d_smtEngine->assertSygusConstraint(*term.d_node); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5175,24 +5663,24 @@ void Solver::addSygusInvConstraint(Term inv, CVC4_API_ARG_CHECK_NOT_NULL(post); CVC4_API_SOLVER_CHECK_TERM(post); - CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv) + CVC4_API_ARG_CHECK_EXPECTED(inv.d_node->getType().isFunction(), inv) << "a function"; - FunctionType invType = inv.d_expr->getType(); + TypeNode invType = inv.d_node->getType(); CVC4_API_ARG_CHECK_EXPECTED(invType.getRangeType().isBoolean(), inv) << "boolean range"; - CVC4_API_CHECK(pre.d_expr->getType() == invType) + CVC4_API_CHECK(pre.d_node->getType() == invType) << "Expected inv and pre to have the same sort"; - CVC4_API_CHECK(post.d_expr->getType() == invType) + CVC4_API_CHECK(post.d_node->getType() == invType) << "Expected inv and post to have the same sort"; - const std::vector<Type>& invArgTypes = invType.getArgTypes(); + const std::vector<TypeNode>& invArgTypes = invType.getArgTypes(); - std::vector<Type> expectedTypes; - expectedTypes.reserve(2 * invType.getArity() + 1); + std::vector<TypeNode> expectedTypes; + expectedTypes.reserve(2 * invArgTypes.size() + 1); for (size_t i = 0, n = invArgTypes.size(); i < 2 * n; i += 2) { @@ -5201,13 +5689,13 @@ void Solver::addSygusInvConstraint(Term inv, } expectedTypes.push_back(invType.getRangeType()); - FunctionType expectedTransType = d_exprMgr->mkFunctionType(expectedTypes); + TypeNode expectedTransType = getNodeManager()->mkFunctionType(expectedTypes); - CVC4_API_CHECK(trans.d_expr->getType() == expectedTransType) + CVC4_API_CHECK(trans.d_node->getType() == expectedTransType) << "Expected trans's sort to be " << invType; d_smtEngine->assertSygusInvConstraint( - *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr); + *inv.d_node, *pre.d_node, *trans.d_node, *post.d_node); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5224,12 +5712,12 @@ Term Solver::getSynthSolution(Term term) const CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - std::map<CVC4::Expr, CVC4::Expr> map; + std::map<CVC4::Node, CVC4::Node> map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) - << "The solver is not in a state immediately preceeded by a " + << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; - std::map<CVC4::Expr, CVC4::Expr>::const_iterator it = map.find(*term.d_expr); + std::map<CVC4::Node, CVC4::Node>::const_iterator it = map.find(*term.d_node); CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term"; @@ -5253,9 +5741,9 @@ std::vector<Term> Solver::getSynthSolutions( << "non-null term"; } - std::map<CVC4::Expr, CVC4::Expr> map; + std::map<CVC4::Node, CVC4::Node> map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) - << "The solver is not in a state immediately preceeded by a " + << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; std::vector<Term> synthSolution; @@ -5263,8 +5751,8 @@ std::vector<Term> Solver::getSynthSolutions( for (size_t i = 0, n = terms.size(); i < n; ++i) { - std::map<CVC4::Expr, CVC4::Expr>::const_iterator it = - map.find(*terms[i].d_expr); + std::map<CVC4::Node, CVC4::Node>::const_iterator it = + map.find(*terms[i].d_node); CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for term at index " << i; @@ -5293,6 +5781,15 @@ ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); } * !!! This is only temporarily available until the parser is fully migrated to * the new API. !!! */ +NodeManager* Solver::getNodeManager(void) const +{ + return d_exprMgr->getNodeManager(); +} + +/** + * !!! This is only temporarily available until the parser is fully migrated to + * the new API. !!! + */ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } /** @@ -5315,22 +5812,42 @@ std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms) return exprs; } +std::vector<Node> termVectorToNodes(const std::vector<Term>& terms) +{ + std::vector<Node> res; + for (const Term& t : terms) + { + res.push_back(t.getNode()); + } + return res; +} + std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts) { std::vector<Type> types; for (size_t i = 0, ssize = sorts.size(); i < ssize; i++) { - types.push_back(sorts[i].getType()); + types.push_back(sorts[i].getTypeNode().toType()); } return types; } -std::set<Type> sortSetToTypes(const std::set<Sort>& sorts) +std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts) { - std::set<Type> types; + std::vector<TypeNode> typeNodes; + for (const Sort& sort : sorts) + { + typeNodes.push_back(sort.getTypeNode()); + } + return typeNodes; +} + +std::set<TypeNode> sortSetToTypeNodes(const std::set<Sort>& sorts) +{ + std::set<TypeNode> types; for (const Sort& s : sorts) { - types.insert(s.getType()); + types.insert(s.getTypeNode()); } return types; } @@ -5352,6 +5869,16 @@ std::vector<Sort> typeVectorToSorts(const Solver* slv, std::vector<Sort> sorts; for (size_t i = 0, tsize = types.size(); i < tsize; i++) { + sorts.push_back(Sort(slv, TypeNode::fromType(types[i]))); + } + return sorts; +} +std::vector<Sort> typeNodeVectorToSorts(const Solver* slv, + const std::vector<TypeNode>& types) +{ + std::vector<Sort> sorts; + for (size_t i = 0, tsize = types.size(); i < tsize; i++) + { sorts.push_back(Sort(slv, types[i])); } return sorts; |