From e33582f42b0998170bc4f30f54290808fc9cf4ac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 May 2022 12:02:33 -0500 Subject: [PATCH] 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. --- src/expr/type_node.cpp | 8 -------- src/expr/type_node.h | 3 --- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 7 +------ src/theory/theory_model_builder.cpp | 12 ++++++------ src/theory/type_set.cpp | 7 +------ src/theory/type_set.h | 7 ++----- test/unit/node/type_node_white.cpp | 6 ------ 7 files changed, 10 insertions(+), 40 deletions(-) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 748677e64..4afbd04aa 100644 --- 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::getArgTypes() const { vector args; if (isDatatypeTester()) diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 314935da8..d20ad0bc2 100644 --- 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 8ef7f3d6f..6d0f41aa1 100644 --- 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& cteqc = d_curr_type_eqc[pvtnb]; + std::vector& 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 7720cdcc9..8d9f5c0d3 100644 --- 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 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* 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* 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 140ec23f9..86c735afd 100644 --- a/src/theory/type_set.cpp +++ b/src/theory/type_set.cpp @@ -65,7 +65,7 @@ std::set* 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* s; if (itSet == d_typeSet.end()) diff --git a/src/theory/type_set.h b/src/theory/type_set.h index 721319272..f5543d8e4 100644 --- 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* 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 b2a349ca0..b2ea12bb4 100644 --- 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 -- 2.30.2