Simplify internal API for sygus (#5687)

This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 8044508c7e5ea6fa506ce1087fbf3b4a9203597f..b11a01628626bf61337b6621624256670cf4efa6 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -5615,7 +5615,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
   Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
 
-  d_smtEngine->declareSygusVar(symbol, res, *sort.d_type);
+  d_smtEngine->declareSygusVar(res);
 
   return Term(this, res);
 
@@ -5740,7 +5740,7 @@ Term Solver::synthFunHelper(const std::string& symbol,
   std::vector<Node> bvns = termVectorToNodes(boundVars);
 
   d_smtEngine->declareSynthFun(
-      symbol, fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns);
+      fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns);
 
   return Term(this, fun);
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 48ed0d5c9ed03e2fd354269265f6cc5615b96e40..4c47587a6fe3dae08dde157b3f51aebfac3d37bc 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1063,10 +1063,10 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
    --------------------------------------------------------------------------
 */
 
-void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type)
+void SmtEngine::declareSygusVar(Node var)
 {
   SmtScope smts(this);
-  d_sygusSolver->declareSygusVar(id, var, type);
+  d_sygusSolver->declareSygusVar(var);
   if (Dump.isOn("raw-benchmark"))
   {
     getOutputManager().getPrinter().toStreamCmdDeclareVar(
@@ -1075,15 +1075,14 @@ void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type)
   // don't need to set that the conjecture is stale
 }
 
-void SmtEngine::declareSynthFun(const std::string& id,
-                                Node func,
+void SmtEngine::declareSynthFun(Node func,
                                 TypeNode sygusType,
                                 bool isInv,
                                 const std::vector<Node>& vars)
 {
   SmtScope smts(this);
   d_state->doPendingPops();
-  d_sygusSolver->declareSynthFun(id, func, sygusType, isInv, vars);
+  d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
 
   // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot
   // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we
@@ -1095,6 +1094,14 @@ void SmtEngine::declareSynthFun(const std::string& id,
         getOutputManager().getDumpOut(), func, vars, isInv, sygusType);
   }
 }
+void SmtEngine::declareSynthFun(Node func,
+                                bool isInv,
+                                const std::vector<Node>& vars)
+{
+  // use a null sygus type
+  TypeNode sygusType;
+  declareSynthFun(func, sygusType, isInv, vars);
+}
 
 void SmtEngine::assertSygusConstraint(Node constraint)
 {

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 6f08359b5fc42ff1f7b0dda4860ca17d34030537..091f69642cc5c9fbdbf5aa3c8a166a2e2691b86f 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -434,13 +434,13 @@ class CVC4_PUBLIC SmtEngine
    * which a function is being synthesized. Thus declared functions should use
    * this method as well.
    */
-  void declareSygusVar(const std::string& id, Node var, TypeNode type);
+  void declareSygusVar(Node var);
 
   /**
    * Add a function-to-synthesize declaration.
    *
-   * The given type may not correspond to the actual function type but to a
-   * datatype encoding the syntax restrictions for the
+   * The given sygusType may not correspond to the actual function type of func
+   * but to a datatype encoding the syntax restrictions for the
    * function-to-synthesize. In this case this information is stored to be used
    * during solving.
    *
@@ -451,11 +451,14 @@ class CVC4_PUBLIC SmtEngine
    * invariant. This information is necessary if we are dumping a command
    * corresponding to this declaration, so that it can be properly printed.
    */
-  void declareSynthFun(const std::string& id,
-                       Node func,
-                       TypeNode type,
+  void declareSynthFun(Node func,
+                       TypeNode sygusType,
                        bool isInv,
                        const std::vector<Node>& vars);
+  /**
+   * Same as above, without a sygus type.
+   */
+  void declareSynthFun(Node func, bool isInv, const std::vector<Node>& vars);
 
   /** Add a regular sygus constraint.*/
   void assertSygusConstraint(Node constraint);

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 42dbcd43ef2ae5e64aab9b2cb040e0f314813589..a3a976d4a325901a6b596a218c35e0295318d46c 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_solver.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::theory;
@@ -44,24 +45,20 @@ SygusSolver::SygusSolver(SmtSolver& sms,
 
 SygusSolver::~SygusSolver() {}
 
-void SygusSolver::declareSygusVar(const std::string& id,
-                                  Node var,
-                                  TypeNode type)
+void SygusSolver::declareSygusVar(Node var)
 {
-  Trace("smt") << "SygusSolver::declareSygusVar: " << id << " " << var << " "
-               << type << "\n";
-  Assert(var.getType() == type);
+  Trace("smt") << "SygusSolver::declareSygusVar: " << var << " "
+               << var.getType() << "\n";
   d_sygusVars.push_back(var);
   // don't need to set that the conjecture is stale
 }
 
-void SygusSolver::declareSynthFun(const std::string& id,
-                                  Node fn,
+void SygusSolver::declareSynthFun(Node fn,
                                   TypeNode sygusType,
                                   bool isInv,
                                   const std::vector<Node>& vars)
 {
-  Trace("smt") << "SygusSolver::declareSynthFun: " << id << "\n";
+  Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n";
   NodeManager* nm = NodeManager::currentNM();
   d_sygusFunSymbols.push_back(fn);
   if (!vars.empty())
@@ -72,7 +69,8 @@ void SygusSolver::declareSynthFun(const std::string& id,
     fn.setAttribute(ssfvla, bvl);
   }
   // whether sygus type encodes syntax restrictions
-  if (sygusType.isDatatype() && sygusType.getDType().isSygus())
+  if (!sygusType.isNull() && sygusType.isDatatype()
+      && sygusType.getDType().isSygus())
   {
     Node sym = nm->mkBoundVar("sfproxy", sygusType);
     // use an attribute to mark its grammar
@@ -180,9 +178,6 @@ Result SygusSolver::checkSynth(Assertions& as)
     NodeManager* nm = NodeManager::currentNM();
     // build synthesis conjecture from asserted constraints and declared
     // variables/functions
-    Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
-    Node inst_attr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
-    Node sygusAttr = nm->mkNode(INST_PATTERN_LIST, inst_attr);
     std::vector<Node> bodyv;
     Trace("smt") << "Sygus : Constructing sygus constraint...\n";
     size_t nconstraints = d_sygusConstraints.size();
@@ -200,15 +195,11 @@ Result SygusSolver::checkSynth(Assertions& as)
     }
     if (!d_sygusFunSymbols.empty())
     {
-      Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusFunSymbols);
-      body = nm->mkNode(FORALL, boundVars, body, sygusAttr);
+      body =
+          quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body);
     }
     Trace("smt") << "...constructed forall " << body << std::endl;
 
-    // set attribute for synthesis conjecture
-    SygusAttribute sa;
-    sygusVar.setAttribute(sa, true);
-
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
     if (Dump.isOn("raw-benchmark"))
     {

diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index c9de7b7e9e480ef0e3b9b67045f929f1145f52dc..b0670ea27f5ffe896331da830c7ed3bb5134bd89 100644 (file)
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -62,7 +62,7 @@ class SygusSolver
    * which a function is being synthesized. Thus declared functions should use
    * this method as well.
    */
-  void declareSygusVar(const std::string& id, Node var, TypeNode type);
+  void declareSygusVar(Node var);
 
   /**
    * Add a function-to-synthesize declaration.
@@ -79,8 +79,7 @@ class SygusSolver
    * invariant. This information is necessary if we are dumping a command
    * corresponding to this declaration, so that it can be properly printed.
    */
-  void declareSynthFun(const std::string& id,
-                       Node func,
+  void declareSynthFun(Node func,
                        TypeNode type,
                        bool isInv,
                        const std::vector<Node>& vars);

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 9fdb3370047d792f072a537ad400bd07fa86f6cb..3edec96c71529504ed2fc1d4898a2e8cf29a3253 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -233,14 +233,6 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   // set the sygus bound variable list
   Trace("sygus-interpol-debug") << "Set attributes..." << std::endl;
   itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared);
-  // sygus attribute
-  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
-  SygusAttribute ca;
-  sygusVar.setAttribute(ca, true);
-  Node instAttr = nm->mkNode(kind::INST_ATTRIBUTE, sygusVar);
-  std::vector<Node> iplc;
-  iplc.push_back(instAttr);
-  Node instAttrList = nm->mkNode(kind::INST_PATTERN_LIST, iplc);
   Trace("sygus-interpol-debug") << "...finish" << std::endl;
 
   // Fa( x )
@@ -339,12 +331,12 @@ bool SygusInterpol::solveInterpolation(const std::string& name,
   l.enableSygus();
   subSolver->setLogic(l);
 
-  for (Node var : d_vars)
+  for (const Node& var : d_vars)
   {
-    subSolver->declareSygusVar(name, var, var.getType());
+    subSolver->declareSygusVar(var);
   }
   std::vector<Node> vars_empty;
-  subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty);
+  subSolver->declareSynthFun(itp, grammarType, false, vars_empty);
   Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : "
                           << d_sygusConj << ", solving for "
                           << d_sygusConj[0][0] << std::endl;