Eliminate use of getBaseType (#8764)

For the model, this was used for ensuring that we skipped enumerating the Real constant 1.0 if the Integer constant 1 already existed in the model. Now, these two nodes are disjoint, and due to #8740, the use of getBaseType in this context has no effect since the set of real and integer constants are disjoint.

It was also used in CEGQI in a similar manner, where since equivalence classes of Int and Real terms are disjoint, it is not necessary to search for e.g. Real variables in integer equivalence classes.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 748677e6465900b8cb64627a4a8f3f8aa6bbc815..4afbd04aadfbd0dc24ed73a320ce1f059176a64c 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -337,14 +337,6 @@ TypeNode TypeNode::getSequenceElementType() const
   return (*this)[0];
 }
 
-TypeNode TypeNode::getBaseType() const {
-  TypeNode realt = NodeManager::currentNM()->realType();
-  if (isSubtypeOf(realt)) {
-    return realt;
-  }
-  return *this;
-}
-
 std::vector<TypeNode> TypeNode::getArgTypes() const {
   vector<TypeNode> args;
   if (isDatatypeTester())

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 314935da8813af0ca4707acd2a633cf76b6e56c8..d20ad0bc221e839bd85563de38ac8066bdf2ce2b 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -688,9 +688,6 @@ private:
    */
   TypeNode getUninterpretedSortConstructor() const;
 
-  /** Get the most general base type of the type */
-  TypeNode getBaseType() const;
-
   /**
    * Returns the leastUpperBound in the extended type lattice of the two types.
    * If this is \top, i.e. there is no inhabited type that contains both,

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 8ef7f3d6fcb36803feb11a3c414979af0220f9a5..6d0f41aa14c943145351235a9fa27c5c8644a203 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -686,7 +686,6 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
                                              Node pv)
 {
   TypeNode pvtn = pv.getType();
-  TypeNode pvtnb = pvtn.getBaseType();
   Node pvr = pv;
   eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
   if (ee->hasTerm(pv))
@@ -783,7 +782,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
     Trace("cegqi-inst-debug")
         << "[2] try based on solving equalities." << std::endl;
     d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
-    std::vector<Node>& cteqc = d_curr_type_eqc[pvtnb];
+    std::vector<Node>& cteqc = d_curr_type_eqc[pvtn];
 
     for (const Node& r : cteqc)
     {
@@ -1416,10 +1415,6 @@ void CegInstantiator::processAssertions() {
     TheoryId tid = d_env.theoryOf(rtn);
     //if we care about the theory of this eqc
     if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){
-      if (rtn.isRealOrInt())
-      {
-        rtn = rtn.getBaseType();
-      }
       Trace("cegqi-proc-debug") << "...type eqc: " << r << std::endl;
       d_curr_type_eqc[rtn].push_back( r );
       if( d_curr_eqc.find( r )==d_curr_eqc.end() ){

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 7720cdcc95dc4626570db7137c3587c551120aa1..8d9f5c0d335e6d459226eb8c42706723432e3339 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -637,15 +637,15 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       // information from another class. Thus, rep may be non-null here.
       // Regardless, we assign constRep as the representative here.
       assignConstantRep(tm, eqc, constRep);
-      typeConstSet.add(eqct.getBaseType(), constRep);
+      typeConstSet.add(eqct, constRep);
       continue;
     }
     else if (!rep.isNull())
     {
       assertedReps[eqc] = rep;
-      typeRepSet.add(eqct.getBaseType(), eqc);
+      typeRepSet.add(eqct, eqc);
       std::unordered_set<TypeNode> visiting;
-      addToTypeList(eqct.getBaseType(), type_list, visiting);
+      addToTypeList(eqct, type_list, visiting);
     }
     else
     {
@@ -758,7 +758,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
       {
         TypeNode t = *type_it;
-        TypeNode tb = t.getBaseType();
+        TypeNode tb = t;
         set<Node>* noRepSet = typeNoRepSet.getSet(t);
 
         // 1. Try to evaluate the EC's in this type
@@ -908,7 +908,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       }
 #endif
 
-      TypeNode tb = t.getBaseType();
+      TypeNode tb = t;
       if (!assignOne)
       {
         set<Node>* repSet = typeRepSet.getSet(tb);
@@ -991,7 +991,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             {
               Trace("model-builder-debug") << "Enumerate term of type " << t
                                            << std::endl;
-              n = typeConstSet.nextTypeEnum(t, true);
+              n = typeConstSet.nextTypeEnum(t);
               //--- AJR: this code checks whether n is a legal value
               Assert(!n.isNull());
               success = true;

diff --git a/src/theory/type_set.cpp b/src/theory/type_set.cpp
index 140ec23f9327c25190a603a2b7424de182372018..86c735afda0228682696d9de37b63cc1c9f13c4b 100644 (file)
--- a/src/theory/type_set.cpp
+++ b/src/theory/type_set.cpp
@@ -65,7 +65,7 @@ std::set<Node>* TypeSet::getSet(TypeNode t) const
   return (*it).second;
 }
 
-Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
+Node TypeSet::nextTypeEnum(TypeNode t)
 {
   TypeEnumerator* te;
   TypeToTypeEnumMap::iterator it = d_teMap.find(t);
@@ -82,11 +82,6 @@ Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
   {
     return Node();
   }
-
-  if (useBaseType)
-  {
-    t = t.getBaseType();
-  }
   iterator itSet = d_typeSet.find(t);
   std::set<Node>* s;
   if (itSet == d_typeSet.end())

diff --git a/src/theory/type_set.h b/src/theory/type_set.h
index 72131927233f862b5c13cc0ea06f62b164f454ba..f5543d8e4646a5dec4a261802e64dd134734303a 100644 (file)
--- a/src/theory/type_set.h
+++ b/src/theory/type_set.h
@@ -52,11 +52,8 @@ class TypeSet
   void add(TypeNode t, TNode n);
   /** get the set of values of type t */
   std::set<Node>* getSet(TypeNode t) const;
-  /** get the next enumerated term of type t
-   *
-   * useBaseType is whether
-   */
-  Node nextTypeEnum(TypeNode t, bool useBaseType = false);
+  /** get the next enumerated term of type t */
+  Node nextTypeEnum(TypeNode t);
 
   bool empty() { return d_typeSet.empty(); }
   iterator begin() { return d_typeSet.begin(); }

diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index b2a349ca0f3c3db79f980442f96c9bf53482c696..b2ea12bb45f55bf72204a5711b316b5717dee589 100644 (file)
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -87,12 +87,6 @@ TEST_F(TestNodeWhiteTypeNode, sub_types)
   ASSERT_FALSE(bvType.isComparableTo(realType));
   ASSERT_FALSE(bvType.isComparableTo(arrayType));
   ASSERT_TRUE(bvType.isComparableTo(bvType));
-
-  ASSERT_TRUE(realType.getBaseType() == realType);
-  ASSERT_TRUE(integerType.getBaseType() == realType);
-  ASSERT_TRUE(booleanType.getBaseType() == booleanType);
-  ASSERT_TRUE(arrayType.getBaseType() == arrayType);
-  ASSERT_TRUE(bvType.getBaseType() == bvType);
 }
 }  // namespace test
 }  // namespace cvc5::internal