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.

1 files changed, 7 insertions, 9 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));
 }