Convert symbol table from Expr-level to Term-level (#5355)

This task is left over from parser migration.

This PR also drops support for a case of symbol overloading, in particular symbols (constructors, selectors) for parametric datatypes cannot be overloaded. One regression is disabled as a result.

2 files changed, 10 insertions, 15 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index e58172b92..e815d9024 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -82,7 +82,7 @@ api::Term Parser::getSymbol(const std::string& name, SymbolType type)
   assert(isDeclared(name, type));
   assert(type == SYM_VARIABLE);
   // Functions share var namespace
-  return api::Term(d_solver, d_symtab->lookup(name));
+  return d_symtab->lookup(name);
 }
 
 api::Term Parser::getVariable(const std::string& name)
@@ -159,7 +159,7 @@ api::Sort Parser::getSort(const std::string& name)
 {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   assert(isDeclared(name, SYM_SORT));
-  api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name));
+  api::Sort t = d_symtab->lookupType(name);
   return t;
 }
 
@@ -168,8 +168,7 @@ api::Sort Parser::getSort(const std::string& name,
 {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   assert(isDeclared(name, SYM_SORT));
-  api::Sort t = api::Sort(
-      d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params)));
+  api::Sort t = d_symtab->lookupType(name, params);
   return t;
 }
 
@@ -279,7 +278,7 @@ void Parser::defineVar(const std::string& name,
                        bool doOverload)
 {
   Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
-  if (!d_symtab->bind(name, val.getExpr(), levelZero, doOverload))
+  if (!d_symtab->bind(name, val, levelZero, doOverload))
   {
     std::stringstream ss;
     ss << "Cannot bind " << name << " to symbol of type " << val.getSort();
@@ -296,10 +295,10 @@ void Parser::defineType(const std::string& name,
 {
   if (skipExisting && isDeclared(name, SYM_SORT))
   {
-    assert(api::Sort(d_solver, d_symtab->lookupType(name)) == type);
+    assert(d_symtab->lookupType(name) == type);
     return;
   }
-  d_symtab->bindType(name, type.getType(), levelZero);
+  d_symtab->bindType(name, type, levelZero);
   assert(isDeclared(name, SYM_SORT));
 }
 
@@ -308,8 +307,7 @@ void Parser::defineType(const std::string& name,
                         const api::Sort& type,
                         bool levelZero)
 {
-  d_symtab->bindType(
-      name, api::sortVectorToTypes(params), type.getType(), levelZero);
+  d_symtab->bindType(name, params, type, levelZero);
   assert(isDeclared(name, SYM_SORT));
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8e8080bc3..bfeafe78b 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -825,7 +825,7 @@ public:
   /** is this function overloaded? */
   bool isOverloadedFunction(api::Term fun)
   {
-    return d_symtab->isOverloadedFunction(fun.getExpr());
+    return d_symtab->isOverloadedFunction(fun);
   }
 
   /** Get overloaded constant for type.
@@ -834,8 +834,7 @@ public:
   */
   api::Term getOverloadedConstantForType(const std::string& name, api::Sort t)
   {
-    return api::Term(d_solver,
-                     d_symtab->getOverloadedConstantForType(name, t.getType()));
+    return d_symtab->getOverloadedConstantForType(name, t);
   }
 
   /**
@@ -846,9 +845,7 @@ public:
   api::Term getOverloadedFunctionForTypes(const std::string& name,
                                           std::vector<api::Sort>& argTypes)
   {
-    return api::Term(d_solver,
-                     d_symtab->getOverloadedFunctionForTypes(
-                         name, api::sortVectorToTypes(argTypes)));
+    return d_symtab->getOverloadedFunctionForTypes(name, argTypes);
   }
   //------------------------ end operator overloading
   /**