Sygus print callbacks (#1348)

* Initial infrastructure for sygus printing.

* Minor

* Minor improvements

* Format

* Minor

* Empty constructor printer.

* Format

* Minor

* Format

* Address.

2 files changed, 64 insertions, 13 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8a80ba59e..6ceb79001 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -364,9 +364,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::CHAIN: break;
   case kind::FUNCTION_TYPE:
     out << "->";
-    for(size_t i = 0; i < n.getNumChildren(); ++i) {
+    for (Node nc : n)
+    {
       out << " ";
-      toStream(out, n[i], toDepth, types, TypeNode::null());
+      toStream(out, nc, toDepth, types, TypeNode::null());
     }
     out << ")";
     return;
@@ -382,11 +383,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
     // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
-    // higher-order
+  // higher-order
   case kind::HO_APPLY: break;
-  case kind::LAMBDA: out << smtKindString(k) << " "; break;
-  
-    // arith theory
+  case kind::LAMBDA:
+    out << smtKindString(k) << " ";
+    break;
+
+  // arith theory
   case kind::PLUS:
   case kind::MULT:
   case kind::NONLINEAR_MULT:
@@ -819,10 +822,11 @@ static string smtKindString(Kind k) throw() {
 
     // uf theory
   case kind::APPLY_UF: break;
-  
-  case kind::LAMBDA: return "lambda";
 
-    // arith theory
+  case kind::LAMBDA:
+    return "lambda";
+
+  // arith theory
   case kind::PLUS: return "+";
   case kind::MULT:
   case kind::NONLINEAR_MULT: return "*";
@@ -1310,6 +1314,47 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   }
 }
 
+void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
+{
+  if (n.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    TypeNode tn = n.getType();
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    if (dt.isSygus())
+    {
+      int cIndex = Datatype::indexOf(n.getOperator().toExpr());
+      Assert(!dt[cIndex].getSygusOp().isNull());
+      SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback();
+      if (spc != nullptr)
+      {
+        spc->toStreamSygus(this, out, n.toExpr());
+      }
+      else
+      {
+        if (n.getNumChildren() > 0)
+        {
+          out << "(";
+        }
+        out << dt[cIndex].getSygusOp();
+        if (n.getNumChildren() > 0)
+        {
+          for (Node nc : n)
+          {
+            out << " ";
+            toStreamSygus(out, nc);
+          }
+          out << ")";
+        }
+      }
+      return;
+    }
+  }
+  else
+  {
+    // cannot convert term to analog, print original
+    toStream(out, n, -1, false, 1);
+  }
+}
 
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "(assert " << c->getExpr() << ")";
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index b7e9e1f40..96f55d7a2 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -48,11 +48,17 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
   void toStream(std::ostream& out, const Model& m) const throw();
-  /** print the unsat core to the stream out.
-  * We use the expression names that are stored in the SMT engine associated 
-  * with the core (UnsatCore::getSmtEngine) for printing named assertions.
-  */
+  /**
+   * Writes the unsat core to the stream out.
+   * We use the expression names that are stored in the SMT engine associated
+   * with the core (UnsatCore::getSmtEngine) for printing named assertions.
+   */
   void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  /**
+   * Write the term that sygus datatype term node n
+   * encodes to a stream with this Printer.
+   */
+  virtual void toStreamSygus(std::ostream& out, TNode n) const throw() override;
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */