Fix bugs related to printing Sygus commands (#3804)

With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.

4 files changed, 71 insertions, 86 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6a045797a..e1f8031da 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -673,17 +673,14 @@ sygusGrammarV1[CVC4::Type & ret,
   : LPAREN_TOK { PARSER_STATE->pushScope(); }
   (LPAREN_TOK
        symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] {
-         std::stringstream ss;
-         ss << fun << "_" << name;
          if (name == "Start")
          {
            startIndex = datatypes.size();
          }
-         std::string dname = ss.str();
          sgts.push_back(std::vector<CVC4::SygusGTerm>());
          sgts.back().push_back(CVC4::SygusGTerm());
          PARSER_STATE->pushSygusDatatypeDef(t,
-                                            dname,
+                                            name,
                                             datatypes,
                                             sorts,
                                             ops,
@@ -692,18 +689,18 @@ sygusGrammarV1[CVC4::Type & ret,
                                             allow_const,
                                             unresolved_gterm_sym);
          Type unres_t;
-         if (!PARSER_STATE->isUnresolvedType(dname))
+         if (!PARSER_STATE->isUnresolvedType(name))
          {
            // if not unresolved, must be undeclared
-           Debug("parser-sygus") << "Make unresolved type : " << dname
+           Debug("parser-sygus") << "Make unresolved type : " << name
                                  << std::endl;
-           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
-           unres_t = PARSER_STATE->mkUnresolvedType(dname);
+           PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
+           unres_t = PARSER_STATE->mkUnresolvedType(name);
          }
          else
          {
-           Debug("parser-sygus") << "Get sort : " << dname << std::endl;
-           unres_t = PARSER_STATE->getSort(dname);
+           Debug("parser-sygus") << "Get sort : " << name << std::endl;
+           unres_t = PARSER_STATE->getSort(name);
          }
          sygus_to_builtin[unres_t] = t;
          Debug("parser-sygus") << "--- Read sygus grammar " << name
@@ -899,10 +896,6 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
         sgt.d_name = name;
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }else{
-        //prepend function name to base sorts when reading an operator
-        std::stringstream ss;
-        ss << fun << "_" << name;
-        name = ss.str();
         if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
           Debug("parser-sygus") << "Sygus grammar " << fun
                                 << " : nested sort " << name << std::endl;
@@ -957,9 +950,7 @@ sygusGrammar[CVC4::Type & ret,
     {
       Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
       // make the datatype, which encodes terms generated by this non-terminal
-      std::stringstream ss;
-      ss << "dt_" << fun << "_" << i.first;
-      std::string dname = ss.str();
+      std::string dname = i.first;
       datatypes.push_back(Datatype(EXPR_MANAGER, dname));
       // make its unresolved type, used for referencing the final version of
       // the datatype
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a7033b277..7b7e9dd82 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -172,7 +172,8 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_PREFIX, "str.prefixof" );
   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
   // at the moment, we only use this syntax for smt2.6.1
-  if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+  if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
+      || getLanguage() == language::input::LANG_SYGUS_V2)
   {
     addOperator(kind::STRING_ITOS, "str.from_int");
     addOperator(kind::STRING_STOI, "str.to_int");
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8153d6856..07422cd8b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -128,6 +128,7 @@ void Smt2Printer::toStream(std::ostream& out,
       case REAL_TYPE: out << "Real"; break;
       case INTEGER_TYPE: out << "Int"; break;
       case STRING_TYPE: out << "String"; break;
+      case REGEXP_TYPE: out << "RegLan"; break;
       case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
       default:
         // fall back on whatever operator<< does on underlying type; we
@@ -1206,7 +1207,8 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_CHARAT: return "str.at" ;
   case kind::STRING_STRIDOF: return "str.indexof" ;
   case kind::STRING_STRREPL: return "str.replace" ;
-  case kind::STRING_STRREPLALL: return "str.replaceall";
+  case kind::STRING_STRREPLALL:
+    return v == smt2_6_1_variant ? "str.replace_all" : "str.replaceall";
   case kind::STRING_TOLOWER: return "str.tolower";
   case kind::STRING_TOUPPER: return "str.toupper";
   case kind::STRING_REV: return "str.rev";
@@ -1214,15 +1216,16 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_SUFFIX: return "str.suffixof" ;
   case kind::STRING_LEQ: return "str.<=";
   case kind::STRING_LT: return "str.<";
-  case kind::STRING_CODE: return "str.code";
+  case kind::STRING_CODE:
+    return v == smt2_6_1_variant ? "str.to_code" : "str.code";
   case kind::STRING_ITOS:
-    return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
+    return v == smt2_6_1_variant ? "str.from_int" : "int.to.str";
   case kind::STRING_STOI:
-    return v == smt2_6_1_variant ? "str.to-int" : "str.to.int";
+    return v == smt2_6_1_variant ? "str.to_int" : "str.to.int";
   case kind::STRING_IN_REGEXP:
-    return v == smt2_6_1_variant ? "str.in-re" : "str.in.re";
+    return v == smt2_6_1_variant ? "str.in_re" : "str.in.re";
   case kind::STRING_TO_REGEXP:
-    return v == smt2_6_1_variant ? "str.to-re" : "str.to.re";
+    return v == smt2_6_1_variant ? "str.to_re" : "str.to.re";
   case kind::REGEXP_EMPTY: return "re.nostr";
   case kind::REGEXP_SIGMA: return "re.allchar";
   case kind::REGEXP_CONCAT: return "re.++";
@@ -2071,25 +2074,23 @@ static void toStream(std::ostream& out, const SynthFunCommand* c)
   Type type = c->getFunction().getType();
   const std::vector<Expr>& vars = c->getVars();
   Assert(!type.isFunction() || !vars.empty());
-  c->getCommandName();
+  out << '(';
   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() << ')';
+    ++i;
+    while (i != i_end)
     {
-      out << '(' << *i << ' ' << (*i).getType() << ')';
-      if (++i != i_end)
-      {
-        out << ' ';
-      }
-    } while (i != i_end);
-    out << ')';
+      out << " (" << *i << ' ' << i->getType() << ')';
+      ++i;
+    }
     FunctionType ft = type;
     type = ft.getRangeType();
   }
+  out << ')';
   // if not invariant-to-synthesize, print return type
   if (!c->isInv())
   {
@@ -2105,6 +2106,7 @@ static void toStream(std::ostream& out, const SynthFunCommand* c)
     std::list<Type> typesToPrint;
     grammarTypes.insert(sygusType);
     typesToPrint.push_back(sygusType);
+    NodeManager* nm = NodeManager::currentNM();
     // for each datatype in grammar
     //   name
     //   sygus type
@@ -2118,61 +2120,41 @@ static void toStream(std::ostream& out, const SynthFunCommand* c)
       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() << ")";
+      types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " (";
+      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)
+        // make a sygus term
+        std::vector<Node> cchildren;
+        cchildren.push_back(Node::fromExpr(cons.getConstructor()));
+        for (const DatatypeConstructorArg& i : cons)
         {
-          types_list << "(";
-          SygusPrintCallback* spc = cons.getSygusPrintCallback().get();
-          if (spc != nullptr && options::sygusPrintCallbacks())
+          Type argType = i.getRangeType();
+          std::stringstream ss;
+          ss << argType;
+          Node bv = nm->mkBoundVar(ss.str(), TypeNode::fromType(argType));
+          cchildren.push_back(bv);
+          // if fresh type, store it for later processing
+          if (grammarTypes.insert(argType).second)
           {
-            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();
+            typesToPrint.push_back(argType);
           }
         }
-        types_list << "\n";
+        Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren);
+        // now, print it
+        sygus_printer->toStreamSygus(types_list, consToPrint);
+        types_list << ' ';
       }
       types_list << "))\n";
     } while (!typesToPrint.empty());
 
-    out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ")";
+    out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ')';
   }
