Support dumping Sygus commands. (#3763)

5 files changed, 215 insertions, 31 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index af193c04b..681b2a1c9 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -368,10 +368,11 @@ bool Parser::isUnresolvedType(const std::string& name) {
 }
 
 std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
-    std::vector<Datatype>& datatypes, bool doOverload) {
+    std::vector<Datatype>& datatypes, bool doOverload, uint32_t flags)
+{
   try {
     std::vector<DatatypeType> types =
-        getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved);
+        getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved, flags);
 
     assert(datatypes.size() == types.size());
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b0ef2328f..2317835ff 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -602,9 +602,15 @@ public:
    * For each symbol defined by the datatype, if a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
    *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   *
+   * flags specify information about the datatype, e.g. whether it should be
+   * printed out as a definition in models or not
+   *   (see enum in expr_manager_template.h).
    */
-  std::vector<DatatypeType>
-  mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, bool doOverload=false);
+  std::vector<DatatypeType> mkMutualDatatypeTypes(
+      std::vector<Datatype>& datatypes,
+      bool doOverload = false,
+      uint32_t flags = ExprManager::DATATYPE_FLAG_NONE);
 
   /** make flat function type
    *
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 90303dd40..3a6b444cc 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -784,7 +784,8 @@ sygusGrammarV1[CVC4::Type & ret,
                             << std::endl;
     }
     std::vector<DatatypeType> datatypeTypes =
-        PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+        PARSER_STATE->mkMutualDatatypeTypes(
+            datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
     ret = datatypeTypes[0];
   };
 
@@ -1068,7 +1069,8 @@ sygusGrammar[CVC4::Type & ret,
     // now, make the sygus datatype
     Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
     std::vector<DatatypeType> datatypeTypes =
-        PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+        PARSER_STATE->mkMutualDatatypeTypes(
+            datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
     // return is the first datatype
     ret = datatypeTypes[0];
   }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 806569b08..bfdaf7852 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1269,8 +1269,7 @@ void Smt2Printer::toStream(std::ostream& out,
   expr::ExprDag::Scope dagScope(out, dag);
 
   if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
-      || tryToStream<PopCommand>(out, c)
-      || tryToStream<CheckSatCommand>(out, c)
+      || tryToStream<PopCommand>(out, c) || tryToStream<CheckSatCommand>(out, c)
       || tryToStream<CheckSatAssumingCommand>(out, c)
       || tryToStream<QueryCommand>(out, c, d_variant)
       || tryToStream<ResetCommand>(out, c)
@@ -1301,7 +1300,14 @@ void Smt2Printer::toStream(std::ostream& out,
       || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
       || tryToStream<CommentCommand>(out, c, d_variant)
       || tryToStream<EmptyCommand>(out, c)
-      || tryToStream<EchoCommand>(out, c, d_variant))
+      || tryToStream<EchoCommand>(out, c, d_variant)
+      || tryToStream<SynthFunCommand>(out, c)
+      || tryToStream<DeclareSygusPrimedVarCommand>(out, c)
+      || tryToStream<DeclareSygusFunctionCommand>(out, c)
+      || tryToStream<DeclareSygusVarCommand>(out, c)
+      || tryToStream<SygusConstraintCommand>(out, c)
+      || tryToStream<SygusInvConstraintCommand>(out, c)
+      || tryToStream<CheckSynthCommand>(out, c))
   {
     return;
   }
@@ -2057,6 +2063,178 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
   out << "(echo \"" << s << "\")";
 }
 
+/*
+   --------------------------------------------------------------------------
+    Handling SyGuS commands
+   --------------------------------------------------------------------------
+*/
+
+static void toStream(std::ostream& out, const SynthFunCommand* c)
+{
+  out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
+      << ' ';
+  Type type = c->getFunction().getType();
+  const std::vector<Expr>& vars = c->getVars();
+  Assert(!type.isFunction() || !vars.empty());
+  c->getCommandName();
+  if (type.isFunction())
+  {
+    // print variable list
+    std::vector<Expr>::const_iterator i = vars.begin(), i_end = vars.end();
+    Assert(i != i_end);
+    out << '(';
+    do
+    {
+      out << '(' << *i << ' ' << (*i).getType() << ')';
+      if (++i != i_end)
+      {
+        out << ' ';
+      }
+    } while (i != i_end);
+    out << ')';
+    FunctionType ft = type;
+    type = ft.getRangeType();
+  }
+  // if not invariant-to-synthesize, print return type
+  if (!c->isInv())
+  {
+    out << ' ' << type;
+  }
+  // print grammar, if any
+  Type sygusType = c->getSygusType();
+  if (sygusType.isDatatype()
+      && static_cast<DatatypeType>(sygusType).getDatatype().isSygus())
+  {
+    std::stringstream types_predecl, types_list;
+    std::set<Type> grammarTypes;
+    std::list<Type> typesToPrint;
+    grammarTypes.insert(sygusType);
+    typesToPrint.push_back(sygusType);
+    // for each datatype in grammar
+    //   name
+    //   sygus type
+    //   constructors in order
+    Printer* sygus_printer =
+        Printer::getPrinter(language::output::LANG_SYGUS_V2);
+    do
+    {
+      Type curr = typesToPrint.front();
+      typesToPrint.pop_front();
+      Assert(curr.isDatatype()
+             && static_cast<DatatypeType>(curr).getDatatype().isSygus());
+      const Datatype& dt = static_cast<DatatypeType>(curr).getDatatype();
+      types_list << "(" << dt.getName() << " " << dt.getSygusType() << "\n(";
+      types_predecl << "(" << dt.getName() << " " << dt.getSygusType() << ")";
+      if (dt.getSygusAllowConst())
+      {
+        types_list << "(Constant " << dt.getSygusType() << ") ";
+      }
+      for (const DatatypeConstructor& cons : dt)
+      {
+        DatatypeConstructor::const_iterator i = cons.begin(),
+                                            i_end = cons.end();
+        if (i != i_end)
+        {
+          types_list << "(";
+          SygusPrintCallback* spc = cons.getSygusPrintCallback().get();
+          if (spc != nullptr && options::sygusPrintCallbacks())
+          {
+            spc->toStreamSygus(sygus_printer, types_list, cons.getSygusOp());
+          }
+          else
+          {
+            types_list << cons.getSygusOp();
+          }
+          do
+          {
+            Type argType = (*i).getRangeType();
+            // print argument type
+            types_list << " " << argType;
+            // if fresh type, store it for later processing
+            if (grammarTypes.insert(argType).second)
+            {
+              typesToPrint.push_back(argType);
+            }
+          } while (++i != i_end);
+          types_list << ")";
+        }
+        else
+        {
+          SygusPrintCallback* spc = cons.getSygusPrintCallback().get();
+          if (spc != nullptr && options::sygusPrintCallbacks())
+          {
+            spc->toStreamSygus(sygus_printer, types_list, cons.getSygusOp());
+          }
+          else
+          {
+            types_list << cons.getSygusOp();
+          }
+        }
+        types_list << "\n";
+      }
+      types_list << "))\n";
+    } while (!typesToPrint.empty());
+
+    out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ")";
+  }
+  out << ")";
+}
+
+static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
+{
+  out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol());
+
+  FunctionType ft = c->getType();
+  stringstream ss;
+
+  for (const Type& i : ft.getArgTypes())
+  {
+    ss << i << ' ';
+  }
+
+  string argTypes = ss.str();
+  argTypes.pop_back();
+
+  out << " (" << argTypes << ") " << ft.getRangeType() << ')';
+}
+
+static void toStream(std::ostream& out, const DeclareSygusPrimedVarCommand* c)
+{
+  out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
+      << ' ' << c->getType() << ')';
+}
+
+static void toStream(std::ostream& out, const DeclareSygusVarCommand* c)
+{
+  out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType()
+      << ')';
+}
+
+static void toStream(std::ostream& out, const SygusConstraintCommand* c)
+{
+  out << '(' << c->getCommandName() << ' ' << c->getExpr() << ')';
+}
+
+static void toStream(std::ostream& out, const SygusInvConstraintCommand* c)
+{
+  out << '(' << c->getCommandName() << ' ';
+  copy(c->getPredicates().cbegin(),
+       c->getPredicates().cend(),
+       std::ostream_iterator<Expr>(out, " "));
+  out << ')';
+}
+
+static void toStream(std::ostream& out, const CheckSynthCommand* c)
+{
+  out << '(' << c->getCommandName() << ')';
+}
+
+/*
+   --------------------------------------------------------------------------
+    End of Handling SyGuS commands
+   --------------------------------------------------------------------------
+*/
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c)
 {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1d96fc207..f1d602bc6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3652,16 +3652,27 @@ void SmtEngine::ensureBoolean(const Expr& e)
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 {
+  Dump("benchmark") << CheckSatCommand(assumption);
   return checkSatisfiability(assumption, inUnsatCore, false);
 }
 
 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
 {
+  if (assumptions.empty())
+  {
+    Dump("benchmark") << CheckSatCommand();
+  }
+  else
+  {
+    Dump("benchmark") << CheckSatAssumingCommand(assumptions);
+  }
+
   return checkSatisfiability(assumptions, inUnsatCore, false);
 }
 
 Result SmtEngine::query(const Expr& assumption, bool inUnsatCore)
 {
+  Dump("benchmark") << QueryCommand(assumption, inUnsatCore);
   return checkSatisfiability(assumption.isNull()
                                  ? std::vector<Expr>()
                                  : std::vector<Expr>{assumption},
@@ -3789,25 +3800,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
 
     d_needPostsolve = true;
 
-    // Dump the query if requested
-    if (Dump.isOn("benchmark"))
-    {
-      size_t size = assumptions.size();
-      // the expr already got dumped out if assertion-dumping is on
-      if (isQuery && size == 1)
-      {
-        Dump("benchmark") << QueryCommand(assumptions[0]);
-      }
-      else if (size == 0)
-      {
-        Dump("benchmark") << CheckSatCommand();
-      }
-      else
-      {
-        Dump("benchmark") << CheckSatAssumingCommand(d_assumptions);
-      }
-    }
-
     // Pop the context
     if (didInternalPush)
     {
@@ -3936,6 +3928,7 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 {
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
+  Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
   // don't need to set that the conjecture is stale
 }
 
@@ -3943,6 +3936,7 @@ void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
 {
   // do nothing (the command is spurious)
   Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
+  Dump("raw-benchmark") << DeclareSygusPrimedVarCommand(id, type);
   // don't need to set that the conjecture is stale
 }
 
@@ -3952,6 +3946,7 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id,
 {
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
+  Dump("raw-benchmark") << DeclareSygusFunctionCommand(id, var, type);
   // don't need to set that the conjecture is stale
 }
 
@@ -3984,6 +3979,7 @@ void SmtEngine::declareSynthFun(const std::string& id,
     setUserAttribute("sygus-synth-grammar", func, attr_value, "");
   }
   Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
+  Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
   // sygus conjecture is now stale
   setSygusConjectureStale();
 }
@@ -3994,6 +3990,7 @@ void SmtEngine::assertSygusConstraint(Expr constraint)
   d_private->d_sygusConstraints.push_back(constraint);
 
   Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
+  Dump("raw-benchmark") << SygusConstraintCommand(constraint);
   // sygus conjecture is now stale
   setSygusConjectureStale();
 }
@@ -4065,6 +4062,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv,
   d_private->d_sygusConstraints.push_back(constraint);
 
   Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n";
+  Dump("raw-benchmark") << SygusInvConstraintCommand(inv, pre, trans, post);
   // sygus conjecture is now stale
   setSygusConjectureStale();
 }
@@ -4118,6 +4116,7 @@ Result SmtEngine::checkSynth()
     setUserAttribute("sygus", sygusVar.toExpr(), {}, "");
 
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
+    Dump("raw-benchmark") << CheckSynthCommand();
 
     d_private->d_sygusConjectureStale = false;
 
@@ -4195,9 +4194,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex)
     // Ensure expr is type-checked at this point.
     e.getType(true);
   }
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << ExpandDefinitionsCommand(e);
-  }
+
   unordered_map<Node, Node, NodeHashFunction> cache;
   Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
   n = postprocess(n, TypeNode::fromType(e.getType()));