Modify the smt2 parser to use the Sygus grammar. (#4829)

3 files changed, 66 insertions, 231 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b88dc70b6..354f2d472 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -549,7 +549,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
   std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
   std::string name, fun;
   bool isInv;
-  CVC4::api::Sort grammar;
+  CVC4::api::Grammar* grammar = nullptr;
 }
   : /* declare-var */
     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -560,7 +560,6 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
       api::Term var = PARSER_STATE->bindBoundVar(name, t);
       cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
     }
-
   | /* synth-fun */
     ( SYNTH_FUN_TOK { isInv = false; }
       | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
@@ -618,23 +617,19 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
  * The argument fun is a unique identifier to avoid naming clashes for the
  * datatypes constructed by this call.
  */
-sygusGrammar[CVC4::api::Sort & ret,
+sygusGrammar[CVC4::api::Grammar*& ret,
              const std::vector<CVC4::api::Term>& sygusVars,
              const std::string& fun]
 @declarations
 {
   // the pre-declaration
-  std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
+  std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames;
   // non-terminal symbols of the grammar
   std::vector<CVC4::api::Term> ntSyms;
   CVC4::api::Sort t;
   std::string name;
   CVC4::api::Term e, e2;
-  std::vector<api::DatatypeDecl> datatypes;
-  std::set<api::Sort> unresTypes;
-  std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
   unsigned dtProcessed = 0;
-  std::unordered_set<unsigned> allowConst;
 }
   :
   // predeclaration
@@ -675,21 +670,13 @@ sygusGrammar[CVC4::api::Sort & ret,
     PARSER_STATE->pushScope(true);
     for (std::pair<std::string, api::Sort>& i : sortedVarNames)
     {
-      Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
-      // make the datatype, which encodes terms generated by this non-terminal
-      std::string dname = i.first;
-      datatypes.push_back(SOLVER->mkDatatypeDecl(dname));
-      // make its unresolved type, used for referencing the final version of
-      // the datatype
-      PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
-      api::Sort urt = PARSER_STATE->mkUnresolvedType(dname);
-      unresTypes.insert(urt);
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
       // make the non-terminal symbol, which will be parsed as an ordinary
       // free variable.
       api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
       ntSyms.push_back(nts);
-      ntsToUnres[nts] = urt;
     }
+    ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms);
   }
   // the grouped rule listing
   LPAREN_TOK
@@ -719,17 +706,15 @@ sygusGrammar[CVC4::api::Sort & ret,
     (
       term[e,e2] {
         // add term as constructor to datatype
-        PARSER_STATE->addSygusConstructorTerm(
-            datatypes[dtProcessed], e, ntsToUnres);
+        ret->addRule(ntSyms[dtProcessed], e);
       }
       | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
-        // allow constants in datatypes[dtProcessed]
-        allowConst.insert(dtProcessed);
+        // allow constants in datatype for ntSyms[dtProcessed]
+        ret->addAnyConstant(ntSyms[dtProcessed]);
       }
       | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
         // add variable constructors to datatype
-        PARSER_STATE->addSygusConstructorVariables(
-            datatypes[dtProcessed], sygusVars, t);
+        ret->addAnyVariable(ntSyms[dtProcessed]);
       }
     )+
     RPAREN_TOK
@@ -740,45 +725,8 @@ sygusGrammar[CVC4::api::Sort & ret,
   )+
   RPAREN_TOK
   {
-    if (dtProcessed != sortedVarNames.size())
-    {
-      PARSER_STATE->parseError(
-          "Number of grouped rule listings does not match "
-          "number of symbols in predeclaration.");
-    }
-    api::Term bvl;
-    if (!sygusVars.empty())
-    {
-      bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars);
-    }
-    Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl;
-    for (unsigned i = 0; i < dtProcessed; i++)
-    {
-      bool aci = allowConst.find(i)!=allowConst.end();
-      api::Sort btt = sortedVarNames[i].second;
-      datatypes[i].getDatatype().setSygus(btt.getType(), bvl.getExpr(), aci, false);
-      Trace("parser-sygus2") << "- " << datatypes[i].getName()
-                             << ", #cons= " << datatypes[i].getNumConstructors()
-                             << ", aci= " << aci << std::endl;
-      // We can be in a case where the only rule specified was (Variable T)
-      // and there are no variables of type T, in which case this is a bogus
-      // grammar. This results in the error below.
-      if (datatypes[i].getNumConstructors() == 0)
-      {
-        std::stringstream se;
-        se << "Grouped rule listing for " << datatypes[i].getName()
-           << " produced an empty rule list.";
-        PARSER_STATE->parseError(se.str());
-      }
-    }
     // pop scope from the pre-declaration
     PARSER_STATE->popScope();
