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.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6a045797a139089d2268279c4bd3db4add51bb63..e1f8031da6653dbe9b8a0846a673d8d09f080fea 100644 (file)
--- 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 a7033b2776f5de286938c84e8921b7f5ccb596ad..7b7e9dd82a2bf5d7098c09da6584de8b190b594f 100644 (file)
--- 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 8153d68568e8fc7d098606c3c4cfd6157ce2f35c..07422cd8b0a9bcbd3785d522c0127f5304602af8 100644 (file)
--- 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 2dc20cc3192524b3df75562acb980aeb035a78d5..6f40d815f4d6039f52671cab71c9324e191e6a05 100644 (file)
--- 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
 }