Sort term overload

src/parser/commands.cpp

@@ -1078,7 +1078,7 @@ void DeclareSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
   // determine if this will be a fresh declaration
   bool fresh = sm->getFreshDeclarations();
   Sort sort = solver->declareSort(d_symbol, d_arity, fresh);
-  sm->bindType(d_symbol, std::vector<Sort>(d_arity), sort);
+  sm->bindType(d_symbol, std::vector<Sort>(d_arity), sort, true);
   // mark that it will be printed in the model, if it is an uninterpreted
   // sort (arity 0)
   if (d_arity == 0)
@@ -1124,7 +1124,7 @@ cvc5::Sort DefineSortCommand::getSort() const { return d_sort; }
 void DefineSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
 {
   // This name is not its own distinct sort, it's an alias.
-  sm->bindType(d_symbol, d_params, d_sort);
+  sm->bindType(d_symbol, d_params, d_sort, true);
   d_commandStatus = CommandSuccess::instance();
 }
 

src/parser/parser_state.cpp

@@ -304,50 +304,31 @@ void ParserState::defineVar(const std::string& name,
 
 void ParserState::defineType(const std::string& name,
                              const Sort& type,
-                             bool skipExisting)
+                             bool isUser)
 {
-  if (skipExisting && isDeclared(name, SYM_SORT))
+  if (!isUser && isDeclared(name, SYM_SORT))
   {
     Assert(d_symtab->lookupType(name) == type);
     return;
   }
-  d_symtab->bindType(name, type);
+  d_symtab->bindType(name, type, isUser);
   Assert(isDeclared(name, SYM_SORT));
 }
 
 void ParserState::defineType(const std::string& name,
                              const std::vector<Sort>& params,
-                             const Sort& type)
+                             const Sort& type,
+                             bool isUser)
 {
-  d_symtab->bindType(name, params, type);
+  d_symtab->bindType(name, params, type, isUser);
   Assert(isDeclared(name, SYM_SORT));
 }
 
-void ParserState::defineParameterizedType(const std::string& name,
-                                          const std::vector<Sort>& params,
-                                          const Sort& type)
-{
-  if (TraceIsOn("parser"))
-  {
-    Trace("parser") << "defineParameterizedType(" << name << ", "
-                    << params.size() << ", [";
-    if (params.size() > 0)
-    {
-      copy(params.begin(),
-           params.end() - 1,
-           ostream_iterator<Sort>(Trace("parser"), ", "));
-      Trace("parser") << params.back();
-    }
-    Trace("parser") << "], " << type << ")" << std::endl;
-  }
-  defineType(name, params, type);
-}
-
 Sort ParserState::mkSort(const std::string& name)
 {
   Trace("parser") << "newSort(" << name << ")" << std::endl;
   Sort type = d_tm.mkUninterpretedSort(name);
-  defineType(name, type);
+  defineType(name, type, true);
   return type;
 }
 
@@ -356,22 +337,22 @@ Sort ParserState::mkSortConstructor(const std::string& name, size_t arity)
   Trace("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
   Sort type = d_tm.mkUninterpretedSortConstructorSort(arity, name);
-  defineType(name, vector<Sort>(arity), type);
+  defineType(name, vector<Sort>(arity), type, true);
   return type;
 }
 
 Sort ParserState::mkUnresolvedType(const std::string& name)
 {
   Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name);
-  defineType(name, unresolved);
+  defineType(name, unresolved, true);
   return unresolved;
 }
 
 Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name,
                                               size_t arity)
 {
   Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name, arity);
-  defineType(name, vector<Sort>(arity), unresolved);
+  defineType(name, vector<Sort>(arity), unresolved, true);
   return unresolved;
 }
 
@@ -381,7 +362,7 @@ Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name,
   Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
   Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name, params.size());
-  defineType(name, params, unresolved);
+  defineType(name, params, unresolved, true);
   Sort t = getParametricSort(name, params);
   return unresolved;
 }

src/parser/parser_state.h

@@ -286,30 +286,24 @@ class CVC5_EXPORT ParserState
    *
    * @param name The name of the type
    * @param type The type that should be associated with the name