-    // now, make the sygus datatype
-    Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
-    std::vector<api::Sort> datatypeTypes =
-      SOLVER->mkDatatypeSorts(datatypes, unresTypes);
-    // return is the first datatype
-    ret = api::Sort(datatypeTypes[0]);
   }
 ;
 
@@ -966,6 +914,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
   std::vector<api::Sort> sorts;
   std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
   std::unique_ptr<CVC4::CommandSequence> seq;
+  api::Grammar* g = nullptr;
 }
     /* Extended SMT-LIB set of commands syntax, not permitted in
      * --smtlib2 compliance mode. */
@@ -1131,10 +1080,10 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     term[e,e2]
     (
-      sygusGrammar[t, terms, name]
+      sygusGrammar[g, terms, name]
     )?
     {
-      cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
+      cmd->reset(new GetAbductCommand(SOLVER, name, e, g));
     }
   | GET_INTERPOL_TOK {
       PARSER_STATE->checkThatLogicIsSet();
@@ -1142,10 +1091,10 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     term[e,e2]
     (
-      sygusGrammar[t, terms, name]
+      sygusGrammar[g, terms, name]
     )?
     {
-      cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType()));
+      cmd->reset(new GetInterpolCommand(SOLVER, name, e, g));
     }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index eef23edfd..fa0f8af43 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -487,11 +487,11 @@ void Smt2::resetAssertions() {
 
 Smt2::SynthFunFactory::SynthFunFactory(
     Smt2* smt2,
-    const std::string& fun,
+    const std::string& id,
     bool isInv,
     api::Sort range,
     std::vector<std::pair<std::string, api::Sort>>& sortedVarNames)
-    : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
+    : d_smt2(smt2), d_id(id), d_sort(range), d_isInv(isInv)
 {
   if (range.isNull())
   {
@@ -501,37 +501,32 @@ Smt2::SynthFunFactory::SynthFunFactory(
   {
     smt2->parseError("Cannot use synth-fun with function return type.");
   }
+
   std::vector<api::Sort> varSorts;
   for (const std::pair<std::string, api::Sort>& p : sortedVarNames)
   {
     varSorts.push_back(p.second);
   }
-  Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
-  api::Sort synthFunType =
-      varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range)
-                          : range;
+
+  api::Sort funSort = varSorts.empty()
+                          ? range
+                          : d_smt2->d_solver->mkFunctionSort(varSorts, range);
 
   // we do not allow overloading for synth fun
-  d_synthFun = d_smt2->bindBoundVar(fun, synthFunType);
-  // set the sygus type to be range by default, which is overwritten below
-  // if a grammar is provided
-  d_sygusType = range;
+  d_fun = d_smt2->bindBoundVar(id, funSort);
+
+  Debug("parser-sygus") << "Define synth fun : " << id << std::endl;
 
   d_smt2->pushScope(true);
   d_sygusVars = d_smt2->bindBoundVars(sortedVarNames);
 }
 
-Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
-
-std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Sort grammar)
+std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar)
 {
-  Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
+  Debug("parser-sygus") << "...read synth fun " << d_id << std::endl;
+  d_smt2->popScope();
   return std::unique_ptr<Command>(new SynthFunCommand(
-      d_fun,
-      d_synthFun.getExpr(),
-      grammar.isNull() ? d_sygusType.getType() : grammar.getType(),
-      d_isInv,
-      api::termVectorToExprs(d_sygusVars)));
+      d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
 }
 
 std::unique_ptr<Command> Smt2::invConstraint(
@@ -762,6 +757,14 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
   return cmd;
 } /* Smt2::setLogic() */
 
+api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
+                              const std::vector<api::Term>& ntSymbols)
+{
+  d_allocGrammars.emplace_back(new api::Grammar(
+      std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols))));
+  return d_allocGrammars.back().get();
+}
+
 bool Smt2::sygus() const
 {
   InputLanguage ilang = getLanguage();
@@ -906,99 +909,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
   return d_solver->mkAbstractValue(name.substr(1));
 }
 
