Update purifySygusGTerm to the new API (#3830)

Towards parser migration.

(Partially) updates the central function used for synth-fun in sygus v2 to the new API.

It also removes an optimization for "pure operators" from the v2 parser that is incompatible with the new API.

2 files changed, 31 insertions, 59 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ff155d0f9..48c1c96c7 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1460,83 +1460,55 @@ void Smt2::addSygusConstructorTerm(Datatype& dt,
   // should be treated as distinct terms.
   // Notice that let expressions are forbidden in the input syntax of term, so
   // this does not lead to exponential behavior with respect to input size.
-  std::vector<Expr> args;
-  std::vector<Type> cargs;
-  Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs);
+  std::vector<api::Term> args;
+  std::vector<api::Sort> cargs;
+  api::Term op = purifySygusGTerm(api::Term(term), ntsToUnres, args, cargs);
+  std::stringstream ssCName;
+  ssCName << op.getKind();
   Trace("parser-sygus2") << "Purified operator " << op
                          << ", #args/cargs=" << args.size() << "/"
                          << cargs.size() << std::endl;
   std::shared_ptr<SygusPrintCallback> spc;
   // callback prints as the expression
-  spc = std::make_shared<printer::SygusExprPrintCallback>(op, args);
+  spc = std::make_shared<printer::SygusExprPrintCallback>(
+      op.getExpr(), api::termVectorToExprs(args));
   if (!args.empty())
   {
-    bool pureVar = false;
-    if (op.getNumChildren() == args.size())
-    {
-      pureVar = true;
-      for (unsigned i = 0, nchild = op.getNumChildren(); i < nchild; i++)
-      {
-        if (op[i] != args[i])
-        {
-          pureVar = false;
-          break;
-        }
-      }
-    }
-    Trace("parser-sygus2") << "Pure var is " << pureVar
-                           << ", hasOp=" << op.hasOperator() << std::endl;
-    if (pureVar && op.hasOperator())
-    {
-      // optimization: use just the operator if it an application to only vars
-      op = op.getOperator();
-    }
-    else
-    {
-      Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args);
-      // its operator is a lambda
-      op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op);
-    }
-  }
-  Trace("parser-sygus2") << "Generated operator " << op << std::endl;
-  std::stringstream ss;
-  ss << op.getKind();
-  dt.addSygusConstructor(op, ss.str(), cargs, spc);
+    api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args);
+    // its operator is a lambda
+    op = d_solver->mkTerm(api::LAMBDA, lbvl, op);
+  }
+  Trace("parser-sygus2") << "addSygusConstructor:  operator " << op
+                         << std::endl;
+  dt.addSygusConstructor(
+      op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc);
 }
 
-Expr Smt2::purifySygusGTerm(Expr term,
-                            std::map<Expr, Type>& ntsToUnres,
-                            std::vector<Expr>& args,
-                            std::vector<Type>& cargs) const
+api::Term Smt2::purifySygusGTerm(api::Term term,
+                                 std::map<Expr, Type>& ntsToUnres,
+                                 std::vector<api::Term>& args,
+                                 std::vector<api::Sort>& cargs) const
 {
   Trace("parser-sygus2-debug")
-      << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren()
-      << std::endl;
-  std::map<Expr, Type>::iterator itn = ntsToUnres.find(term);
+      << "purifySygusGTerm: " << term
+      << " #nchild=" << term.getExpr().getNumChildren() << std::endl;
+  std::map<Expr, Type>::iterator itn = ntsToUnres.find(term.getExpr());
   if (itn != ntsToUnres.end())
   {
-    Expr ret = getExprManager()->mkBoundVar(term.getType());
+    api::Term ret = d_solver->mkVar(term.getSort());
     Trace("parser-sygus2-debug")
         << "...unresolved non-terminal, intro " << ret << std::endl;
-    args.push_back(ret);
+    args.push_back(ret.getExpr());
     cargs.push_back(itn->second);
     return ret;
   }
-  std::vector<Expr> pchildren;
-  // To test whether the operator should be passed to mkExpr below, we check
-  // whether this term is parameterized. This includes APPLY_UF terms and BV
-  // extraction terms, but excludes applications of most interpreted symbols
-  // like PLUS.
-  if (term.isParameterized())
-  {
-    pchildren.push_back(term.getOperator());
-  }
+  std::vector<api::Term> pchildren;
   bool childChanged = false;
   for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
   {
     Trace("parser-sygus2-debug")
         << "......purify child " << i << " : " << term[i] << std::endl;
-    Expr ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
+    api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
     pchildren.push_back(ptermc);
     childChanged = childChanged || ptermc != term[i];
   }
@@ -1545,7 +1517,7 @@ Expr Smt2::purifySygusGTerm(Expr term,
     Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
     return term;
   }
-  Expr nret = getExprManager()->mkExpr(term.getKind(), pchildren);
+  api::Term nret = d_solver->mkTerm(term.getOp(), pchildren);
   Trace("parser-sygus2-debug")
       << "...child changed, return " << nret << std::endl;
   return nret;
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 35ac781f5..53ebf5929 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -602,10 +602,10 @@ class Smt2 : public Parser
    * by a lambda), and cargs contains the types of the arguments of the
    * sygus constructor.
    */
-  Expr purifySygusGTerm(Expr term,
-                        std::map<Expr, Type>& ntsToUnres,
-                        std::vector<Expr>& args,
-                        std::vector<Type>& cargs) const;
+  api::Term purifySygusGTerm(api::Term term,
+                             std::map<Expr, Type>& ntsToUnres,
+                             std::vector<api::Term>& args,
+                             std::vector<api::Sort>& cargs) const;
 
   void addArithmeticOperators();