From: Andrew Reynolds Date: Tue, 3 Nov 2020 23:47:15 +0000 (-0600) Subject: Add scope methods constructing types in API (#5393) X-Git-Tag: cvc5-1.0.0~2634 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7029e89bc6ada688da48dc54362aef180b7c20ef;p=cvc5.git Add scope methods constructing types in API (#5393) This addresses the nightly failures. It ensures a node manager is in scope when constructing type nodes. It also simplifies the construction of atomic type nodes to avoid an extra TypeNode(...) constructor. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e16d8c519..2c694dbed 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3386,6 +3386,7 @@ Sort Solver::getNullSort(void) const Sort Solver::getBooleanSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->booleanType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3393,6 +3394,7 @@ Sort Solver::getBooleanSort(void) const Sort Solver::getIntegerSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->integerType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3400,6 +3402,7 @@ Sort Solver::getIntegerSort(void) const Sort Solver::getRealSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->realType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3407,6 +3410,7 @@ Sort Solver::getRealSort(void) const Sort Solver::getRegExpSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->regExpType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3414,6 +3418,7 @@ Sort Solver::getRegExpSort(void) const Sort Solver::getStringSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->stringType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3421,6 +3426,7 @@ Sort Solver::getStringSort(void) const Sort Solver::getRoundingModeSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; @@ -3432,6 +3438,7 @@ Sort Solver::getRoundingModeSort(void) const Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort) << "non-null index sort"; @@ -3448,6 +3455,7 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const Sort Solver::mkBitVectorSort(uint32_t size) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; @@ -3458,6 +3466,7 @@ Sort Solver::mkBitVectorSort(uint32_t size) const Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; @@ -3503,6 +3512,7 @@ std::vector Solver::mkDatatypeSorts( Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) << "non-null codomain sort"; @@ -3522,6 +3532,7 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const Sort Solver::mkFunctionSort(const std::vector& sorts, Sort codomain) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for function sort"; @@ -3553,6 +3564,7 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, Sort codomain) const Sort Solver::mkParamSort(const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort( this, @@ -3562,6 +3574,7 @@ Sort Solver::mkParamSort(const std::string& symbol) const Sort Solver::mkPredicateSort(const std::vector& sorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for predicate sort"; @@ -3610,6 +3623,7 @@ Sort Solver::mkRecordSort( Sort Solver::mkSetSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; @@ -3622,6 +3636,7 @@ Sort Solver::mkSetSort(Sort elemSort) const Sort Solver::mkBagSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; @@ -3634,6 +3649,7 @@ Sort Solver::mkBagSort(Sort elemSort) const Sort Solver::mkSequenceSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; @@ -3646,6 +3662,7 @@ Sort Solver::mkSequenceSort(Sort elemSort) const Sort Solver::mkUninterpretedSort(const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->mkSort(symbol)); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3654,6 +3671,7 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; @@ -3664,6 +3682,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol, Sort Solver::mkTupleSort(const std::vector& sorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = sorts.size(); i < size; ++i) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e9f121047..7c847d8ce 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -105,6 +105,71 @@ NodeManager::NodeManager(ExprManager* exprManager) init(); } +TypeNode NodeManager::booleanType() +{ + return mkTypeConst(BOOLEAN_TYPE); +} + +TypeNode NodeManager::integerType() +{ + return mkTypeConst(INTEGER_TYPE); +} + +TypeNode NodeManager::realType() +{ + return mkTypeConst(REAL_TYPE); +} + +TypeNode NodeManager::stringType() +{ + return mkTypeConst(STRING_TYPE); +} + +TypeNode NodeManager::regExpType() +{ + return mkTypeConst(REGEXP_TYPE); +} + +TypeNode NodeManager::roundingModeType() +{ + return mkTypeConst(ROUNDINGMODE_TYPE); +} + +TypeNode NodeManager::boundVarListType() +{ + return mkTypeConst(BOUND_VAR_LIST_TYPE); +} + +TypeNode NodeManager::instPatternType() +{ + return mkTypeConst(INST_PATTERN_TYPE); +} + +TypeNode NodeManager::instPatternListType() +{ + return mkTypeConst(INST_PATTERN_LIST_TYPE); +} + +TypeNode NodeManager::builtinOperatorType() +{ + return mkTypeConst(BUILTIN_OPERATOR_TYPE); +} + +TypeNode NodeManager::mkBitVectorType(unsigned size) +{ + return mkTypeConst(BitVectorSize(size)); +} + +TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) +{ + return mkTypeConst(FloatingPointSize(exp, sig)); +} + +TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) +{ + return mkTypeConst(fs); +} + void NodeManager::init() { // `mkConst()` indirectly needs the correct NodeManager in scope because we // call `NodeValue::inc()` which uses `NodeManager::curentNM()` diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5cf19aab9..99db9feb2 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -808,37 +808,37 @@ class NodeManager { const typename AttrKind::value_type& value); /** Get the (singleton) type for Booleans. */ - inline TypeNode booleanType(); + TypeNode booleanType(); /** Get the (singleton) type for integers. */ - inline TypeNode integerType(); + TypeNode integerType(); /** Get the (singleton) type for reals. */ - inline TypeNode realType(); + TypeNode realType(); /** Get the (singleton) type for strings. */ - inline TypeNode stringType(); + TypeNode stringType(); /** Get the (singleton) type for RegExp. */ - inline TypeNode regExpType(); + TypeNode regExpType(); /** Get the (singleton) type for rounding modes. */ - inline TypeNode roundingModeType(); + TypeNode roundingModeType(); /** Get the bound var list type. */ - inline TypeNode boundVarListType(); + TypeNode boundVarListType(); /** Get the instantiation pattern type. */ - inline TypeNode instPatternType(); + TypeNode instPatternType(); /** Get the instantiation pattern type. */ - inline TypeNode instPatternListType(); + TypeNode instPatternListType(); /** * Get the (singleton) type for builtin operators (that is, the type * of the Node returned from Node::getOperator() when the operator * is built-in, like EQUAL). */ - inline TypeNode builtinOperatorType(); + TypeNode builtinOperatorType(); /** * Make a function type from domain to range. @@ -906,11 +906,11 @@ class NodeManager { /** Make the type of floating-point with exp bit exponent and sig bit significand */ - inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); - inline TypeNode mkFloatingPointType(FloatingPointSize fs); + TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + TypeNode mkFloatingPointType(FloatingPointSize fs); /** Make the type of bitvectors of size size */ - inline TypeNode mkBitVectorType(unsigned size); + TypeNode mkBitVectorType(unsigned size); /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); @@ -1129,56 +1129,6 @@ public: } };/* class NodeManagerScope */ -/** Get the (singleton) type for booleans. */ -inline TypeNode NodeManager::booleanType() { - return TypeNode(mkTypeConst(BOOLEAN_TYPE)); -} - -/** Get the (singleton) type for integers. */ -inline TypeNode NodeManager::integerType() { - return TypeNode(mkTypeConst(INTEGER_TYPE)); -} - -/** Get the (singleton) type for reals. */ -inline TypeNode NodeManager::realType() { - return TypeNode(mkTypeConst(REAL_TYPE)); -} - -/** Get the (singleton) type for strings. */ -inline TypeNode NodeManager::stringType() { - return TypeNode(mkTypeConst(STRING_TYPE)); -} - -/** Get the (singleton) type for regexps. */ -inline TypeNode NodeManager::regExpType() { - return TypeNode(mkTypeConst(REGEXP_TYPE)); -} - -/** Get the (singleton) type for rounding modes. */ -inline TypeNode NodeManager::roundingModeType() { - return TypeNode(mkTypeConst(ROUNDINGMODE_TYPE)); -} - -/** Get the bound var list type. */ -inline TypeNode NodeManager::boundVarListType() { - return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternType() { - return TypeNode(mkTypeConst(INST_PATTERN_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternListType() { - return TypeNode(mkTypeConst(INST_PATTERN_LIST_TYPE)); -} - -/** Get the (singleton) type for builtin operators. */ -inline TypeNode NodeManager::builtinOperatorType() { - return TypeNode(mkTypeConst(BUILTIN_OPERATOR_TYPE)); -} - inline TypeNode NodeManager::mkSExprType(const std::vector& types) { std::vector typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { @@ -1187,18 +1137,6 @@ inline TypeNode NodeManager::mkSExprType(const std::vector& types) { return mkTypeNode(kind::SEXPR_TYPE, typeNodes); } -inline TypeNode NodeManager::mkBitVectorType(unsigned size) { - return TypeNode(mkTypeConst(BitVectorSize(size))); -} - -inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { - return TypeNode(mkTypeConst(FloatingPointSize(exp,sig))); -} - -inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) { - return TypeNode(mkTypeConst(fs)); -} - inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType,