* 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"
#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"
#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"
#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 {
{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},
{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},
{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,
{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},
{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},
{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},
/* 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},
{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},
{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},
{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,
/* 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 ------------------------------------------------ */
{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},
{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},
/* 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},
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 \
{
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;
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;
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<cvc5::TypeNode> tparams = sortVectorToTypeNodes(params);
if (d_type->isDatatype())
{
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;
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;
}
{
case DIVISIBLE:
{
- t = d_solver->mkValHelper<Rational>(
+ t = d_solver->mkRationalValHelper(
Rational(d_node->getConst<Divisible>().k));
break;
}
case BITVECTOR_REPEAT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorRepeat>().d_repeatAmount);
break;
}
case BITVECTOR_ZERO_EXTEND:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount);
break;
}
case BITVECTOR_SIGN_EXTEND:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorSignExtend>().d_signExtendAmount);
break;
}
case BITVECTOR_ROTATE_LEFT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount);
break;
}
case BITVECTOR_ROTATE_RIGHT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount);
break;
}
case INT_TO_BITVECTOR:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<IntToBitVector>().d_size);
break;
}
case IAND:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
- d_node->getConst<IntAnd>().d_size);
+ t = d_solver->mkRationalValHelper(d_node->getConst<IntAnd>().d_size);
break;
}
case FLOATINGPOINT_TO_UBV:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size);
break;
}
case FLOATINGPOINT_TO_SBV:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size);
break;
}
case REGEXP_REPEAT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<RegExpRepeat>().d_repeatAmount);
break;
}
case BITVECTOR_EXTRACT:
{
cvc5::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(ext.d_high)
- : d_solver->mkValHelper<cvc5::Rational>(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:
cvc5::FloatingPointToFPIEEEBitVector ext =
d_node->getConst<FloatingPointToFPIEEEBitVector>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- 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<FloatingPointToFPFloatingPoint>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case FLOATINGPOINT_TO_FP_REAL:
cvc5::FloatingPointToFPReal ext =
d_node->getConst<FloatingPointToFPReal>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- 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<FloatingPointToFPSignedBitVector>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- 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<FloatingPointToFPUnsignedBitVector>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- 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<FloatingPointToFPGeneric>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- 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<RegExpLoop>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(ext.d_loopMinOcc)
- : d_solver->mkValHelper<cvc5::Rational>(ext.d_loopMaxOcc);
+ t = index == 0 ? d_solver->mkRationalValHelper(ext.d_loopMinOcc)
+ : d_solver->mkRationalValHelper(ext.d_loopMaxOcc);
break;
}
{
const std::vector<uint32_t>& projectionIndices =
d_node->getConst<TupleProjectOp>().getIndices();
- t = d_solver->mkValHelper<cvc5::Rational>(projectionIndices[index]);
+ t = d_solver->mkRationalValHelper(projectionIndices[index]);
break;
}
default:
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,
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<Node> nodes = Term::termVectorToNodes(terms);
std::vector<Node> nodeReplacements = Term::termVectorToNodes(replacements);
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;
{
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;
}
} // 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<int32_t>(r.sgn());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
bool Term::isInt32Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
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;
}
<< "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;
}
return res;
}
+std::vector<Term> Term::nodeVectorToTerms(const Solver* slv,
+ const std::vector<Node>& nodes)
+{
+ std::vector<Term> res;
+ for (const Node& n : nodes)
+ {
+ res.push_back(Term(slv, n));
+ }
+ return res;
+}
+
bool Term::isReal32Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
<< "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;
}
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<AbstractValue>().getIndex().toString();
+ std::stringstream ss;
+ ss << d_node->getConst<UninterpretedSortValue>();
+ return ss.str();
////////
CVC5_API_TRY_CATCH_END;
}
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)
{
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<Sort, std::int32_t> 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<UninterpretedConstant>();
- 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();
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);
////////
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) {}
CVC5_API_TRY_CATCH_END;
}
-Sort DatatypeSelector::getRangeSort() const
+Sort DatatypeSelector::getCodomainSort() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
CVC5_API_TRY_CATCH_END;
}
-Term DatatypeConstructor::getSpecializedConstructorTerm(
+Term DatatypeConstructor::getInstantiatedConstructorTerm(
const Sort& retSort) const
{
CVC5_API_TRY_CATCH_BEGIN;
<< "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);
CVC5_API_TRY_CATCH_END;
}
+std::vector<Sort> 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<cvc5::TypeNode> params = d_dtype->getParameters();
+ return Sort::typeNodeVectorToSorts(d_solver, params);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
bool Datatype::isParametric() const
{
CVC5_API_TRY_CATCH_BEGIN;
{
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
////////
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
{
bool Grammar::containsFreeVariables(const Term& rule) const
{
+ // we allow the argument list and non-terminal symbols to be in scope
std::unordered_set<TNode> scope;
for (const Term& sygusVar : d_sygusVars)
scope.emplace(*ntsymbol.d_node);
}
- std::unordered_set<Node> 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)
void Solver::increment_term_stats(Kind kind) const
{
- if constexpr (Configuration::isStatisticsBuild())
+ if constexpr (configuration::isStatisticsBuild())
{
d_stats->d_terms << kind;
}
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
/* .......................................................................... */
template <typename T>
-Term Solver::mkValHelper(T t) const
+Term Solver::mkValHelper(const T& t) const
{
//////// all checks before this line
Node res = getNodeManager()->mkConst(t);
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
cvc5::Rational r = s.find('/') != std::string::npos
? cvc5::Rational(s)
: cvc5::Rational::fromDecimal(s);
- return mkValHelper<cvc5::Rational>(r);
+ return mkRationalValHelper(r, isInt);
}
catch (const std::invalid_argument& e)
{
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";
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 << ")";
}
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);
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<Node>());
{
// 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<Node> 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);
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()
// 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()
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);
Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& 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<Node> echildren = Term::termVectorToNodes(children);
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;
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<Term>& 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<TypeConstant>(
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
{
{
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
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- Term integer = mkValHelper<cvc5::Rational>(cvc5::Rational(val));
+ Term integer = mkRationalValHelper(cvc5::Rational(val));
Assert(integer.getSort() == getIntegerSort());
return integer;
////////
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;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(val));
- return ensureRealSort(rational);
+ return mkRationalValHelper(cvc5::Rational(val), false);
////////
CVC5_API_TRY_CATCH_END;
}
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- Term rational = mkValHelper<cvc5::Rational>(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<cvc5::Node>());
+ d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALL, std::vector<cvc5::Node>());
(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<cvc5::Node>());
+ d_nodeMgr->mkNode(cvc5::kind::REGEXP_NONE, std::vector<cvc5::Node>());
+ (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<cvc5::Node>());
(void)res.getType(true); /* kick off type checking */
return Term(this, res);
////////
//////// 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);
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
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
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
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
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
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>(
- 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;
{
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));
<< "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);
////////
<< "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));
////////
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);
////////
<< "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);
////////
<< "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)
{
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++)
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
<< "'";
CVC5_API_TRY_CATCH_END;
}
-Term Solver::defineFun(const Term& fun,
- const std::vector<Term>& 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<Sort> 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<Node> 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<Term>& bound_vars,
const Sort& sort,
/* Can not use
* return std::vector<Term>(assertions.begin(), assertions.end());
* here since constructor is private */
- std::vector<Term> res;
- for (const Node& e : assertions)
- {
- res.push_back(Term(this, e));
- }
- return res;
+ return Term::nodeVectorToTerms(this, assertions);
////////
CVC5_API_TRY_CATCH_END;
}
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);
////////
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
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<Term, Term> res;
std::map<Node, Node> dmap;
CVC5_API_TRY_CATCH_END;
}
+std::vector<Term> 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<Node> 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);
////////
<< "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<Term> res;
<< "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 "
<< "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)
<< "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)
{
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;
}
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);
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))
<< "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))
<< "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());
////////
{
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);
{
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);
<< "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);
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;
<< "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();
////////
<< "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));
////////
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"
const std::string& value) const
{
CVC5_API_TRY_CATCH_BEGIN;
+ std::vector<std::string> 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",
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;
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)
{
projects / cvc5.git / blobdiff