TypeNode: Rename isSort() and getSortConstructorArity(). (#8446)

Names of these two functions were slightly confusing with respect to API
terminology. This renames isSort() to isUninterpretedSort() and
getSortConstructorArity() to getUninterpretedSortConstructorArity() for
more consistency and clarity.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index c4b91282594b4a07cc043c59f53430691fe6ecff..aea5add41f2edae1a978439d16ebf177bc798b42 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1405,7 +1405,7 @@ bool Sort::isUninterpretedSort() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return d_type->isSort();
+  return d_type->isUninterpretedSort();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -1414,7 +1414,7 @@ bool Sort::isUninterpretedSortConstructor() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return d_type->isSortConstructor();
+  return d_type->isUninterpretedSortConstructor();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -1445,13 +1445,15 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_DOMAIN_SORTS(params);
-  CVC5_API_CHECK(d_type->isParametricDatatype() || d_type->isSortConstructor())
+  CVC5_API_CHECK(d_type->isParametricDatatype()
+                 || d_type->isUninterpretedSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
   CVC5_API_CHECK(!d_type->isParametricDatatype()
                  || d_type->getNumChildren() == params.size() + 1)
       << "Arity mismatch for instantiated parametric datatype";
-  CVC5_API_CHECK(!d_type->isSortConstructor()
-                 || d_type->getSortConstructorArity() == params.size())
+  CVC5_API_CHECK(!d_type->isUninterpretedSortConstructor()
+                 || d_type->getUninterpretedSortConstructorArity()
+                        == params.size())
       << "Arity mismatch for instantiated sort constructor";
   //////// all checks before this line
   std::vector<internal::TypeNode> tparams = sortVectorToTypeNodes(params);
@@ -1459,7 +1461,7 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   {
     return Sort(d_solver, d_type->instantiateParametricDatatype(tparams));
   }
-  Assert(d_type->isSortConstructor());
+  Assert(d_type->isUninterpretedSortConstructor());
   return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams));
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -1710,9 +1712,10 @@ size_t Sort::getUninterpretedSortConstructorArity() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(d_type->isSortConstructor()) << "Not a sort constructor sort.";
+  CVC5_API_CHECK(d_type->isUninterpretedSortConstructor())
+      << "Not a sort constructor sort.";
   //////// all checks before this line
-  return d_type->getSortConstructorArity();
+  return d_type->getUninterpretedSortConstructorArity();
   ////////
   CVC5_API_TRY_CATCH_END;
 }

