X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fapi%2Fcpp%2Fcvc5.cpp;h=8f5fc6566f701a1a3d8e0ed0dfde012022eebfb1;hb=5a795677fd0e9663508664009a67abf6857b0ac9;hp=5e38096c830ca938afd12c3d88323ffe1f99b28b;hpb=f3a2e3814d0a3f32fe1e9e24de954bc2d9ff999e;p=cvc5.git diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 5e38096c8..8f5fc6566 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -27,7 +27,7 @@ * Our Integer implementation, e.g., is such a special case since we support * two different back end implementations (GMP, CLN). Be aware that they do * not fully agree on what is (in)valid input, which requires extra checks for - * consistent behavior (see Solver::mkRealFromStrHelper for an example). + * consistent behavior (see Solver::mkRealOrIntegerFromStrHelper for example). */ #include "api/cpp/cvc5.h" @@ -53,10 +53,11 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" #include "expr/sequence.h" #include "expr/type_node.h" -#include "expr/uninterpreted_constant.h" #include "options/base_options.h" +#include "options/expr_options.h" #include "options/main_options.h" #include "options/option_exception.h" #include "options/options.h" @@ -70,7 +71,6 @@ #include "theory/datatypes/tuple_project_op.h" #include "theory/logic_info.h" #include "theory/theory_model.h" -#include "util/abstract_value.h" #include "util/bitvector.h" #include "util/divisible.h" #include "util/floatingpoint.h" @@ -83,6 +83,7 @@ #include "util/statistics_stats.h" #include "util/statistics_value.h" #include "util/string.h" +#include "util/uninterpreted_sort_value.h" #include "util/utility.h" namespace cvc5 { @@ -109,8 +110,7 @@ const static std::unordered_map s_kinds{ {UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND}, {NULL_EXPR, cvc5::Kind::NULL_EXPR}, /* Builtin ------------------------------------------------------------- */ - {UNINTERPRETED_CONSTANT, cvc5::Kind::UNINTERPRETED_CONSTANT}, - {ABSTRACT_VALUE, cvc5::Kind::ABSTRACT_VALUE}, + {UNINTERPRETED_SORT_VALUE, cvc5::Kind::UNINTERPRETED_SORT_VALUE}, {EQUAL, cvc5::Kind::EQUAL}, {DISTINCT, cvc5::Kind::DISTINCT}, {CONSTANT, cvc5::Kind::VARIABLE}, @@ -126,20 +126,17 @@ const static std::unordered_map s_kinds{ {OR, cvc5::Kind::OR}, {XOR, cvc5::Kind::XOR}, {ITE, cvc5::Kind::ITE}, - {MATCH, cvc5::Kind::MATCH}, - {MATCH_CASE, cvc5::Kind::MATCH_CASE}, - {MATCH_BIND_CASE, cvc5::Kind::MATCH_BIND_CASE}, /* UF ------------------------------------------------------------------ */ {APPLY_UF, cvc5::Kind::APPLY_UF}, {CARDINALITY_CONSTRAINT, cvc5::Kind::CARDINALITY_CONSTRAINT}, {HO_APPLY, cvc5::Kind::HO_APPLY}, /* Arithmetic ---------------------------------------------------------- */ - {PLUS, cvc5::Kind::PLUS}, + {ADD, cvc5::Kind::ADD}, {MULT, cvc5::Kind::MULT}, {IAND, cvc5::Kind::IAND}, {POW2, cvc5::Kind::POW2}, - {MINUS, cvc5::Kind::MINUS}, - {UMINUS, cvc5::Kind::UMINUS}, + {SUB, cvc5::Kind::SUB}, + {NEG, cvc5::Kind::NEG}, {DIVISION, cvc5::Kind::DIVISION}, {INTS_DIVISION, cvc5::Kind::INTS_DIVISION}, {INTS_MODULUS, cvc5::Kind::INTS_MODULUS}, @@ -234,13 +231,13 @@ const static std::unordered_map s_kinds{ {FLOATINGPOINT_LT, cvc5::Kind::FLOATINGPOINT_LT}, {FLOATINGPOINT_GEQ, cvc5::Kind::FLOATINGPOINT_GEQ}, {FLOATINGPOINT_GT, cvc5::Kind::FLOATINGPOINT_GT}, - {FLOATINGPOINT_ISN, cvc5::Kind::FLOATINGPOINT_ISN}, - {FLOATINGPOINT_ISSN, cvc5::Kind::FLOATINGPOINT_ISSN}, - {FLOATINGPOINT_ISZ, cvc5::Kind::FLOATINGPOINT_ISZ}, - {FLOATINGPOINT_ISINF, cvc5::Kind::FLOATINGPOINT_ISINF}, - {FLOATINGPOINT_ISNAN, cvc5::Kind::FLOATINGPOINT_ISNAN}, - {FLOATINGPOINT_ISNEG, cvc5::Kind::FLOATINGPOINT_ISNEG}, - {FLOATINGPOINT_ISPOS, cvc5::Kind::FLOATINGPOINT_ISPOS}, + {FLOATINGPOINT_IS_NORMAL, cvc5::Kind::FLOATINGPOINT_IS_NORMAL}, + {FLOATINGPOINT_IS_SUBNORMAL, cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL}, + {FLOATINGPOINT_IS_ZERO, cvc5::Kind::FLOATINGPOINT_IS_ZERO}, + {FLOATINGPOINT_IS_INF, cvc5::Kind::FLOATINGPOINT_IS_INF}, + {FLOATINGPOINT_IS_NAN, cvc5::Kind::FLOATINGPOINT_IS_NAN}, + {FLOATINGPOINT_IS_NEG, cvc5::Kind::FLOATINGPOINT_IS_NEG}, + {FLOATINGPOINT_IS_POS, cvc5::Kind::FLOATINGPOINT_IS_POS}, {FLOATINGPOINT_TO_FP_FLOATINGPOINT, cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, @@ -265,6 +262,9 @@ const static std::unordered_map s_kinds{ {APPLY_TESTER, cvc5::Kind::APPLY_TESTER}, {APPLY_UPDATER, cvc5::Kind::APPLY_UPDATER}, {DT_SIZE, cvc5::Kind::DT_SIZE}, + {MATCH, cvc5::Kind::MATCH}, + {MATCH_CASE, cvc5::Kind::MATCH_CASE}, + {MATCH_BIND_CASE, cvc5::Kind::MATCH_BIND_CASE}, {TUPLE_PROJECT, cvc5::Kind::TUPLE_PROJECT}, /* Separation Logic ---------------------------------------------------- */ {SEP_NIL, cvc5::Kind::SEP_NIL}, @@ -273,43 +273,49 @@ const static std::unordered_map s_kinds{ {SEP_STAR, cvc5::Kind::SEP_STAR}, {SEP_WAND, cvc5::Kind::SEP_WAND}, /* Sets ---------------------------------------------------------------- */ - {EMPTYSET, cvc5::Kind::EMPTYSET}, - {UNION, cvc5::Kind::UNION}, - {INTERSECTION, cvc5::Kind::INTERSECTION}, - {SETMINUS, cvc5::Kind::SETMINUS}, - {SUBSET, cvc5::Kind::SUBSET}, - {MEMBER, cvc5::Kind::MEMBER}, - {SINGLETON, cvc5::Kind::SINGLETON}, - {INSERT, cvc5::Kind::INSERT}, - {CARD, cvc5::Kind::CARD}, - {COMPLEMENT, cvc5::Kind::COMPLEMENT}, - {UNIVERSE_SET, cvc5::Kind::UNIVERSE_SET}, - {JOIN, cvc5::Kind::JOIN}, - {PRODUCT, cvc5::Kind::PRODUCT}, - {TRANSPOSE, cvc5::Kind::TRANSPOSE}, - {TCLOSURE, cvc5::Kind::TCLOSURE}, - {JOIN_IMAGE, cvc5::Kind::JOIN_IMAGE}, - {IDEN, cvc5::Kind::IDEN}, - {COMPREHENSION, cvc5::Kind::COMPREHENSION}, - {CHOOSE, cvc5::Kind::CHOOSE}, - {IS_SINGLETON, cvc5::Kind::IS_SINGLETON}, + {SET_EMPTY, cvc5::Kind::SET_EMPTY}, + {SET_UNION, cvc5::Kind::SET_UNION}, + {SET_INTER, cvc5::Kind::SET_INTER}, + {SET_MINUS, cvc5::Kind::SET_MINUS}, + {SET_SUBSET, cvc5::Kind::SET_SUBSET}, + {SET_MEMBER, cvc5::Kind::SET_MEMBER}, + {SET_SINGLETON, cvc5::Kind::SET_SINGLETON}, + {SET_INSERT, cvc5::Kind::SET_INSERT}, + {SET_CARD, cvc5::Kind::SET_CARD}, + {SET_COMPLEMENT, cvc5::Kind::SET_COMPLEMENT}, + {SET_UNIVERSE, cvc5::Kind::SET_UNIVERSE}, + {SET_COMPREHENSION, cvc5::Kind::SET_COMPREHENSION}, + {SET_CHOOSE, cvc5::Kind::SET_CHOOSE}, + {SET_IS_SINGLETON, cvc5::Kind::SET_IS_SINGLETON}, + {SET_MAP, cvc5::Kind::SET_MAP}, + /* Relations ----------------------------------------------------------- */ + {RELATION_JOIN, cvc5::Kind::RELATION_JOIN}, + {RELATION_PRODUCT, cvc5::Kind::RELATION_PRODUCT}, + {RELATION_TRANSPOSE, cvc5::Kind::RELATION_TRANSPOSE}, + {RELATION_TCLOSURE, cvc5::Kind::RELATION_TCLOSURE}, + {RELATION_JOIN_IMAGE, cvc5::Kind::RELATION_JOIN_IMAGE}, + {RELATION_IDEN, cvc5::Kind::RELATION_IDEN}, /* Bags ---------------------------------------------------------------- */ - {UNION_MAX, cvc5::Kind::UNION_MAX}, - {UNION_DISJOINT, cvc5::Kind::UNION_DISJOINT}, - {INTERSECTION_MIN, cvc5::Kind::INTERSECTION_MIN}, - {DIFFERENCE_SUBTRACT, cvc5::Kind::DIFFERENCE_SUBTRACT}, - {DIFFERENCE_REMOVE, cvc5::Kind::DIFFERENCE_REMOVE}, - {SUBBAG, cvc5::Kind::SUBBAG}, + {BAG_UNION_MAX, cvc5::Kind::BAG_UNION_MAX}, + {BAG_UNION_DISJOINT, cvc5::Kind::BAG_UNION_DISJOINT}, + {BAG_INTER_MIN, cvc5::Kind::BAG_INTER_MIN}, + {BAG_DIFFERENCE_SUBTRACT, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT}, + {BAG_DIFFERENCE_REMOVE, cvc5::Kind::BAG_DIFFERENCE_REMOVE}, + {BAG_SUBBAG, cvc5::Kind::BAG_SUBBAG}, {BAG_COUNT, cvc5::Kind::BAG_COUNT}, - {DUPLICATE_REMOVAL, cvc5::Kind::DUPLICATE_REMOVAL}, - {MK_BAG, cvc5::Kind::MK_BAG}, - {EMPTYBAG, cvc5::Kind::EMPTYBAG}, + {BAG_MEMBER, cvc5::Kind::BAG_MEMBER}, + {BAG_DUPLICATE_REMOVAL, cvc5::Kind::BAG_DUPLICATE_REMOVAL}, + {BAG_MAKE, cvc5::Kind::BAG_MAKE}, + {BAG_EMPTY, cvc5::Kind::BAG_EMPTY}, {BAG_CARD, cvc5::Kind::BAG_CARD}, {BAG_CHOOSE, cvc5::Kind::BAG_CHOOSE}, {BAG_IS_SINGLETON, cvc5::Kind::BAG_IS_SINGLETON}, {BAG_FROM_SET, cvc5::Kind::BAG_FROM_SET}, {BAG_TO_SET, cvc5::Kind::BAG_TO_SET}, {BAG_MAP, cvc5::Kind::BAG_MAP}, + {BAG_FILTER, cvc5::Kind::BAG_FILTER}, + {BAG_FOLD, cvc5::Kind::BAG_FOLD}, + {TABLE_PRODUCT, cvc5::Kind::TABLE_PRODUCT}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, cvc5::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, cvc5::Kind::STRING_IN_REGEXP}, @@ -348,8 +354,9 @@ const static std::unordered_map s_kinds{ {REGEXP_RANGE, cvc5::Kind::REGEXP_RANGE}, {REGEXP_REPEAT, cvc5::Kind::REGEXP_REPEAT}, {REGEXP_LOOP, cvc5::Kind::REGEXP_LOOP}, - {REGEXP_EMPTY, cvc5::Kind::REGEXP_EMPTY}, - {REGEXP_SIGMA, cvc5::Kind::REGEXP_SIGMA}, + {REGEXP_NONE, cvc5::Kind::REGEXP_NONE}, + {REGEXP_ALL, cvc5::Kind::REGEXP_ALL}, + {REGEXP_ALLCHAR, cvc5::Kind::REGEXP_ALLCHAR}, {REGEXP_COMPLEMENT, cvc5::Kind::REGEXP_COMPLEMENT}, // maps to the same kind as the string versions {SEQ_CONCAT, cvc5::Kind::STRING_CONCAT}, @@ -370,7 +377,7 @@ const static std::unordered_map s_kinds{ /* Quantifiers --------------------------------------------------------- */ {FORALL, cvc5::Kind::FORALL}, {EXISTS, cvc5::Kind::EXISTS}, - {BOUND_VAR_LIST, cvc5::Kind::BOUND_VAR_LIST}, + {VARIABLE_LIST, cvc5::Kind::BOUND_VAR_LIST}, {INST_PATTERN, cvc5::Kind::INST_PATTERN}, {INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN}, {INST_POOL, cvc5::Kind::INST_POOL}, @@ -387,8 +394,7 @@ const static std::unordered_map {cvc5::Kind::UNDEFINED_KIND, UNDEFINED_KIND}, {cvc5::Kind::NULL_EXPR, NULL_EXPR}, /* Builtin --------------------------------------------------------- */ - {cvc5::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT}, - {cvc5::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE}, + {cvc5::Kind::UNINTERPRETED_SORT_VALUE, UNINTERPRETED_SORT_VALUE}, {cvc5::Kind::EQUAL, EQUAL}, {cvc5::Kind::DISTINCT, DISTINCT}, {cvc5::Kind::VARIABLE, CONSTANT}, @@ -404,20 +410,17 @@ const static std::unordered_map {cvc5::Kind::OR, OR}, {cvc5::Kind::XOR, XOR}, {cvc5::Kind::ITE, ITE}, - {cvc5::Kind::MATCH, MATCH}, - {cvc5::Kind::MATCH_CASE, MATCH_CASE}, - {cvc5::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE}, /* UF -------------------------------------------------------------- */ {cvc5::Kind::APPLY_UF, APPLY_UF}, {cvc5::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT}, {cvc5::Kind::HO_APPLY, HO_APPLY}, /* Arithmetic ------------------------------------------------------ */ - {cvc5::Kind::PLUS, PLUS}, + {cvc5::Kind::ADD, ADD}, {cvc5::Kind::MULT, MULT}, {cvc5::Kind::IAND, IAND}, {cvc5::Kind::POW2, POW2}, - {cvc5::Kind::MINUS, MINUS}, - {cvc5::Kind::UMINUS, UMINUS}, + {cvc5::Kind::SUB, SUB}, + {cvc5::Kind::NEG, NEG}, {cvc5::Kind::DIVISION, DIVISION}, {cvc5::Kind::DIVISION_TOTAL, INTERNAL_KIND}, {cvc5::Kind::INTS_DIVISION, INTS_DIVISION}, @@ -524,13 +527,13 @@ const static std::unordered_map {cvc5::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT}, {cvc5::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ}, {cvc5::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT}, - {cvc5::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN}, - {cvc5::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN}, - {cvc5::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ}, - {cvc5::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF}, - {cvc5::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN}, - {cvc5::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG}, - {cvc5::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS}, + {cvc5::Kind::FLOATINGPOINT_IS_NORMAL, FLOATINGPOINT_IS_NORMAL}, + {cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL, FLOATINGPOINT_IS_SUBNORMAL}, + {cvc5::Kind::FLOATINGPOINT_IS_ZERO, FLOATINGPOINT_IS_ZERO}, + {cvc5::Kind::FLOATINGPOINT_IS_INF, FLOATINGPOINT_IS_INF}, + {cvc5::Kind::FLOATINGPOINT_IS_NAN, FLOATINGPOINT_IS_NAN}, + {cvc5::Kind::FLOATINGPOINT_IS_NEG, FLOATINGPOINT_IS_NEG}, + {cvc5::Kind::FLOATINGPOINT_IS_POS, FLOATINGPOINT_IS_POS}, {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, @@ -569,10 +572,12 @@ const static std::unordered_map /* Datatypes ------------------------------------------------------- */ {cvc5::Kind::APPLY_SELECTOR, APPLY_SELECTOR}, {cvc5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, - {cvc5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND}, {cvc5::Kind::APPLY_TESTER, APPLY_TESTER}, {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER}, {cvc5::Kind::DT_SIZE, DT_SIZE}, + {cvc5::Kind::MATCH, MATCH}, + {cvc5::Kind::MATCH_CASE, MATCH_CASE}, + {cvc5::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE}, {cvc5::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, {cvc5::Kind::TUPLE_PROJECT_OP, TUPLE_PROJECT}, /* Separation Logic ------------------------------------------------ */ @@ -582,43 +587,49 @@ const static std::unordered_map {cvc5::Kind::SEP_STAR, SEP_STAR}, {cvc5::Kind::SEP_WAND, SEP_WAND}, /* Sets ------------------------------------------------------------ */ - {cvc5::Kind::EMPTYSET, EMPTYSET}, - {cvc5::Kind::UNION, UNION}, - {cvc5::Kind::INTERSECTION, INTERSECTION}, - {cvc5::Kind::SETMINUS, SETMINUS}, - {cvc5::Kind::SUBSET, SUBSET}, - {cvc5::Kind::MEMBER, MEMBER}, - {cvc5::Kind::SINGLETON, SINGLETON}, - {cvc5::Kind::INSERT, INSERT}, - {cvc5::Kind::CARD, CARD}, - {cvc5::Kind::COMPLEMENT, COMPLEMENT}, - {cvc5::Kind::UNIVERSE_SET, UNIVERSE_SET}, - {cvc5::Kind::JOIN, JOIN}, - {cvc5::Kind::PRODUCT, PRODUCT}, - {cvc5::Kind::TRANSPOSE, TRANSPOSE}, - {cvc5::Kind::TCLOSURE, TCLOSURE}, - {cvc5::Kind::JOIN_IMAGE, JOIN_IMAGE}, - {cvc5::Kind::IDEN, IDEN}, - {cvc5::Kind::COMPREHENSION, COMPREHENSION}, - {cvc5::Kind::CHOOSE, CHOOSE}, - {cvc5::Kind::IS_SINGLETON, IS_SINGLETON}, + {cvc5::Kind::SET_EMPTY, SET_EMPTY}, + {cvc5::Kind::SET_UNION, SET_UNION}, + {cvc5::Kind::SET_INTER, SET_INTER}, + {cvc5::Kind::SET_MINUS, SET_MINUS}, + {cvc5::Kind::SET_SUBSET, SET_SUBSET}, + {cvc5::Kind::SET_MEMBER, SET_MEMBER}, + {cvc5::Kind::SET_SINGLETON, SET_SINGLETON}, + {cvc5::Kind::SET_INSERT, SET_INSERT}, + {cvc5::Kind::SET_CARD, SET_CARD}, + {cvc5::Kind::SET_COMPLEMENT, SET_COMPLEMENT}, + {cvc5::Kind::SET_UNIVERSE, SET_UNIVERSE}, + {cvc5::Kind::SET_COMPREHENSION, SET_COMPREHENSION}, + {cvc5::Kind::SET_CHOOSE, SET_CHOOSE}, + {cvc5::Kind::SET_IS_SINGLETON, SET_IS_SINGLETON}, + {cvc5::Kind::SET_MAP, SET_MAP}, + /* Relations ------------------------------------------------------- */ + {cvc5::Kind::RELATION_JOIN, RELATION_JOIN}, + {cvc5::Kind::RELATION_PRODUCT, RELATION_PRODUCT}, + {cvc5::Kind::RELATION_TRANSPOSE, RELATION_TRANSPOSE}, + {cvc5::Kind::RELATION_TCLOSURE, RELATION_TCLOSURE}, + {cvc5::Kind::RELATION_JOIN_IMAGE, RELATION_JOIN_IMAGE}, + {cvc5::Kind::RELATION_IDEN, RELATION_IDEN}, /* Bags ------------------------------------------------------------ */ - {cvc5::Kind::UNION_MAX, UNION_MAX}, - {cvc5::Kind::UNION_DISJOINT, UNION_DISJOINT}, - {cvc5::Kind::INTERSECTION_MIN, INTERSECTION_MIN}, - {cvc5::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT}, - {cvc5::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE}, - {cvc5::Kind::SUBBAG, SUBBAG}, + {cvc5::Kind::BAG_UNION_MAX, BAG_UNION_MAX}, + {cvc5::Kind::BAG_UNION_DISJOINT, BAG_UNION_DISJOINT}, + {cvc5::Kind::BAG_INTER_MIN, BAG_INTER_MIN}, + {cvc5::Kind::BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_SUBTRACT}, + {cvc5::Kind::BAG_DIFFERENCE_REMOVE, BAG_DIFFERENCE_REMOVE}, + {cvc5::Kind::BAG_SUBBAG, BAG_SUBBAG}, {cvc5::Kind::BAG_COUNT, BAG_COUNT}, - {cvc5::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL}, - {cvc5::Kind::MK_BAG, MK_BAG}, - {cvc5::Kind::EMPTYBAG, EMPTYBAG}, + {cvc5::Kind::BAG_MEMBER, BAG_MEMBER}, + {cvc5::Kind::BAG_DUPLICATE_REMOVAL, BAG_DUPLICATE_REMOVAL}, + {cvc5::Kind::BAG_MAKE, BAG_MAKE}, + {cvc5::Kind::BAG_EMPTY, BAG_EMPTY}, {cvc5::Kind::BAG_CARD, BAG_CARD}, {cvc5::Kind::BAG_CHOOSE, BAG_CHOOSE}, {cvc5::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, {cvc5::Kind::BAG_FROM_SET, BAG_FROM_SET}, {cvc5::Kind::BAG_TO_SET, BAG_TO_SET}, - {cvc5::Kind::BAG_MAP,BAG_MAP}, + {cvc5::Kind::BAG_MAP, BAG_MAP}, + {cvc5::Kind::BAG_FILTER, BAG_FILTER}, + {cvc5::Kind::BAG_FOLD, BAG_FOLD}, + {cvc5::Kind::TABLE_PRODUCT, TABLE_PRODUCT}, /* Strings --------------------------------------------------------- */ {cvc5::Kind::STRING_CONCAT, STRING_CONCAT}, {cvc5::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, @@ -659,8 +670,9 @@ const static std::unordered_map {cvc5::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT}, {cvc5::Kind::REGEXP_LOOP, REGEXP_LOOP}, {cvc5::Kind::REGEXP_LOOP_OP, REGEXP_LOOP}, - {cvc5::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, - {cvc5::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, + {cvc5::Kind::REGEXP_NONE, REGEXP_NONE}, + {cvc5::Kind::REGEXP_ALL, REGEXP_ALL}, + {cvc5::Kind::REGEXP_ALLCHAR, REGEXP_ALLCHAR}, {cvc5::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, {cvc5::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, {cvc5::Kind::SEQ_UNIT, SEQ_UNIT}, @@ -668,7 +680,7 @@ const static std::unordered_map /* Quantifiers ----------------------------------------------------- */ {cvc5::Kind::FORALL, FORALL}, {cvc5::Kind::EXISTS, EXISTS}, - {cvc5::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST}, + {cvc5::Kind::BOUND_VAR_LIST, VARIABLE_LIST}, {cvc5::Kind::INST_PATTERN, INST_PATTERN}, {cvc5::Kind::INST_NO_PATTERN, INST_NO_PATTERN}, {cvc5::Kind::INST_POOL, INST_POOL}, @@ -855,6 +867,27 @@ class CVC5ApiRecoverableExceptionStream std::stringstream d_stream; }; +class CVC5ApiUnsupportedExceptionStream +{ + public: + CVC5ApiUnsupportedExceptionStream() {} + /* 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). */ + ~CVC5ApiUnsupportedExceptionStream() noexcept(false) + { + if (std::uncaught_exceptions() == 0) + { + throw CVC5ApiUnsupportedException(d_stream.str()); + } + } + + std::ostream& ostream() { return d_stream; } + + private: + std::stringstream d_stream; +}; + #define CVC5_API_TRY_CATCH_BEGIN \ try \ { @@ -1083,6 +1116,29 @@ bool Sort::operator>=(const Sort& s) const CVC5_API_TRY_CATCH_END; } +bool Sort::hasSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_type->hasAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + +std::string Sort::getSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(d_type->hasAttribute(expr::VarNameAttr())) + << "Invalid call to '" << __PRETTY_FUNCTION__ + << "', expected the sort to have a symbol."; + //////// all checks before this line + return d_type->getAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Sort::isNull() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1338,16 +1394,6 @@ bool Sort::isSubsortOf(const Sort& s) const CVC5_API_TRY_CATCH_END; } -bool Sort::isComparableTo(const Sort& s) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_ARG_CHECK_SOLVER("sort", s); - //////// all checks before this line - return d_type->isComparableTo(*s.d_type); - //////// - CVC5_API_TRY_CATCH_END; -} - Datatype Sort::getDatatype() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1366,6 +1412,9 @@ Sort Sort::instantiate(const std::vector& params) const CVC5_API_CHECK_SORTS(params); CVC5_API_CHECK(isParametricDatatype() || isSortConstructor()) << "Expected parametric datatype or sort constructor sort."; + CVC5_API_CHECK(isSortConstructor() + || d_type->getNumChildren() == params.size() + 1) + << "Arity mismatch for instantiated parametric datatype"; //////// all checks before this line std::vector tparams = sortVectorToTypeNodes(params); if (d_type->isDatatype()) @@ -1417,10 +1466,6 @@ std::string Sort::toString() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - if (d_solver != nullptr) - { - return d_type->toString(); - } return d_type->toString(); //////// CVC5_API_TRY_CATCH_END; @@ -1735,7 +1780,7 @@ size_t Sort::getDatatypeArity() const CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK(isDatatype()) << "Not a datatype sort."; //////// all checks before this line - return d_type->getNumChildren() - 1; + return d_type->isParametricDatatype() ? d_type->getNumChildren() - 1 : 0; //////// CVC5_API_TRY_CATCH_END; } @@ -1924,75 +1969,74 @@ Term Op::getIndexHelper(size_t index) const { case DIVISIBLE: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( Rational(d_node->getConst().k)); break; } case BITVECTOR_REPEAT: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_repeatAmount); break; } case BITVECTOR_ZERO_EXTEND: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_zeroExtendAmount); break; } case BITVECTOR_SIGN_EXTEND: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_signExtendAmount); break; } case BITVECTOR_ROTATE_LEFT: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_rotateLeftAmount); break; } case BITVECTOR_ROTATE_RIGHT: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_rotateRightAmount); break; } case INT_TO_BITVECTOR: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_size); break; } case IAND: { - t = d_solver->mkValHelper( - d_node->getConst().d_size); + t = d_solver->mkRationalValHelper(d_node->getConst().d_size); break; } case FLOATINGPOINT_TO_UBV: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_bv_size.d_size); break; } case FLOATINGPOINT_TO_SBV: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_bv_size.d_size); break; } case REGEXP_REPEAT: { - t = d_solver->mkValHelper( + t = d_solver->mkRationalValHelper( d_node->getConst().d_repeatAmount); break; } case BITVECTOR_EXTRACT: { cvc5::BitVectorExtract ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper(ext.d_high) - : d_solver->mkValHelper(ext.d_low); + t = index == 0 ? d_solver->mkRationalValHelper(ext.d_high) + : d_solver->mkRationalValHelper(ext.d_low); break; } case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: @@ -2000,20 +2044,18 @@ Term Op::getIndexHelper(size_t index) const cvc5::FloatingPointToFPIEEEBitVector ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper( - ext.getSize().exponentWidth()) - : d_solver->mkValHelper( - ext.getSize().significandWidth()); + t = index == 0 + ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) + : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } case FLOATINGPOINT_TO_FP_FLOATINGPOINT: { cvc5::FloatingPointToFPFloatingPoint ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper( - ext.getSize().exponentWidth()) - : d_solver->mkValHelper( - ext.getSize().significandWidth()); + t = index == 0 + ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) + : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } case FLOATINGPOINT_TO_FP_REAL: @@ -2021,47 +2063,43 @@ Term Op::getIndexHelper(size_t index) const cvc5::FloatingPointToFPReal ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper( - ext.getSize().exponentWidth()) - : d_solver->mkValHelper( - ext.getSize().significandWidth()); + t = index == 0 + ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) + : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: { cvc5::FloatingPointToFPSignedBitVector ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper( - ext.getSize().exponentWidth()) - : d_solver->mkValHelper( - ext.getSize().significandWidth()); + t = index == 0 + ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) + : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: { cvc5::FloatingPointToFPUnsignedBitVector ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper( - ext.getSize().exponentWidth()) - : d_solver->mkValHelper( - ext.getSize().significandWidth()); + t = index == 0 + ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) + : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } case FLOATINGPOINT_TO_FP_GENERIC: { cvc5::FloatingPointToFPGeneric ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper( - ext.getSize().exponentWidth()) - : d_solver->mkValHelper( - ext.getSize().significandWidth()); + t = index == 0 + ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) + : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } case REGEXP_LOOP: { cvc5::RegExpLoop ext = d_node->getConst(); - t = index == 0 ? d_solver->mkValHelper(ext.d_loopMinOcc) - : d_solver->mkValHelper(ext.d_loopMaxOcc); + t = index == 0 ? d_solver->mkRationalValHelper(ext.d_loopMinOcc) + : d_solver->mkRationalValHelper(ext.d_loopMaxOcc); break; } @@ -2070,7 +2108,7 @@ Term Op::getIndexHelper(size_t index) const { const std::vector& projectionIndices = d_node->getConst().getIndices(); - t = d_solver->mkValHelper(projectionIndices[index]); + t = d_solver->mkRationalValHelper(projectionIndices[index]); break; } default: @@ -2441,8 +2479,8 @@ Term Term::substitute(const Term& term, const Term& replacement) const CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_TERM(term); CVC5_API_CHECK_TERM(replacement); - CVC5_API_CHECK(term.getSort().isComparableTo(replacement.getSort())) - << "Expecting terms of comparable sort in substitute"; + CVC5_API_CHECK(term.getSort() == replacement.getSort()) + << "Expecting terms of the same sort in substitute"; //////// all checks before this line return Term( d_solver, @@ -2458,7 +2496,7 @@ Term Term::substitute(const std::vector& terms, CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK(terms.size() == replacements.size()) << "Expecting vectors of the same arity in substitute"; - CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms, replacements); + CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_SORT_EQUAL_TO(terms, replacements); //////// all checks before this line std::vector nodes = Term::termVectorToNodes(terms); std::vector nodeReplacements = Term::termVectorToNodes(replacements); @@ -2512,6 +2550,29 @@ Op Term::getOp() const CVC5_API_TRY_CATCH_END; } +bool Term::hasSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->hasAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + +std::string Term::getSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(d_node->hasAttribute(expr::VarNameAttr())) + << "Invalid call to '" << __PRETTY_FUNCTION__ + << "', expected the term to have a symbol."; + //////// all checks before this line + return d_node->getAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Term::isNull() const { CVC5_API_TRY_CATCH_BEGIN; @@ -2616,10 +2677,6 @@ std::string Term::toString() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - if (d_solver != nullptr) - { - return d_node->toString(); - } return d_node->toString(); //////// CVC5_API_TRY_CATCH_END; @@ -2804,6 +2861,17 @@ bool isUInt64(const Node& node) } } // namespace detail +int32_t Term::getRealOrIntegerValueSign() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + const Rational& r = detail::getRational(*d_node); + return static_cast(r.sgn()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Term::isInt32Value() const { CVC5_API_TRY_CATCH_BEGIN; @@ -2864,7 +2932,7 @@ std::int64_t Term::getInt64Value() const CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node), *d_node) << "Term to be a 64-bit integer value when calling getInt64Value()"; //////// all checks before this line - return detail::getInteger(*d_node).getLong(); + return detail::getInteger(*d_node).getSigned64(); //////// CVC5_API_TRY_CATCH_END; } @@ -2887,7 +2955,7 @@ std::uint64_t Term::getUInt64Value() const << "Term to be a unsigned 64-bit integer value when calling " "getUInt64Value()"; //////// all checks before this line - return detail::getInteger(*d_node).getUnsignedLong(); + return detail::getInteger(*d_node).getUnsigned64(); //////// CVC5_API_TRY_CATCH_END; } @@ -2946,6 +3014,17 @@ std::vector Term::termVectorToNodes(const std::vector& terms) return res; } +std::vector Term::nodeVectorToTerms(const Solver* slv, + const std::vector& nodes) +{ + std::vector res; + for (const Node& n : nodes) + { + res.push_back(Term(slv, n)); + } + return res; +} + bool Term::isReal32Value() const { CVC5_API_TRY_CATCH_BEGIN; @@ -2985,8 +3064,8 @@ std::pair Term::getReal64Value() const << "Term to be a 64-bit rational value when calling getReal64Value()"; //////// all checks before this line const Rational& r = detail::getRational(*d_node); - return std::make_pair(r.getNumerator().getLong(), - r.getDenominator().getUnsignedLong()); + return std::make_pair(r.getNumerator().getSigned64(), + r.getDenominator().getUnsigned64()); //////// CVC5_API_TRY_CATCH_END; } @@ -3084,25 +3163,27 @@ std::string Term::getBitVectorValue(std::uint32_t base) const CVC5_API_TRY_CATCH_END; } -bool Term::isAbstractValue() const +bool Term::isUninterpretedSortValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; //////// all checks before this line - return d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE; + return d_node->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE; //////// CVC5_API_TRY_CATCH_END; } -std::string Term::getAbstractValue() const +std::string Term::getUninterpretedSortValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE, - *d_node) + CVC5_API_ARG_CHECK_EXPECTED( + d_node->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE, *d_node) << "Term to be an abstract value when calling " - "getAbstractValue()"; + "getUninterpretedSortValue()"; //////// all checks before this line - return d_node->getConst().getIndex().toString(); + std::stringstream ss; + ss << d_node->getConst(); + return ss.str(); //////// CVC5_API_TRY_CATCH_END; } @@ -3245,12 +3326,12 @@ void Term::collectSet(std::set& set, const Solver* slv) { // We asserted that node has a set type, and node.isConst() - // Thus, node only contains of EMPTYSET, UNION and SINGLETON. + // Thus, node only contains of SET_EMPTY, SET_UNION and SET_SINGLETON. switch (node.getKind()) { - case cvc5::Kind::EMPTYSET: break; - case cvc5::Kind::SINGLETON: set.emplace(Term(slv, node[0])); break; - case cvc5::Kind::UNION: + case cvc5::Kind::SET_EMPTY: break; + case cvc5::Kind::SET_SINGLETON: set.emplace(Term(slv, node[0])); break; + case cvc5::Kind::SET_UNION: { for (const auto& sub : node) { @@ -3308,31 +3389,6 @@ std::vector Term::getSequenceValue() const CVC5_API_TRY_CATCH_END; } -bool Term::isUninterpretedValue() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - //////// all checks before this line - return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT; - //////// - CVC5_API_TRY_CATCH_END; -} -std::pair Term::getUninterpretedValue() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_ARG_CHECK_EXPECTED( - d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node) - << "Term to be an uninterpreted value when calling " - "getUninterpretedValue()"; - //////// all checks before this line - const auto& uc = d_node->getConst(); - return std::make_pair(Sort(d_solver, uc.getType()), - uc.getIndex().toUnsignedInt()); - //////// - CVC5_API_TRY_CATCH_END; -} - std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); @@ -3461,7 +3517,7 @@ void DatatypeConstructorDecl::addSelector(const std::string& name, CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_SORT(sort); CVC5_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) - << "non-null range sort for selector"; + << "non-null codomain sort for selector"; //////// all checks before this line d_ctor->addArg(name, *sort.d_type); //////// @@ -3514,6 +3570,11 @@ std::ostream& operator<<(std::ostream& out, bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor == nullptr; } +bool DatatypeConstructorDecl::isResolved() const +{ + return d_ctor == nullptr || d_ctor->isResolved(); +} + /* DatatypeDecl ------------------------------------------------------------- */ DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {} @@ -3675,7 +3736,7 @@ Term DatatypeSelector::getUpdaterTerm() const CVC5_API_TRY_CATCH_END; } -Sort DatatypeSelector::getRangeSort() const +Sort DatatypeSelector::getCodomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -3755,7 +3816,7 @@ Term DatatypeConstructor::getConstructorTerm() const CVC5_API_TRY_CATCH_END; } -Term DatatypeConstructor::getSpecializedConstructorTerm( +Term DatatypeConstructor::getInstantiatedConstructorTerm( const Sort& retSort) const { CVC5_API_TRY_CATCH_BEGIN; @@ -3766,13 +3827,7 @@ Term DatatypeConstructor::getSpecializedConstructorTerm( << "Cannot get specialized constructor type for non-datatype type " << retSort; //////// all checks before this line - - 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()); + Node ret = d_ctor->getInstantiatedConstructor(*retSort.d_type); (void)ret.getType(true); /* kick off type checking */ // apply type ascription to the operator Term sctor = api::Term(d_solver, ret); @@ -4066,6 +4121,18 @@ size_t Datatype::getNumConstructors() const CVC5_API_TRY_CATCH_END; } +std::vector Datatype::getParameters() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(isParametric()) << "Expected parametric datatype"; + //////// all checks before this line + std::vector params = d_dtype->getParameters(); + return Sort::typeNodeVectorToSorts(d_solver, params); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Datatype::isParametric() const { CVC5_API_TRY_CATCH_BEGIN; @@ -4110,6 +4177,8 @@ bool Datatype::isFinite() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(!d_dtype->isParametric()) + << "Invalid call to 'isFinite()', expected non-parametric Datatype"; //////// all checks before this line // we assume that finite model finding is disabled by passing false as the // second argument @@ -4127,15 +4196,6 @@ bool Datatype::isWellFounded() const //////// CVC5_API_TRY_CATCH_END; } -bool Datatype::hasNestedRecursion() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - //////// all checks before this line - return d_dtype->hasNestedRecursion(); - //////// - CVC5_API_TRY_CATCH_END; -} bool Datatype::isNull() const { @@ -4671,6 +4731,7 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, bool Grammar::containsFreeVariables(const Term& rule) const { + // we allow the argument list and non-terminal symbols to be in scope std::unordered_set scope; for (const Term& sygusVar : d_sygusVars) @@ -4683,8 +4744,7 @@ bool Grammar::containsFreeVariables(const Term& rule) const scope.emplace(*ntsymbol.d_node); } - std::unordered_set fvs; - return expr::getFreeVariablesScope(*rule.d_node, fvs, scope, false); + return expr::hasFreeVariablesScope(*rule.d_node, scope); } std::ostream& operator<<(std::ostream& out, const Grammar& grammar) @@ -4962,7 +5022,7 @@ NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr; } void Solver::increment_term_stats(Kind kind) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_stats->d_terms << kind; } @@ -4970,7 +5030,7 @@ void Solver::increment_term_stats(Kind kind) const void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { const TypeNode tn = sort.getTypeNode(); TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT @@ -4991,7 +5051,7 @@ void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const /* .......................................................................... */ template -Term Solver::mkValHelper(T t) const +Term Solver::mkValHelper(const T& t) const { //////// all checks before this line Node res = getNodeManager()->mkConst(t); @@ -4999,7 +5059,23 @@ Term Solver::mkValHelper(T t) const return Term(this, res); } -Term Solver::mkRealFromStrHelper(const std::string& s) const +Term Solver::mkRationalValHelper(const Rational& r, bool isInt) const +{ + //////// all checks before this line + NodeManager* nm = getNodeManager(); + Node res = isInt ? nm->mkConstInt(r) : nm->mkConstReal(r); + (void)res.getType(true); /* kick off type checking */ + api::Term t = Term(this, res); + // NOTE: this block will be eliminated when arithmetic subtyping is eliminated + if (!isInt) + { + t = ensureRealSort(t); + } + return t; +} + +Term Solver::mkRealOrIntegerFromStrHelper(const std::string& s, + bool isInt) const { //////// all checks before this line try @@ -5007,7 +5083,7 @@ Term Solver::mkRealFromStrHelper(const std::string& s) const cvc5::Rational r = s.find('/') != std::string::npos ? cvc5::Rational(s) : cvc5::Rational::fromDecimal(s); - return mkValHelper(r); + return mkRationalValHelper(r, isInt); } catch (const std::invalid_argument& e) { @@ -5031,6 +5107,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base) const { + CVC5_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; CVC5_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC5_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; @@ -5040,7 +5117,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, if (val.strictlyNegative()) { - CVC5_API_CHECK(val >= -Integer("2", 10).pow(size - 1)) + CVC5_API_CHECK(val >= -Integer(2).pow(size - 1)) << "Overflow in bitvector construction (specified bitvector size " << size << " too small to hold value " << s << ")"; } @@ -5056,6 +5133,12 @@ Term Solver::mkBVFromStrHelper(uint32_t size, Term Solver::getValueHelper(const Term& term) const { // Note: Term is checked in the caller to avoid double checks + bool wasShadow = false; + bool freeOrShadowedVar = + expr::hasFreeOrShadowedVar(term.getNode(), wasShadow); + CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar) + << "Cannot get value of term containing " + << (wasShadow ? "shadowed" : "free") << " variables"; //////// all checks before this line Node value = d_slv->getValue(*term.d_node); Term res = Term(this, value); @@ -5078,14 +5161,15 @@ Sort Solver::mkTupleSortHelper(const std::vector& sorts) const Term Solver::mkTermFromKind(Kind kind) const { - CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY - || kind == REGEXP_SIGMA || kind == SEP_EMP, + CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_NONE + || kind == REGEXP_ALL + || kind == REGEXP_ALLCHAR || kind == SEP_EMP, kind) - << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP"; + << "PI, REGEXP_NONE, REGEXP_ALL, REGEXP_ALLCHAR or SEP_EMP"; //////// all checks before this line Node res; cvc5::Kind k = extToIntKind(kind); - if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) + if (kind == REGEXP_NONE || kind == REGEXP_ALL || kind == REGEXP_ALLCHAR) { Assert(isDefinedIntKind(k)); res = d_nodeMgr->mkNode(k, std::vector()); @@ -5108,14 +5192,17 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const { // Note: Kind and children are checked in the caller to avoid double checks //////// all checks before this line - + if (children.size() == 0) + { + return mkTermFromKind(kind); + } std::vector echildren = Term::termVectorToNodes(children); cvc5::Kind k = extToIntKind(kind); Node res; if (echildren.size() > 2) { - if (kind == INTS_DIVISION || kind == XOR || kind == MINUS - || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF) + if (kind == INTS_DIVISION || kind == XOR || kind == SUB || kind == DIVISION + || kind == HO_APPLY || kind == REGEXP_DIFF) { // left-associative, but cvc5 internally only supports 2 args res = d_nodeMgr->mkLeftAssociative(k, echildren); @@ -5147,13 +5234,14 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const else if (kind::isAssociative(k)) { // associative case, same as above + checkMkTerm(kind, children.size()); res = d_nodeMgr->mkAssociative(k, echildren); } else { // default case, same as above checkMkTerm(kind, children.size()); - if (kind == api::SINGLETON) + if (kind == api::SET_SINGLETON) { // the type of the term is the same as the type of the internal node // see Term::getSort() @@ -5165,7 +5253,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const // element type can be used safely here. res = getNodeManager()->mkSingleton(type, *children[0].d_node); } - else if (kind == api::MK_BAG) + else if (kind == api::BAG_MAKE) { // the type of the term is the same as the type of the internal node // see Term::getSort() @@ -5178,6 +5266,13 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const res = getNodeManager()->mkBag( type, *children[0].d_node, *children[1].d_node); } + else if (kind == api::SEQ_UNIT) + { + // 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(); + res = getNodeManager()->mkSeqUnit(type, *children[0].d_node); + } else { res = d_nodeMgr->mkNode(k, echildren); @@ -5191,15 +5286,15 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const Term Solver::mkTermHelper(const Op& op, const std::vector& children) const { - // Note: Op and children are checked in the caller to avoid double checks - checkMkTerm(op.d_kind, children.size()); - //////// all checks before this line - if (!op.isIndexedHelper()) { return mkTermHelper(op.d_kind, children); } + // Note: Op and children are checked in the caller to avoid double checks + checkMkTerm(op.d_kind, children.size()); + //////// all checks before this line + const cvc5::Kind int_kind = extToIntKind(op.d_kind); std::vector echildren = Term::termVectorToNodes(children); @@ -5299,7 +5394,8 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const res = Term(this, d_nodeMgr->mkNode(extToIntKind(DIVISION), *res.d_node, - d_nodeMgr->mkConst(cvc5::Rational(1)))); + d_nodeMgr->mkConst(kind::CONST_RATIONAL, + cvc5::Rational(1)))); } Assert(res.getSort() == sort); return res; @@ -5360,9 +5456,37 @@ bool Solver::isValidInteger(const std::string& s) const return true; } +void Solver::ensureWellFormedTerm(const Term& t) const +{ + // only check if option is set + if (d_slv->getOptions().expr.wellFormedChecking) + { + bool wasShadow = false; + if (expr::hasFreeOrShadowedVar(*t.d_node, wasShadow)) + { + std::stringstream se; + se << "Cannot process term with " << (wasShadow ? "shadowed" : "free") + << " variable"; + throw CVC5ApiException(se.str().c_str()); + } + } +} + +void Solver::ensureWellFormedTerms(const std::vector& ts) const +{ + // only check if option is set + if (d_slv->getOptions().expr.wellFormedChecking) + { + for (const Term& t : ts) + { + ensureWellFormedTerm(t); + } + } +} + void Solver::resetStatistics() { - if constexpr (Configuration::isStatisticsBuild()) + if constexpr (configuration::isStatisticsBuild()) { d_stats.reset(new APIStatistics{ d_slv->getStatisticsRegistry().registerHistogram( @@ -5649,6 +5773,19 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const CVC5_API_TRY_CATCH_END; } +Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + if (arity) + { + return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity)); + } + return Sort(this, getNodeManager()->mkSort(symbol)); + //////// + CVC5_API_TRY_CATCH_END; +} + Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { @@ -5716,7 +5853,7 @@ Term Solver::mkInteger(const std::string& s) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s), s) << " an integer "; - Term integer = mkRealFromStrHelper(s); + Term integer = mkRealOrIntegerFromStrHelper(s); CVC5_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s) << " a string representing an integer"; //////// all checks before this line @@ -5729,7 +5866,7 @@ Term Solver::mkInteger(int64_t val) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - Term integer = mkValHelper(cvc5::Rational(val)); + Term integer = mkRationalValHelper(cvc5::Rational(val)); Assert(integer.getSort() == getIntegerSort()); return integer; //////// @@ -5745,8 +5882,7 @@ Term Solver::mkReal(const std::string& s) const CVC5_API_ARG_CHECK_EXPECTED(s != ".", s) << "a string representing a real or rational value."; //////// all checks before this line - Term rational = mkRealFromStrHelper(s); - return ensureRealSort(rational); + return mkRealOrIntegerFromStrHelper(s, false); //////// CVC5_API_TRY_CATCH_END; } @@ -5755,8 +5891,7 @@ Term Solver::mkReal(int64_t val) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - Term rational = mkValHelper(cvc5::Rational(val)); - return ensureRealSort(rational); + return mkRationalValHelper(cvc5::Rational(val), false); //////// CVC5_API_TRY_CATCH_END; } @@ -5765,30 +5900,41 @@ Term Solver::mkReal(int64_t num, int64_t den) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - Term rational = mkValHelper(cvc5::Rational(num, den)); - return ensureRealSort(rational); + return mkRationalValHelper(cvc5::Rational(num, den), false); //////// CVC5_API_TRY_CATCH_END; } -Term Solver::mkRegexpEmpty() const +Term Solver::mkRegexpAll() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNode(cvc5::kind::REGEXP_EMPTY, std::vector()); + d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALL, std::vector()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// CVC5_API_TRY_CATCH_END; } -Term Solver::mkRegexpSigma() const +Term Solver::mkRegexpNone() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNode(cvc5::kind::REGEXP_SIGMA, std::vector()); + d_nodeMgr->mkNode(cvc5::kind::REGEXP_NONE, std::vector()); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + //////// + CVC5_API_TRY_CATCH_END; +} + +Term Solver::mkRegexpAllchar() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + Node res = + d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// @@ -5883,7 +6029,7 @@ Term Solver::mkUniverseSet(const Sort& sort) const //////// all checks before this line Node res = getNodeManager()->mkNullaryOperator(*sort.d_type, - cvc5::kind::UNIVERSE_SET); + cvc5::kind::SET_UNIVERSE); // TODO(#2771): Reenable? // (void)res->getType(true); /* kick off type checking */ return Term(this, res); @@ -5935,7 +6081,7 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const +Term Solver::mkFloatingPointPosInf(uint32_t exp, uint32_t sig) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -5945,7 +6091,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const +Term Solver::mkFloatingPointNegInf(uint32_t exp, uint32_t sig) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -5955,7 +6101,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkNaN(uint32_t exp, uint32_t sig) const +Term Solver::mkFloatingPointNaN(uint32_t exp, uint32_t sig) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -5965,7 +6111,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const +Term Solver::mkFloatingPointPosZero(uint32_t exp, uint32_t sig) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -5975,7 +6121,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const +Term Solver::mkFloatingPointNegZero(uint32_t exp, uint32_t sig) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -5994,46 +6140,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_SORT(sort); - //////// all checks before this line - return mkValHelper( - cvc5::UninterpretedConstant(*sort.d_type, index)); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkAbstractValue(const std::string& index) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; - - cvc5::Integer idx(index, 10); - CVC5_API_ARG_CHECK_EXPECTED(idx > 0, index) - << "a string representing an integer > 0"; - //////// all checks before this line - return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx))); - // do not call getType(), for abstract values, type can not be computed - // until it is substituted away - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkAbstractValue(uint64_t index) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; - //////// all checks before this line - return Term(this, - getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index)))); - // do not call getType(), for abstract values, type can not be computed - // until it is substituted away - //////// - CVC5_API_TRY_CATCH_END; -} - Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { CVC5_API_TRY_CATCH_BEGIN; @@ -6233,14 +6339,12 @@ Term Solver::mkTerm(const Op& op) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_OP(op); - checkMkTerm(op.d_kind, 0); - //////// all checks before this line - if (!op.isIndexedHelper()) { return mkTermFromKind(op.d_kind); } - + checkMkTerm(op.d_kind, 0); + //////// all checks before this line const cvc5::Kind int_kind = extToIntKind(op.d_kind); Term res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node)); @@ -6575,6 +6679,7 @@ Result Solver::checkEntailed(const Term& term) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); + ensureWellFormedTerm(term); //////// all checks before this line return d_slv->checkEntailed(*term.d_node); //////// @@ -6589,6 +6694,7 @@ Result Solver::checkEntailed(const std::vector& terms) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); + ensureWellFormedTerms(terms); //////// all checks before this line return d_slv->checkEntailed(Term::termVectorToNodes(terms)); //////// @@ -6603,6 +6709,7 @@ void Solver::assertFormula(const Term& term) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, getBooleanSort()); + ensureWellFormedTerm(term); //////// all checks before this line d_slv->assertFormula(*term.d_node); //////// @@ -6630,6 +6737,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); + ensureWellFormedTerm(assumption); //////// all checks before this line return d_slv->checkSat(*assumption.d_node); //////// @@ -6644,6 +6752,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); + ensureWellFormedTerms(assumptions); //////// all checks before this line for (const Term& term : assumptions) { @@ -6663,6 +6772,11 @@ Sort Solver::declareDatatype( CVC5_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors) << "a datatype declaration with at least one constructor"; CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors); + for (size_t i = 0, size = ctors.size(); i < size; i++) + { + CVC5_API_CHECK(!ctors[i].isResolved()) + << "cannot use a constructor for multiple datatypes"; + } //////// all checks before this line DatatypeDecl dtdecl(this, symbol); for (size_t i = 0, size = ctors.size(); i < size; i++) @@ -6716,7 +6830,7 @@ Term Solver::defineFun(const std::string& symbol, CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort); CVC5_API_SOLVER_CHECK_TERM(term); - CVC5_API_CHECK(sort == term.getSort()) + CVC5_API_CHECK(term.getSort().isSubsortOf(sort)) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -6743,37 +6857,6 @@ Term Solver::defineFun(const std::string& symbol, CVC5_API_TRY_CATCH_END; } -Term Solver::defineFun(const Term& fun, - const std::vector& bound_vars, - const Term& term, - bool global) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_TERM(fun); - CVC5_API_SOLVER_CHECK_TERM(term); - if (fun.getSort().isFunction()) - { - std::vector domain_sorts = fun.getSort().getFunctionDomainSorts(); - CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); - Sort codomain = fun.getSort().getFunctionCodomainSort(); - CVC5_API_CHECK(codomain == term.getSort()) - << "Invalid sort of function body '" << term << "', expected '" - << codomain << "'"; - } - else - { - CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars); - CVC5_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun) - << "function or nullary symbol"; - } - //////// all checks before this line - std::vector ebound_vars = Term::termVectorToNodes(bound_vars); - d_slv->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); - return fun; - //////// - CVC5_API_TRY_CATCH_END; -} - Term Solver::defineFunRec(const std::string& symbol, const std::vector& bound_vars, const Sort& sort, @@ -6933,12 +7016,7 @@ std::vector Solver::getAssertions(void) const /* Can not use * return std::vector(assertions.begin(), assertions.end()); * here since constructor is private */ - std::vector res; - for (const Node& e : assertions) - { - res.push_back(Term(this, e)); - } - return res; + return Term::nodeVectorToTerms(this, assertions); //////// CVC5_API_TRY_CATCH_END; } @@ -6946,8 +7024,8 @@ std::vector Solver::getAssertions(void) const std::string Solver::getInfo(const std::string& flag) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_slv->isValidGetInfoFlag(flag)) - << "Unrecognized flag for getInfo."; + CVC5_API_UNSUPPORTED_CHECK(d_slv->isValidGetInfoFlag(flag)) + << "Unrecognized flag: " << flag << "."; //////// all checks before this line return d_slv->getInfo(flag); //////// @@ -6956,11 +7034,14 @@ std::string Solver::getInfo(const std::string& flag) const std::string Solver::getOption(const std::string& option) const { - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return d_slv->getOption(option); - //////// - CVC5_API_TRY_CATCH_END; + try + { + return d_slv->getOption(option); + } + catch (OptionException& e) + { + throw CVC5ApiUnsupportedException(e.getMessage()); + } } // Supports a visitor from a list of lambdas @@ -7214,7 +7295,7 @@ std::map Solver::getDifficulty() const CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT || d_slv->getSmtMode() == SmtMode::SAT || d_slv->getSmtMode() == SmtMode::SAT_UNKNOWN) - << "Cannot get difficulty unless after a UNSAT, SAT or unknown response."; + << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response."; //////// all checks before this line std::map res; std::map dmap; @@ -7239,10 +7320,39 @@ std::string Solver::getProof(void) const CVC5_API_TRY_CATCH_END; } +std::vector Solver::getLearnedLiterals(void) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(d_slv->getOptions().smt.produceLearnedLiterals) + << "Cannot get learned literals unless enabled (try " + "--produce-learned-literals)"; + CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT + || d_slv->getSmtMode() == SmtMode::SAT + || d_slv->getSmtMode() == SmtMode::SAT_UNKNOWN) + << "Cannot get learned literals unless after a UNSAT, SAT or UNKNOWN " + "response."; + //////// all checks before this line + std::vector lits = d_slv->getLearnedLiterals(); + return Term::nodeVectorToTerms(this, lits); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::getValue(const Term& term) const { CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels) + << "Cannot get value unless model generation is enabled " + "(try --produce-models)"; + CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) + << "Cannot get value unless after a SAT or UNKNOWN response."; CVC5_API_SOLVER_CHECK_TERM(term); + CVC5_API_RECOVERABLE_CHECK(term.getSort().isFirstClass()) + << "Cannot get value of a term that is not first class."; + CVC5_API_RECOVERABLE_CHECK(!term.getSort().isDatatype() + || term.getSort().getDatatype().isWellFounded()) + << "Cannot get value of a term of non-well-founded datatype sort."; + ensureWellFormedTerm(term); //////// all checks before this line return getValueHelper(term); //////// @@ -7256,8 +7366,17 @@ std::vector Solver::getValue(const std::vector& terms) const << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Cannot get value unless after a SAT or unknown response."; + << "Cannot get value unless after a SAT or UNKNOWN response."; + for (const Term& t : terms) + { + CVC5_API_RECOVERABLE_CHECK(t.getSort().isFirstClass()) + << "Cannot get value of a term that is not first class."; + CVC5_API_RECOVERABLE_CHECK(!t.getSort().isDatatype() + || t.getSort().getDatatype().isWellFounded()) + << "Cannot get value of a term of non-well-founded datatype sort."; + } CVC5_API_SOLVER_CHECK_TERMS(terms); + ensureWellFormedTerms(terms); //////// all checks before this line std::vector res; @@ -7278,7 +7397,7 @@ std::vector Solver::getModelDomainElements(const Sort& s) const << "Cannot get domain elements unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Cannot get domain elements unless after a SAT or unknown response."; + << "Cannot get domain elements unless after a SAT or UNKNOWN response."; CVC5_API_SOLVER_CHECK_SORT(s); CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort()) << "Expecting an uninterpreted sort as argument to " @@ -7302,7 +7421,7 @@ bool Solver::isModelCoreSymbol(const Term& v) const << "Cannot check if model core symbol unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Cannot check if model core symbol unless after a SAT or unknown " + << "Cannot check if model core symbol unless after a SAT or UNKNOWN " "response."; CVC5_API_SOLVER_CHECK_TERM(v); CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT) @@ -7321,7 +7440,7 @@ std::string Solver::getModel(const std::vector& sorts, << "Cannot get model unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Cannot get model unless after a SAT or unknown response."; + << "Cannot get model unless after a SAT or UNKNOWN response."; CVC5_API_SOLVER_CHECK_SORTS(sorts); for (const Sort& s : sorts) { @@ -7347,7 +7466,7 @@ Term Solver::getQuantifierElimination(const Term& q) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term(this, d_slv->getQuantifierElimination(q.getNode(), true, true)); + return Term(this, d_slv->getQuantifierElimination(q.getNode(), true)); //////// CVC5_API_TRY_CATCH_END; } @@ -7357,13 +7476,12 @@ Term Solver::getQuantifierEliminationDisjunct(const Term& q) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term(this, d_slv->getQuantifierElimination(q.getNode(), false, true)); + return Term(this, d_slv->getQuantifierElimination(q.getNode(), false)); //////// CVC5_API_TRY_CATCH_END; } -void Solver::declareSeparationHeap(const Sort& locSort, - const Sort& dataSort) const +void Solver::declareSepHeap(const Sort& locSort, const Sort& dataSort) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(locSort); @@ -7377,7 +7495,7 @@ void Solver::declareSeparationHeap(const Sort& locSort, CVC5_API_TRY_CATCH_END; } -Term Solver::getSeparationHeap() const +Term Solver::getValueSepHeap() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) @@ -7387,14 +7505,14 @@ Term Solver::getSeparationHeap() const << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Can only get separtion heap term after sat or unknown response."; + << "Can only get separtion heap term after SAT or UNKNOWN response."; //////// all checks before this line return Term(this, d_slv->getSepHeapExpr()); //////// CVC5_API_TRY_CATCH_END; } -Term Solver::getSeparationNilTerm() const +Term Solver::getValueSepNil() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) @@ -7404,7 +7522,7 @@ Term Solver::getSeparationNilTerm() const << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Can only get separtion nil term after sat or unknown response."; + << "Can only get separtion nil term after SAT or UNKNOWN response."; //////// all checks before this line return Term(this, d_slv->getSepNilExpr()); //////// @@ -7448,9 +7566,14 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + << "Cannot get interpolant unless interpolants are enabled (try " + "--produce-interpols=mode)"; //////// all checks before this line Node result; - bool success = d_slv->getInterpol(*conj.d_node, result); + TypeNode nullType; + bool success = d_slv->getInterpolant(*conj.d_node, nullType, result); if (success) { output = Term(this, result); @@ -7466,10 +7589,36 @@ bool Solver::getInterpolant(const Term& conj, { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + << "Cannot get interpolant unless interpolants are enabled (try " + "--produce-interpols=mode)"; //////// all checks before this line Node result; bool success = - d_slv->getInterpol(*conj.d_node, *grammar.resolve().d_type, result); + d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type, result); + if (success) + { + output = Term(this, result); + } + return success; + //////// + CVC5_API_TRY_CATCH_END; +} + +bool Solver::getInterpolantNext(Term& output) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols + != options::ProduceInterpols::NONE) + << "Cannot get interpolant unless interpolants are enabled (try " + "--produce-interpols=mode)"; + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) + << "Cannot get next interpolant when not solving incrementally (try " + "--incremental)"; + //////// all checks before this line + Node result; + bool success = d_slv->getInterpolantNext(result); if (success) { output = Term(this, result); @@ -7487,7 +7636,8 @@ bool Solver::getAbduct(const Term& conj, Term& output) const << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line Node result; - bool success = d_slv->getAbduct(*conj.d_node, result); + TypeNode nullType; + bool success = d_slv->getAbduct(*conj.d_node, nullType, result); if (success) { output = Term(this, result); @@ -7516,6 +7666,27 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const CVC5_API_TRY_CATCH_END; } +bool Solver::getAbductNext(Term& output) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) + << "Cannot get next abduct unless abducts are enabled (try " + "--produce-abducts)"; + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) + << "Cannot get next abduct when not solving incrementally (try " + "--incremental)"; + //////// all checks before this line + Node result; + bool success = d_slv->getAbductNext(result); + if (success) + { + output = Term(this, result); + } + return success; + //////// + CVC5_API_TRY_CATCH_END; +} + void Solver::blockModel() const { CVC5_API_TRY_CATCH_BEGIN; @@ -7523,7 +7694,7 @@ void Solver::blockModel() const << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Can only block model after sat or unknown response."; + << "Can only block model after SAT or UNKNOWN response."; //////// all checks before this line d_slv->blockModel(); //////// @@ -7537,10 +7708,11 @@ void Solver::blockModelValues(const std::vector& terms) const << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) - << "Can only block model values after sat or unknown response."; + << "Can only block model values after SAT or UNKNOWN response."; CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "a non-empty set of terms"; CVC5_API_SOLVER_CHECK_TERMS(terms); + ensureWellFormedTerms(terms); //////// all checks before this line d_slv->blockModelValues(Term::termVectorToNodes(terms)); //////// @@ -7582,13 +7754,14 @@ void Solver::resetAssertions(void) const void Solver::setInfo(const std::string& keyword, const std::string& value) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED( + CVC5_API_UNSUPPORTED_CHECK( keyword == "source" || keyword == "category" || keyword == "difficulty" - || keyword == "filename" || keyword == "license" || keyword == "name" - || keyword == "notes" || keyword == "smt-lib-version" - || keyword == "status", - keyword) - << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " + || keyword == "filename" || keyword == "license" || keyword == "name" + || keyword == "notes" || keyword == "smt-lib-version" + || keyword == "status") + << "Unrecognized keyword: " << keyword + << ", expected 'source', 'category', 'difficulty', " + "'filename', 'license', 'name', " "'notes', 'smt-lib-version' or 'status'"; CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED( keyword != "smt-lib-version" || value == "2" || value == "2.0" @@ -7621,6 +7794,11 @@ void Solver::setOption(const std::string& option, const std::string& value) const { CVC5_API_TRY_CATCH_BEGIN; + std::vector options = options::getNames(); + CVC5_API_UNSUPPORTED_CHECK( + option.find("command-verbosity") != std::string::npos + || std::find(options.cbegin(), options.cend(), option) != options.cend()) + << "Unrecognized option: " << option << '.'; static constexpr auto mutableOpts = {"diagnostic-output-channel", "print-success", "regular-output-channel", @@ -7807,6 +7985,18 @@ Result Solver::checkSynth() const CVC5_API_TRY_CATCH_END; } +Result Solver::checkSynthNext() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) + << "Cannot checkSynthNext when not solving incrementally (use " + "--incremental)"; + //////// all checks before this line + return d_slv->checkSynth(true); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::getSynthSolution(Term term) const { CVC5_API_TRY_CATCH_BEGIN; @@ -7880,12 +8070,12 @@ bool Solver::isOutputOn(const std::string& tag) const std::ostream& Solver::getOutput(const std::string& tag) const { - // `getOutput(tag)` may raise an `OptionException`, which we do not want to + // `output(tag)` may raise an `OptionException`, which we do not want to // forward as such. We thus do not use the standard exception handling macros // here but roll our own. try { - return d_slv->getEnv().getOutput(tag); + return d_slv->getEnv().output(tag); } catch (const cvc5::Exception& e) {