-  out << ")";
+  out << ')';
 }
 
 static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2dc20cc31..6f40d815f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -963,16 +963,18 @@ void SmtEngine::finishInit()
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
-  // dump out a set-logic command
-  if(Dump.isOn("benchmark")) {
-    if (Dump.isOn("raw-benchmark")) {
-      Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic.getLogicString());
-    } else {
+  // dump out a set-logic command only when raw-benchmark is disabled to avoid
+  // dumping the command twice.
+  if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark"))
+  {
       LogicInfo everything;
       everything.lock();
-      Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.")
-                        << SetBenchmarkLogicCommand(everything.getLogicString());
-    }
+      Dump("benchmark") << CommentCommand(
+          "CVC4 always dumps the most general, all-supported logic (below), as "
+          "some internals might require the use of a logic more general than "
+          "the input.")
+                        << SetBenchmarkLogicCommand(
+                               everything.getLogicString());
   }
 
   Trace("smt-debug") << "Dump declaration commands..." << std::endl;
@@ -1128,9 +1130,18 @@ void SmtEngine::setLogic(const LogicInfo& logic)
 void SmtEngine::setLogic(const std::string& s)
 {
   SmtScope smts(this);
-  try {
+  try
+  {
     setLogic(LogicInfo(s));
-  } catch(IllegalArgumentException& e) {
+    // dump out a set-logic command
+    if (Dump.isOn("raw-benchmark"))
+    {
+      Dump("raw-benchmark")
+          << SetBenchmarkLogicCommand(d_logic.getLogicString());
+    }
+  }
+  catch (IllegalArgumentException& e)
+  {
     throw LogicException(e.what());
   }
 }
@@ -3937,7 +3948,6 @@ 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
 }
 
@@ -3947,7 +3957,8 @@ 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);
+  Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
+
   // don't need to set that the conjecture is stale
 }