diff --git a/src/expr/cardinality_constraint.cpp b/src/expr/cardinality_constraint.cpp
index a470dfb3ae275adb9c5b6746e6a2e68b36ea4294..5f6c33dbf1de18e7d81cb1f91290728e2b3fd913 100644 (file)
--- a/src/expr/cardinality_constraint.cpp
+++ b/src/expr/cardinality_constraint.cpp
@@ -25,7 +25,7 @@ CardinalityConstraint::CardinalityConstraint(const TypeNode& type,
                                              const Integer& ub)
     : d_type(new TypeNode(type)), d_ubound(ub)
 {
-  AlwaysAssert(type.isSort())
+  AlwaysAssert(type.isUninterpretedSort())
       << "Unexpected cardinality constraints for " << type;
 }
 

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 4375ac6e3898b2fcd09c8e6836403bc9600531f7..5fbceee64ec7dd4a20a288204cae0d61fd4b4b1e 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -446,7 +446,7 @@ bool DType::computeCardinalityRecSingleton(
       TypeNode tc = d_constructors[0]->getArgType(i);
       // if it is an uninterpreted sort, then we depend on it having cardinality
       // one
-      if (tc.isSort())
+      if (tc.isUninterpretedSort())
       {
         if (std::find(u_assume.begin(), u_assume.end(), tc) == u_assume.end())
         {

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 71ec23f8dde99f0e4b254b27ede425bd635230c7..8cde888d6975e73c78526d11f02b026c0d1d0f01 100644 (file)
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -310,7 +310,7 @@ bool DTypeConstructor::involvesUninterpretedType() const
 {
   for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
   {
-    if (!getArgType(i).isSort())
+    if (!getArgType(i).isUninterpretedSort())
     {
       return true;
     }
@@ -645,7 +645,8 @@ TypeNode DTypeConstructor::doParametricSubstitution(
   }
   for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
   {
-    if (paramTypes[i].getSortConstructorArity() == origChildren.size())
+    if (paramTypes[i].getUninterpretedSortConstructorArity()
+        == origChildren.size())
     {
       TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren);
       if (range == tn)

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 9f8e8885a8acec0b639dab5a50445a57373a35c9..6bd665f26b9fd9d28e5ecc3378339862f06b7b09 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -645,14 +645,14 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
     // unresolved SortType used as a placeholder in complex types)
     // with "(*resolver).second" (the TypeNode we created in the
     // first step, above).
-    if (ut.isSort())
+    if (ut.isUninterpretedSort())
     {
       placeholders.push_back(ut);
       replacements.push_back((*resolver).second);
     }
     else
     {
-      Assert(ut.isSortConstructor());
+      Assert(ut.isUninterpretedSortConstructor());
       paramTypes.push_back(ut);
       paramReplacements.push_back((*resolver).second);
     }

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 8c0bd44dce264d462930f64c3f7b9c0699048ce5..7280c590290bd86fb6c8ea2ee5ec4d034e234eed 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -490,11 +490,13 @@ cvc5::Sort SymbolTable::Implementation::lookupType(
                         "expected parametric datatype");
     return p.second.instantiate(params);
   }
-  bool isSortConstructor = p.second.isUninterpretedSortConstructor();
+  bool isUninterpretedSortConstructor =
+      p.second.isUninterpretedSortConstructor();
   if (TraceIsOn("sort"))
   {
     Trace("sort") << "instantiating using a sort "
-                  << (isSortConstructor ? "constructor" : "substitution")
+                  << (isUninterpretedSortConstructor ? "constructor"
+                                                     : "substitution")
                   << std::endl;
     Trace("sort") << "have formals [";
     copy(p.first.begin(),
@@ -508,10 +510,9 @@ cvc5::Sort SymbolTable::Implementation::lookupType(
                   << "type ctor    " << name << std::endl
                   << "type is      " << p.second << std::endl;
   }
-  cvc5::Sort instantiation = isSortConstructor
-                                 ? p.second.instantiate(params)
-                                 : p.second.substitute(p.first, params);
-
+  cvc5::Sort instantiation = isUninterpretedSortConstructor
+                                ? p.second.instantiate(params)
+                                : p.second.substitute(p.first, params);
   Trace("sort") << "instance is  " << instantiation << std::endl;
 
   return instantiation;

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 5fa22a1a907b4819bef1a58bc98de06cf4ef89d2..2f92e92332b0f91acb12069bbd837ea982884fa0 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -96,7 +96,7 @@ CardinalityClass TypeNode::getCardinalityClass()
         getAttribute(TypeCardinalityClassAttr()));
   }
   CardinalityClass ret = CardinalityClass::INFINITE;
-  if (isSort())
+  if (isUninterpretedSort())
   {
     ret = CardinalityClass::INTERPRETED_ONE;
   }
@@ -217,7 +217,8 @@ bool TypeNode::isClosedEnumerable()
   if (!getAttribute(IsClosedEnumerableComputedAttr()))
   {
     bool ret = true;
-    if (isArray() || isSort() || isCodatatype() || isFunction() || isRegExp())
+    if (isArray() || isUninterpretedSort() || isCodatatype() || isFunction()
+        || isRegExp())
     {
       ret = false;
     }
@@ -424,7 +425,7 @@ bool TypeNode::isInstantiatedDatatype() const {
 bool TypeNode::isInstantiated() const
 {
   return isInstantiatedDatatype()
-         || (isSort() && getNumChildren() > 0);
+         || (isUninterpretedSort() && getNumChildren() > 0);
 }
 
 TypeNode TypeNode::instantiateParametricDatatype(
@@ -443,22 +444,23 @@ TypeNode TypeNode::instantiateParametricDatatype(
   return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
 }
 
-uint64_t TypeNode::getSortConstructorArity() const
+uint64_t TypeNode::getUninterpretedSortConstructorArity() const
 {
-  Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr()));
+  Assert(isUninterpretedSortConstructor()
+         && hasAttribute(expr::SortArityAttr()));
   return getAttribute(expr::SortArityAttr());
 }
 
 std::string TypeNode::getName() const
 {
-  Assert(isSort() || isSortConstructor());
+  Assert(isUninterpretedSort() || isUninterpretedSortConstructor());
   return getAttribute(expr::VarNameAttr());
 }
 
 TypeNode TypeNode::instantiateSortConstructor(
     const std::vector<TypeNode>& params) const
 {
-  Assert(isSortConstructor());
+  Assert(isUninterpretedSortConstructor());
   return NodeManager::currentNM()->mkSort(*this, params);
 }
 
@@ -570,12 +572,14 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
 }
 
 /** Is this a sort kind */
-bool TypeNode::isSort() const {
+bool TypeNode::isUninterpretedSort() const
+{
   return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
 }
 
 /** Is this a sort constructor kind */
-bool TypeNode::isSortConstructor() const {
+bool TypeNode::isUninterpretedSortConstructor() const
+{
   return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 }
 

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 8c6e98ddbb0297ca22c10afd45939a1a730abc44..584c64554d940b6f1bcb368fd099ee2289899212 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -650,13 +650,13 @@ private:
   uint32_t getBitVectorSize() const;
 
   /** Is this a sort kind */
-  bool isSort() const;
+  bool isUninterpretedSort() const;
 
   /** Is this a sort constructor kind */
-  bool isSortConstructor() const;
+  bool isUninterpretedSortConstructor() const;
 
   /** Get sort constructor arity */
-  uint64_t getSortConstructorArity() const;
+  uint64_t getUninterpretedSortConstructorArity() const;
 
   /**
    * Get name, for uninterpreted sorts and uninterpreted sort constructors.

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index f1b1e2257632f79f254fc4319017fc283e1f3bad..4788e57f56ee4203aeae4952767a16f210cc015f 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -239,7 +239,7 @@ std::unordered_set<TNode> getVarsWithUSorts(AssertionPipeline* assertions)
 
     for (const TNode& var : vars)
     {
-      if (var.getType().isSort())
+      if (var.getType().isUninterpretedSort())
       {
         res.insert(var);
       }

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f7ef49c88465c2c184ebfea4f015d476fd9088cc..583567e9894e671ff2088c1b2b859abaf8963abe 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1387,7 +1387,7 @@ void Smt2Printer::toStreamModelSort(std::ostream& out,
                                     TypeNode tn,
                                     const std::vector<Node>& elements) const
 {
-  if (!tn.isSort())
+  if (!tn.isUninterpretedSort())
   {
     out << "ERROR: don't know how to print non uninterpreted sort in model: "
         << tn << std::endl;
@@ -1651,8 +1651,10 @@ void Smt2Printer::toStreamCmdDefineFunctionRec(
 void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
                                          TypeNode type) const
 {
-  Assert(type.isSort() || type.isSortConstructor());
-  size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
+  Assert(type.isUninterpretedSort() || type.isUninterpretedSortConstructor());
+  size_t arity = type.isUninterpretedSortConstructor()
+                     ? type.getUninterpretedSortConstructorArity()
+                     : 0;
   out << "(declare-sort " << type << " " << arity << ")" << std::endl;
 }
 

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 9a2453eb63ac69ce73a01a6733dc36c14b372677..4259dde07c5cc3f92c0dfab887aceabf3a5a6a30 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -562,7 +562,7 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
       std::stringstream ss;
       options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
       tn.toStream(ss);
-      if (tn.isSort() || (tn.isDatatype() && !tn.isTuple()))
+      if (tn.isUninterpretedSort() || (tn.isDatatype() && !tn.isTuple()))
       {
         std::stringstream sss;
         sss << LfscNodeConverter::getNameForUserName(ss.str());

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index 52b64fe5b607296b6eec3281ff5153d8e5766f42..bba0fad2205552699b210fad1d6ee57415977d67 100644 (file)
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -242,7 +242,7 @@ void LfscPrinter::printTypeDefinition(
     return;
   }
   processed.insert(tn);
-  if (tn.isSort())
+  if (tn.isUninterpretedSort())
   {
     os << "(declare ";
     printType(os, tn);

diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp
index fa9a50a7807b5c4f65016c46c127d05c3d9fd4c2..a02cc4b197f6369d76d7a6959d291521e7971530 100644 (file)
--- a/src/smt/print_benchmark.cpp
+++ b/src/smt/print_benchmark.cpp
@@ -56,7 +56,7 @@ void PrintBenchmark::printAssertions(std::ostream& out,
       std::vector<TypeNode> datatypeBlock;
       for (const TypeNode& ctn : connectedTypes)
       {
-        if (ctn.isSort())
+        if (ctn.isUninterpretedSort())
         {
           d_printer->toStreamCmdDeclareType(out, ctn);
         }
@@ -183,7 +183,7 @@ void PrintBenchmark::getConnectedSubfieldTypes(
     return;
   }
   processed.insert(tn);
-  if (tn.isSort())
+  if (tn.isUninterpretedSort())
   {
     connectedTypes.push_back(tn);
   }

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 247950476b0dca9486de2185b7dc8e5d28d09fbd..59264ee70e886c2a42b7943093c777ec0b76f8fd 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1010,7 +1010,7 @@ std::vector<Node> SolverEngine::getValues(const std::vector<Node>& exprs) const
 
 std::vector<Node> SolverEngine::getModelDomainElements(TypeNode tn) const
 {
-  Assert(tn.isSort());
+  Assert(tn.isUninterpretedSort());
   TheoryModel* m = getAvailableModel("getModelDomainElements");
   return m->getDomainElements(tn);
 }

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 2bc208fa335da9316cdcf8447cfa429846737191..ac58a4d9f797e2f04b129c79b4d75153e242074b 100644 (file)
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -63,7 +63,8 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
           r = tr;
           r = d_qstate.getRepresentative(r);
         }else{
-          if( r.getType().isSort() ){
+          if (r.getType().isUninterpretedSort())
+          {
             Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
             //should never happen : UF constants should never escape model
             Assert(false);

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index f707c952c37045de0d45ddd93f31b662652a5109..57be2d8d4444b2fbac43a39590b3334aa81e1d1b 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -157,7 +157,7 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
 bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
 {
   RepSet* rs = d_model->getRepSetPtr();
-  if (tn.isSort())
+  if (tn.isUninterpretedSort())
   {
     // must ensure uninterpreted type is non-empty.
     if (!rs->hasType(tn))

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 96f33ed5d9104d878f17999df7fab3f5000f3309..464e672579a250c146c69ba1d6e78ed4b1e67c8d 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -438,7 +438,7 @@ void BoundedIntegers::checkOwnership(Node f)
       for( unsigned i=0; i<f[0].getNumChildren(); i++) {
         if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
           TypeNode tn = f[0][i].getType();
-          if ((tn.isSort() && d_env.isFiniteType(tn))
+          if ((tn.isUninterpretedSort() && d_env.isFiniteType(tn))
               || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
           {
             success = true;

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 68548dc4255725f6f8868981123e4e00c7d8b20c..27d49bc46508674629c3ccaf73c003c88a073959 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -65,7 +65,8 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;
       }
     }
-    if( c[index].getType().isSort() ){
+    if (c[index].getType().isUninterpretedSort())
+    {
       //for star: check if all children are defined and have generalizations
       if (c[index] == st)
       {  /// option fmfFmcCoverSimplify
@@ -371,7 +372,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
        it != rs->d_type_reps.end();
        ++it)
   {
-    if( it->first.isSort() ){
+    if (it->first.isUninterpretedSort())
+    {
       Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       for( size_t a=0; a<it->second.size(); a++ ){
         Node r = m->getRepresentative(it->second[a]);
@@ -613,13 +615,16 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
   else
   {
     TypeNode tn = n.getType();
-    if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){
+    if (tn.isUninterpretedSort() && d_rep_ids.find(tn) != d_rep_ids.end())
+    {
       if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
         Trace(tr) << d_rep_ids[tn][n];
       }else{
         Trace(tr) << n;
       }
-    }else{
+    }
+    else
+    {
       Trace(tr) << n;
     }
   }
@@ -1059,7 +1064,8 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
     d.addEntry(fm, mkCond(cond), d_true);
   }else{
     TypeNode tn = eq[0].getType();
-    if( tn.isSort() ){
+    if (tn.isUninterpretedSort())
+    {
       int j = fm->getVariableId(f, eq[0]);
       int k = fm->getVariableId(f, eq[1]);
       const RepSet* rs = fm->getRepSet();
@@ -1076,7 +1082,9 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
         d.addEntry( fm, mkCond(cond), d_true);
       }
       d.addEntry( fm, mkCondDefault(fm, f), d_false);
-    }else{
+    }
+    else
+    {
       d.addEntry( fm, mkCondDefault(fm, f), Node::null());
     }
   }

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 86e4a87781fdf5bf35b31d0f52c7b795a6307124..2c4db6ae79ebe399029a2a337f007b75741a9c1f 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -139,7 +139,8 @@ void ModelEngine::registerQuantifier( Node f ){
     bool canHandle = true;
     for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
       TypeNode tn = f[0][i].getType();
-      if( !tn.isSort() ){
+      if (!tn.isUninterpretedSort())
+      {
         if (!d_env.isFiniteType(tn))
         {
           if( tn.isInteger() ){
@@ -168,8 +169,10 @@ int ModelEngine::checkModel(){
        it != fm->getRepSetPtr()->d_type_reps.end();
        ++it)
   {
-    if( it->first.isSort() ){
-      Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+    if (it->first.isUninterpretedSort())
+    {
+      Trace("model-engine") << "Cardinality( " << it->first << " )"
+                            << " = " << it->second.size() << std::endl;
       Trace("model-engine-debug") << "        Reps : ";
       for( size_t i=0; i<it->second.size(); i++ ){
         Trace("model-engine-debug") << it->second[i] << "  ";

diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp
index effe9147596d85a854cbcc18f15a5fade340fe9b..0552e1d29599e294775c6ee421b2a42712d3a08b 100644 (file)
--- a/src/theory/quantifiers/quant_bound_inference.cpp
+++ b/src/theory/quantifiers/quant_bound_inference.cpp
@@ -73,7 +73,7 @@ bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
     return true;
   }
   TypeNode tn = v.getType();
-  if (tn.isSort() && d_isFmf)
+  if (tn.isUninterpretedSort() && d_isFmf)
   {
     return true;
   }

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 510f2b38fecdcdc759690d0b3f0ff9f4306bf35c..3d9c67b925df6c83022f3b23a67b43abab1c2460 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -533,7 +533,7 @@ bool CegGrammarConstructor::isHandledType(TypeNode t)
   collectSygusGrammarTypesFor(t, types);
   for (const TypeNode& tn : types)
   {
-    if (tn.isSort() || tn.isFloatingPoint())
+    if (tn.isUninterpretedSort() || tn.isFloatingPoint())
     {
       return false;
     }
@@ -1050,7 +1050,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         sdts[i].addConstructor(cop, dt[l].getName(), cargsCons);
       }
     }
-    else if (types[i].isSort() || types[i].isFunction()
+    else if (types[i].isUninterpretedSort() || types[i].isFunction()
              || types[i].isRoundingMode())
     {
       // do nothing

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index a4f897860d93389525cc9a6b4682234b70984bba..4209bf250125459fd4c65f1c2ae1e270b285cec9 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -214,7 +214,8 @@ int TermUtil::getTermDepth( Node n ) {
 bool TermUtil::containsUninterpretedConstant( Node n ) {
   if (!n.hasAttribute(ContainsUConstAttribute()) ){
     bool ret = false;
-    if (n.getKind() == UNINTERPRETED_SORT_VALUE && n.getType().isSort())
+    if (n.getKind() == UNINTERPRETED_SORT_VALUE
+        && n.getType().isUninterpretedSort())
     {
       ret = true;
     }

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index b263544679263838cd3e19ec850d822200464e5b..df161616a3fa265bc071d46f9ccf74dc026432a4 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1197,10 +1197,13 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
 
     //check whether monotonic (elements can be added to tn without effecting satisfiability)
     bool tn_is_monotonic = true;
-    if( tn.isSort() ){
+    if (tn.isUninterpretedSort())
+    {
       //TODO: use monotonicity inference
       tn_is_monotonic = !logicInfo().isQuantified();
-    }else{
+    }
+    else
+    {
       tn_is_monotonic = tn.getCardinality().isInfinite();
     }
     //add a reference type for maximum occurrences of empty in a constraint

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 3c4cf6487bb87dea09c62eb92ff5294fdcd85f38..b4c0c07c70bb62d367d3b6d221701014c95dbafd 100644 (file)
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -381,7 +381,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
         //apply sort inference to quantified variables
         for( size_t i=0; i<n[0].getNumChildren(); i++ ){
           TypeNode nitn = n[0][i].getType();
-          if( !nitn.isSort() )
+          if (!nitn.isUninterpretedSort())
           {
             // If the variable is of an interpreted sort, we assume the
             // the sort of the variable will stay the same sort.
@@ -574,7 +574,7 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
     // to be rewritten in the sort-inferred signature. Notice we only assign
     // pref here if it is an uninterpreted sort.
     if (!pref.isNull() && d_id_for_types.find(pref) == d_id_for_types.end()
-        && pref.isSort())
+        && pref.isUninterpretedSort())
     {
       retType = pref;
     }else{
@@ -875,7 +875,7 @@ bool SortInference::isWellSorted( Node n ) {
 }
 
 bool SortInference::isMonotonic( TypeNode tn ) {
-  Assert(tn.isSort());
+  Assert(tn.isUninterpretedSort());
   return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
 }
 

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 453b323d82a0a8f5208f53b8083043f6d7311e7e..c434a8e9138566e1063d51f3ea4103331816fb1d 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -111,7 +111,7 @@ bool TheoryModel::getHeapModel(Node& h, Node& neq) const
 std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
 {
   // must be an uninterpreted sort
-  Assert(tn.isSort());
+  Assert(tn.isUninterpretedSort());
   std::vector<Node> elements;
   const std::vector<Node>* type_refs = d_rep_set.getTypeRepsOrNull(tn);
   if (type_refs == nullptr || type_refs->empty())
@@ -171,7 +171,7 @@ bool TheoryModel::isModelCoreSymbol(Node s) const
 Cardinality TheoryModel::getCardinality(TypeNode tn) const
 {
   //for now, we only handle cardinalities for uninterpreted sorts
-  if (!tn.isSort())
+  if (!tn.isUninterpretedSort())
   {
     Trace("model-getvalue-debug")
         << "Get cardinality other sort, unknown." << std::endl;

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 6938f7bf063283314f2d75a204daf1864e3fd7e2..942374a47742d0ec959a1c3ed666d668030811ac 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -282,7 +282,7 @@ bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, Node r)
 
 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const
 {
-  if (tn.isSort())
+  if (tn.isUninterpretedSort())
   {
     return true;
   }
@@ -316,7 +316,7 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue(
   {
     visited[v] = true;
     TypeNode tn = v.getType();
-    if (tn.isSort())
+    if (tn.isUninterpretedSort())
     {
       Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
                                    << tn << std::endl;
@@ -608,7 +608,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
     // count the number of equivalence classes of sorts in finite model finding
     if (options().quantifiers.finiteModelFind)
     {
-      if (eqct.isSort())
+      if (eqct.isUninterpretedSort())
       {
         eqc_usort_count[eqct]++;
       }
@@ -889,7 +889,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       bool isUSortFiniteRestricted = false;
       if (options().quantifiers.finiteModelFind)
       {
-        isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
+        isUSortFiniteRestricted = !t.isUninterpretedSort() && involvesUSort(t);
       }
 #endif
 
@@ -960,7 +960,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             n = itAssigner->second.getNextAssignment();
             Assert(!n.isNull());
           }
-          else if (t.isSort() || !d_env.isFiniteType(t))
+          else if (t.isUninterpretedSort() || !d_env.isFiniteType(t))
           {
             // If its interpreted as infinite, we get a fresh value that does
             // not occur in the model.

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 8c75a407d25849d61e9f32bdacb9ff4ff5de772f..b193adfdeef6a4a3204dde7c218f55a0305b5004 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1346,7 +1346,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
       const CardinalityConstraint& cc =
           lit.getOperator().getConst<CardinalityConstraint>();
       TypeNode tn = cc.getType();
-      Assert(tn.isSort());
+      Assert(tn.isUninterpretedSort());
       Assert(d_rep_model[tn]);
       uint32_t nCard = cc.getUpperBound().getUnsignedInt();
       Trace("uf-ss-debug") << "...check cardinality constraint : " << tn
@@ -1525,7 +1525,8 @@ void CardinalityExtension::check(Theory::Effort level)
         while( !eqcs_i.isFinished() ){
           Node a = *eqcs_i;
           TypeNode tn = a.getType();
-          if( tn.isSort() ){
+          if (tn.isUninterpretedSort())
+          {
             if( type_proc.find( tn )==type_proc.end() ){
               std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn );
               if( itel!=eqc_list.end() ){
@@ -1610,7 +1611,7 @@ void CardinalityExtension::preRegisterTerm(TNode n)
   {
     tn = n.getType();
   }
-  if (!tn.isSort())
+  if (!tn.isUninterpretedSort())
   {
     return;
   }
@@ -1618,7 +1619,7 @@ void CardinalityExtension::preRegisterTerm(TNode n)
   if (it == d_rep_model.end())
   {
     SortModel* rm = nullptr;
-    if (tn.isSort())
+    if (tn.isUninterpretedSort())
     {
       Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
       rm = new SortModel(d_env, tn, d_state, d_im, this);

diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp
index 7f15f1c5752f420934c3eddce7ed98fa80ebd4e6..bdea5057ac2ed03bf1b40af1ce476a9aa32e103c 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.cpp
+++ b/src/theory/uf/theory_uf_type_rules.cpp
@@ -73,7 +73,7 @@ TypeNode CardinalityConstraintOpTypeRule::computeType(NodeManager* nodeManager,
   if (check)
   {
     const CardinalityConstraint& cc = n.getConst<CardinalityConstraint>();
-    if (!cc.getType().isSort())
+    if (!cc.getType().isUninterpretedSort())
     {
       throw TypeCheckingExceptionPrivate(
           n, "cardinality constraint must apply to uninterpreted sort");

diff --git a/src/util/uninterpreted_sort_value.cpp b/src/util/uninterpreted_sort_value.cpp
index b2fde93f33067295c6761dd825f6fd9aae230c92..4a1c86f415f2e1803c8b2e6d6aa400a2785a0e7b 100644 (file)
--- a/src/util/uninterpreted_sort_value.cpp
+++ b/src/util/uninterpreted_sort_value.cpp
@@ -35,7 +35,7 @@ UninterpretedSortValue::UninterpretedSortValue(const TypeNode& type,
                                                const Integer& index)
     : d_type(new TypeNode(type)), d_index(index)
 {
-  PrettyCheckArgument(type.isSort(),
+  PrettyCheckArgument(type.isUninterpretedSort(),
                       type,
                       "uninterpreted constants can only be created for "
                       "uninterpreted sorts, not `%s'",

diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index 0eb03ca42bd5b03de67084001005ce3913189151..cfdffe116164868b5102d80169a4694ca1c8a243 100644 (file)
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -162,7 +162,7 @@ TEST_F(TestNodeBlackNodeManager, booleanType)
   ASSERT_FALSE(t.isFunction());
   ASSERT_FALSE(t.isNull());
   ASSERT_FALSE(t.isPredicate());
-  ASSERT_FALSE(t.isSort());
+  ASSERT_FALSE(t.isUninterpretedSort());
   ASSERT_EQ(t, t2);
   ASSERT_NE(t, t3);
 
@@ -180,7 +180,7 @@ TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
   ASSERT_TRUE(t.isFunction());
   ASSERT_FALSE(t.isNull());
   ASSERT_TRUE(t.isPredicate());
-  ASSERT_FALSE(t.isSort());
+  ASSERT_FALSE(t.isUninterpretedSort());
 
   ASSERT_EQ(t, t2);
 
@@ -208,7 +208,7 @@ TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
   ASSERT_TRUE(t.isFunction());
   ASSERT_FALSE(t.isNull());
   ASSERT_FALSE(t.isPredicate());
-  ASSERT_FALSE(t.isSort());
+  ASSERT_FALSE(t.isUninterpretedSort());
 
   ASSERT_EQ(t, t2);
 
@@ -238,7 +238,7 @@ TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
   ASSERT_TRUE(t.isFunction());
   ASSERT_FALSE(t.isNull());
   ASSERT_FALSE(t.isPredicate());
-  ASSERT_FALSE(t.isSort());
+  ASSERT_FALSE(t.isUninterpretedSort());
 
   ASSERT_EQ(t, t2);
 
@@ -269,7 +269,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType)
   ASSERT_TRUE(t.isFunction());
   ASSERT_FALSE(t.isNull());
   ASSERT_TRUE(t.isPredicate());
-  ASSERT_FALSE(t.isSort());
+  ASSERT_FALSE(t.isUninterpretedSort());
 
   ASSERT_EQ(t, t2);