-   * @param skipExisting If true, the type definition is ignored if the same
-   *                     symbol has already been defined. It is assumed that
-   *                     the definition is the exact same as the existing one.
+   * @param isUser does this correspond to a user sort
    */
   void defineType(const std::string& name,
                   const Sort& type,
-                  bool skipExisting = false);
+                  bool isUser);
 
   /**
    * Create a new (parameterized) type definition.
    *
    * @param name The name of the type
    * @param params The type parameters
    * @param type The type that should be associated with the name
+   * @param isUser does this correspond to a user sort
    */
   void defineType(const std::string& name,
                   const std::vector<Sort>& params,
-                  const Sort& type);
-
-  /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
-  void defineParameterizedType(const std::string& name,
-                               const std::vector<Sort>& params,
-                               const Sort& type);
-
+                  const Sort& type,
+                  bool isUser);
   /**
    * Creates a new sort with the given name.
    */

src/parser/smt2/smt2_state.cpp

@@ -296,10 +296,10 @@ void Smt2State::addSepOperators()
 
 void Smt2State::addCoreSymbols()
 {
-  defineType("Bool", d_tm.getBooleanSort(), true);
+  defineType("Bool", d_tm.getBooleanSort(), false);
   Sort tupleSort = d_tm.mkTupleSort({});
-  defineType("Relation", d_tm.mkSetSort(tupleSort), true);
-  defineType("Table", d_tm.mkBagSort(tupleSort), true);
+  defineType("Relation", d_tm.mkSetSort(tupleSort), false);
+  defineType("Table", d_tm.mkBagSort(tupleSort), false);
   defineVar("true", d_tm.mkTrue(), true);
   defineVar("false", d_tm.mkFalse(), true);
   addOperator(Kind::AND, "and");
@@ -799,7 +799,7 @@ void Smt2State::setLogic(std::string name)
   {
     if (d_logic.areIntegersUsed())
     {
-      defineType("Int", d_tm.getIntegerSort(), true);
+      defineType("Int", d_tm.getIntegerSort(), false);
       addArithmeticOperators();
       if (!strictModeEnabled() || !d_logic.isLinear())
       {
@@ -817,7 +817,7 @@ void Smt2State::setLogic(std::string name)
 
     if (d_logic.areRealsUsed())
     {
-      defineType("Real", d_tm.getRealSort(), true);
+      defineType("Real", d_tm.getRealSort(), false);
       addArithmeticOperators();
       addOperator(Kind::DIVISION, "/");
       if (!strictModeEnabled())
@@ -872,7 +872,7 @@ void Smt2State::setLogic(std::string name)
   if (d_logic.isTheoryEnabled(internal::theory::THEORY_DATATYPES))
   {
     const std::vector<Sort> types;
-    defineType("UnitTuple", d_tm.mkTupleSort(types), true);
+    defineType("UnitTuple", d_tm.mkTupleSort(types), false);
     addDatatypesOperators();
   }
 
@@ -956,9 +956,9 @@ void Smt2State::setLogic(std::string name)
   }
   if (d_logic.isTheoryEnabled(internal::theory::THEORY_STRINGS))
   {
-    defineType("String", d_tm.getStringSort(), true);
-    defineType("RegLan", d_tm.getRegExpSort(), true);
-    defineType("Int", d_tm.getIntegerSort(), true);
+    defineType("String", d_tm.getStringSort(), false);
+    defineType("RegLan", d_tm.getRegExpSort(), false);
+    defineType("Int", d_tm.getIntegerSort(), false);
 
     defineVar("re.none", d_tm.mkRegexpNone());
     defineVar("re.allchar", d_tm.mkRegexpAllchar());
@@ -976,11 +976,11 @@ void Smt2State::setLogic(std::string name)
 
   if (d_logic.isTheoryEnabled(internal::theory::THEORY_FP))
   {
-    defineType("RoundingMode", d_tm.getRoundingModeSort(), true);
-    defineType("Float16", d_tm.mkFloatingPointSort(5, 11), true);
-    defineType("Float32", d_tm.mkFloatingPointSort(8, 24), true);
-    defineType("Float64", d_tm.mkFloatingPointSort(11, 53), true);
-    defineType("Float128", d_tm.mkFloatingPointSort(15, 113), true);
+    defineType("RoundingMode", d_tm.getRoundingModeSort(), false);
+    defineType("Float16", d_tm.mkFloatingPointSort(5, 11), false);
+    defineType("Float32", d_tm.mkFloatingPointSort(8, 24), false);
+    defineType("Float64", d_tm.mkFloatingPointSort(11, 53), false);
+    defineType("Float128", d_tm.mkFloatingPointSort(15, 113), false);
 
     defineVar("RNE",
               d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN));

src/parser/sym_manager.cpp

@@ -332,9 +332,10 @@ bool SymManager::bind(const std::string& name, cvc5::Term obj, bool doOverload)
   return d_implementation->getSymbolTable().bind(name, obj, doOverload);
 }
 
-void SymManager::bindType(const std::string& name, cvc5::Sort t)
+void SymManager::bindType(const std::string& name, cvc5::Sort t,
+                bool isUser)
 {
-  return d_implementation->getSymbolTable().bindType(name, t);
+  return d_implementation->getSymbolTable().bindType(name, t, isUser);
 }
 
 bool SymManager::bindMutualDatatypeTypes(
@@ -349,11 +350,11 @@ bool SymManager::bindMutualDatatypeTypes(
     if (dt.isParametric())
     {
       std::vector<Sort> paramTypes = dt.getParameters();
-      bindType(name, paramTypes, t);
+      bindType(name, paramTypes, t, true);
     }
     else
     {
-      bindType(name, t);
+      bindType(name, t, true);
     }
     for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
     {
@@ -403,9 +404,10 @@ bool SymManager::bindMutualDatatypeTypes(
 
 void SymManager::bindType(const std::string& name,
                           const std::vector<cvc5::Sort>& params,
-                          cvc5::Sort t)
+                          cvc5::Sort t,
+                bool isUser)
 {
-  return d_implementation->getSymbolTable().bindType(name, params, t);
+  return d_implementation->getSymbolTable().bindType(name, params, t, isUser);
 }
 
 NamingResult SymManager::setExpressionName(cvc5::Term t,

src/parser/sym_manager.h

@@ -93,8 +93,10 @@ class CVC5_EXPORT SymManager
    *
    * @param name an identifier
    * @param t the type to bind to <code>name</code>
+   * @param isUser does this correspond to a user sort?
    */
-  void bindType(const std::string& name, cvc5::Sort t);
+  void bindType(const std::string& name, cvc5::Sort t,
+                bool isUser);
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -106,10 +108,12 @@ class CVC5_EXPORT SymManager
    * @param name an identifier
    * @param params the parameters to the type
    * @param t the type to bind to <code>name</code>
+   * @param isUser does this correspond to a user sort?
    */
   void bindType(const std::string& name,
                 const std::vector<cvc5::Sort>& params,
-                cvc5::Sort t);
+                cvc5::Sort t,
+                bool isUser);
   /**
    * Binds sorts of a list of mutually-recursive datatype declarations.
    *

src/parser/symbol_table.cpp

@@ -654,14 +654,14 @@ bool SymbolTable::bind(const string& name, Term obj, bool doOverload)
   return d_implementation->bind(name, obj, doOverload);
 }
 
-void SymbolTable::bindType(const string& name, Sort t)
+void SymbolTable::bindType(const string& name, Sort t, bool isUser)
 {
   d_implementation->bindType(name, t);
 }
 
 void SymbolTable::bindType(const string& name,
                            const vector<Sort>& params,
-                           Sort t)
+                           Sort t, bool isUser)
 {
   d_implementation->bindType(name, params, t);
 }

src/parser/symbol_table.h

@@ -82,8 +82,10 @@ class CVC5_EXPORT SymbolTable
    *
    * @param name an identifier
    * @param t the type to bind to <code>name</code>
+   * @param isUser does this correspond to a user sort
    */
-  void bindType(const std::string& name, cvc5::Sort t);
+  void bindType(const std::string& name, cvc5::Sort t,
+                bool isUser);
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -95,10 +97,12 @@ class CVC5_EXPORT SymbolTable
    * @param name an identifier
    * @param params the parameters to the type
    * @param t the type to bind to <code>name</code>
+   * @param isUser does this correspond to a user sort
    */
   void bindType(const std::string& name,
                 const std::vector<cvc5::Sort>& params,
-                cvc5::Sort t);
+                cvc5::Sort t,
+                bool isUser);
 
   /**
    * Check whether a name is bound to an expression with bind().