-
-void Smt2::addSygusConstructorTerm(
-    api::DatatypeDecl& dt,
-    api::Term term,
-    std::map<api::Term, api::Sort>& ntsToUnres) const
-{
-  Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
-  // At this point, we should know that dt is well founded, and that its
-  // builtin sygus operators are well-typed.
-  // Now, purify each occurrence of a non-terminal symbol in term, replace by
-  // free variables. These become arguments to constructors. Notice we must do
-  // a tree traversal in this function, since unique paths to the same term
-  // 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<api::Term> args;
-  std::vector<api::Sort> cargs;
-  api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs);
-  std::stringstream ssCName;
-  ssCName << op.getKind();
-  Trace("parser-sygus2") << "Purified operator " << op
-                         << ", #args/cargs=" << args.size() << "/"
-                         << cargs.size() << std::endl;
-  if (!args.empty())
-  {
-    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.getDatatype().addSygusConstructor(
-      op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs));
-}
-
-api::Term Smt2::purifySygusGTerm(api::Term term,
-                                 std::map<api::Term, api::Sort>& ntsToUnres,
-                                 std::vector<api::Term>& args,
-                                 std::vector<api::Sort>& cargs) const
-{
-  Trace("parser-sygus2-debug")
-      << "purifySygusGTerm: " << term
-      << " #nchild=" << term.getExpr().getNumChildren() << std::endl;
-  std::map<api::Term, api::Sort>::iterator itn = ntsToUnres.find(term);
-  if (itn != ntsToUnres.end())
-  {
-    api::Term ret = d_solver->mkVar(term.getSort());
-    Trace("parser-sygus2-debug")
-        << "...unresolved non-terminal, intro " << ret << std::endl;
-    args.push_back(api::Term(d_solver, ret.getExpr()));
-    cargs.push_back(itn->second);
-    return ret;
-  }
-  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;
-    api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
-    pchildren.push_back(ptermc);
-    childChanged = childChanged || ptermc != term[i];
-  }
-  if (!childChanged)
-  {
-    Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
-    return term;
-  }
-  api::Term nret = d_solver->mkTerm(term.getOp(), pchildren);
-  Trace("parser-sygus2-debug")
-      << "...child changed, return " << nret << std::endl;
-  return nret;
-}
-
-void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt,
-                                        const std::vector<api::Term>& sygusVars,
-                                        api::Sort type) const
-{
-  // each variable of appropriate type becomes a sygus constructor in dt.
-  for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
-  {
-    api::Term v = sygusVars[i];
-    if (v.getSort() == type)
-    {
-      std::stringstream ss;
-      ss << v;
-      std::vector<api::Sort> cargs;
-      dt.getDatatype().addSygusConstructor(
-          v.getExpr(), ss.str(), api::sortVectorToTypes(cargs));
-    }
-  }
-}
-
 InputLanguage Smt2::getLanguage() const
 {
   return d_solver->getOptions().getInputLanguage();
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 579fa90ce..2e725f9bf 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -60,6 +60,11 @@ class Smt2 : public Parser
    */
   std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
   std::pair<api::Term, std::string> d_lastNamedTerm;
+  /**
+   * A list of sygus grammar objects. We keep track of them here to ensure that
+   * they don't get deleted before the commands using them get invoked.
+   */
+  std::vector<std::unique_ptr<api::Grammar>> d_allocGrammars;
 
  protected:
   Smt2(api::Solver* solver,
@@ -198,7 +203,7 @@ class Smt2 : public Parser
      * Creates an instance of `SynthFunFactory`.
      *
      * @param smt2 Pointer to the parser state
-     * @param fun Name of the function to synthesize
+     * @param id Name of the function to synthesize
      * @param isInv True if the goal is to synthesize an invariant, false
      * otherwise
      * @param range The return type of the function-to-synthesize
@@ -206,11 +211,10 @@ class Smt2 : public Parser
      */
     SynthFunFactory(
         Smt2* smt2,
-        const std::string& fun,
+        const std::string& id,
         bool isInv,
         api::Sort range,
         std::vector<std::pair<std::string, api::Sort>>& sortedVarNames);
-    ~SynthFunFactory();
 
     const std::vector<api::Term>& getSygusVars() const { return d_sygusVars; }
 
@@ -220,13 +224,13 @@ class Smt2 : public Parser
      * @param grammar Optional grammar associated with the synth-fun command
      * @return The instance of `SynthFunCommand`
      */
-    std::unique_ptr<Command> mkCommand(api::Sort grammar);
+    std::unique_ptr<Command> mkCommand(api::Grammar* grammar);
 
    private:
     Smt2* d_smt2;
-    std::string d_fun;
-    api::Term d_synthFun;
-    api::Sort d_sygusType;
+    std::string d_id;
+    api::Term d_fun;
+    api::Sort d_sort;
     bool d_isInv;
     std::vector<api::Term> d_sygusVars;
   };
@@ -257,6 +261,15 @@ class Smt2 : public Parser
    */
   const LogicInfo& getLogic() const { return d_logic; }
 
+  /**
+   * Create a Sygus grammar.
+   * @param boundVars the parameters to corresponding synth-fun/synth-inv
+   * @param ntSymbols the pre-declaration of the non-terminal symbols
+   * @return a pointer to the grammar
+   */
+  api::Grammar* mkGrammar(const std::vector<api::Term>& boundVars,
+                          const std::vector<api::Term>& ntSymbols);
+
   bool v2_0() const
   {
     return getLanguage() == language::input::LANG_SMTLIB_V2_0;
@@ -308,10 +321,13 @@ class Smt2 : public Parser
    */
   void checkLogicAllowsFunctions();
 
-  void checkUserSymbol(const std::string& name) {
-    if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) {
+  void checkUserSymbol(const std::string& name)
+  {
+    if (name.length() > 0 && (name[0] == '.' || name[0] == '@'))
+    {
       std::stringstream ss;
-      ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB";
+      ss << "cannot declare or define symbol `" << name
+         << "'; symbols starting with . and @ are reserved in SMT-LIB";
       parseError(ss.str());
     }
     else if (isOperatorEnabled(name))
@@ -329,7 +345,8 @@ class Smt2 : public Parser
     d_lastNamedTerm = std::make_pair(e, name);
   }
 
-  void clearLastNamedTerm() {
+  void clearLastNamedTerm()
+  {
     d_lastNamedTerm = std::make_pair(api::Term(), "");
   }
 
@@ -346,31 +363,6 @@ class Smt2 : public Parser
   api::Term mkAbstractValue(const std::string& name);
 
   /**
-   * Adds a constructor to sygus datatype dt whose sygus operator is term.
-   *
-   * ntsToUnres contains a mapping from non-terminal symbols to the unresolved
-   * types they correspond to. This map indicates how the argument term should
-   * be interpreted (instances of symbols from the domain of ntsToUnres
-   * correspond to constructor arguments).
-   *
-   * The sygus operator that is actually added to dt corresponds to replacing
-   * each occurrence of non-terminal symbols from the domain of ntsToUnres
-   * with bound variables via purifySygusGTerm, and binding these variables
-   * via a lambda.
-   */
-  void addSygusConstructorTerm(
-      api::DatatypeDecl& dt,
-      api::Term term,
-      std::map<api::Term, api::Sort>& ntsToUnres) const;
-  /**
-   * This adds constructors to dt for sygus variables in sygusVars whose
-   * type is argument type. This method should be called when the sygus grammar
-   * term (Variable type) is encountered.
-   */
-  void addSygusConstructorVariables(api::DatatypeDecl& dt,
-                                    const std::vector<api::Term>& sygusVars,
-                                    api::Sort type) const;
-  /**
    * Smt2 parser provides its own checkDeclaration, which does the
    * same as the base, but with some more helpful errors.
    */
@@ -475,22 +467,6 @@ class Smt2 : public Parser
   //------------------------- end processing parse operators
  private:
 
-  /** Purify sygus grammar term
-   *
-   * This returns a term where all occurrences of non-terminal symbols (those
-   * in the domain of ntsToUnres) are replaced by fresh variables. For each
-   * variable replaced in this way, we add the fresh variable it is replaced
-   * with to args, and the unresolved type corresponding to the non-terminal
-   * symbol to cargs (constructor args). In other words, args contains the
-   * free variables in the term returned by this method (which should be bound
-   * by a lambda), and cargs contains the types of the arguments of the
-   * sygus constructor.
-   */
-  api::Term purifySygusGTerm(api::Term term,
-                             std::map<api::Term, api::Sort>& ntsToUnres,
-                             std::vector<api::Term>& args,
-                             std::vector<api::Sort>& cargs) const;
-
   void addArithmeticOperators();
 
   void addTranscendentalOperators();
@@ -519,7 +495,7 @@ class Smt2 : public Parser
   api::Term mkAnd(const std::vector<api::Term>& es);
 }; /* class Smt2 */
 
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+}  // namespace parser
+}  // namespace CVC4
 
 #endif /* CVC4__PARSER__SMT2_H */