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 e16d8c519d728d0864b56a499e7b2bbdeceb104d..2c694dbedfb39ef0f4cfafacc8ce81bd111955c1 100644 (file)
--- 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<Sort> 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<Sort>& sorts, Sort codomain) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
       << "at least one parameter sort for function sort";
@@ -3553,6 +3564,7 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& 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<Sort>& sorts) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
       << "at least one parameter sort for predicate sort";
@@ -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<Sort>& 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 e9f121047b2a4c8e68bce7ede5cfadbfcce22123..7c847d8ce09d1487621cbbe1cdefe9e103aaaf75 100644 (file)
--- 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<TypeConstant>(BOOLEAN_TYPE);
+}
+
+TypeNode NodeManager::integerType()
+{
+  return mkTypeConst<TypeConstant>(INTEGER_TYPE);
+}
+
+TypeNode NodeManager::realType()
+{
+  return mkTypeConst<TypeConstant>(REAL_TYPE);
+}
+
+TypeNode NodeManager::stringType()
+{
+  return mkTypeConst<TypeConstant>(STRING_TYPE);
+}
+
+TypeNode NodeManager::regExpType()
+{
+  return mkTypeConst<TypeConstant>(REGEXP_TYPE);
+}
+
+TypeNode NodeManager::roundingModeType()
+{
+  return mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE);
+}
+
+TypeNode NodeManager::boundVarListType()
+{
+  return mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE);
+}
+
+TypeNode NodeManager::instPatternType()
+{
+  return mkTypeConst<TypeConstant>(INST_PATTERN_TYPE);
+}
+
+TypeNode NodeManager::instPatternListType()
+{
+  return mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE);
+}
+
+TypeNode NodeManager::builtinOperatorType()
+{
+  return mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE);
+}
+
+TypeNode NodeManager::mkBitVectorType(unsigned size)
+{
+  return mkTypeConst<BitVectorSize>(BitVectorSize(size));
+}
+
+TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig)
+{
+  return mkTypeConst<FloatingPointSize>(FloatingPointSize(exp, sig));
+}
+
+TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs)
+{
+  return mkTypeConst<FloatingPointSize>(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 5cf19aab9843d90fc316e667df9ec1d89c840b2d..99db9feb29716543efae9c2443658af3394153f7 100644 (file)
--- 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 <code>exp</code> bit exponent and
       <code>sig</code> 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 <code>size</code> */
-  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<TypeConstant>(BOOLEAN_TYPE));
-}
-
-/** Get the (singleton) type for integers. */
-inline TypeNode NodeManager::integerType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
-}
-
-/** Get the (singleton) type for reals. */
-inline TypeNode NodeManager::realType() {
-  return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
-}
-
-/** Get the (singleton) type for strings. */
-inline TypeNode NodeManager::stringType() {
-  return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
-}
-
-/** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regExpType() {
-  return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
-}
-
-/** Get the (singleton) type for rounding modes. */
-inline TypeNode NodeManager::roundingModeType() {
-  return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
-}
-
-/** Get the bound var list type. */
-inline TypeNode NodeManager::boundVarListType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternListType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
-}
-
-/** Get the (singleton) type for builtin operators. */
-inline TypeNode NodeManager::builtinOperatorType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
-}
-
 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
@@ -1187,18 +1137,6 @@ inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
 }
 
-inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
-  return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
-}
-
-inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
-  return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
-}
-
-inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
-  return TypeNode(mkTypeConst<FloatingPointSize>(fs));
-}
-
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
   CheckArgument(!indexType.isNull(), indexType,