Make SygusSolver use sygus attributes directly (#5172)

Previously, the SmtEngine was using an interface through TheoryEngine to set user attributes to indicate that e.g. a synth-fun is associated with a given grammar. Since SmtEngine and its members are internal now, this can simply be done directly via attributes. This makes it so that SygusSolver does not depend on TheoryEngine nor does it require the TheoryEngine to be initialized at the time a synth-fun is created.

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 3073ef0fea455c7ae89f782a421608b670c6e9d8..0b40bf8948de5056fd7c82b3167a8dff08d11274 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -21,8 +21,9 @@
 #include "smt/dump.h"
 #include "smt/preprocessor.h"
 #include "smt/smt_solver.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/smt_engine_subsolver.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4::theory;
 using namespace CVC4::kind;
@@ -62,23 +63,21 @@ void SygusSolver::declareSynthFun(const std::string& id,
 {
   Trace("smt") << "SygusSolver::declareSynthFun: " << id << "\n";
   NodeManager* nm = NodeManager::currentNM();
-  TheoryEngine* te = d_smtSolver.getTheoryEngine();
-  Assert(te != nullptr);
   d_sygusFunSymbols.push_back(fn);
   if (!vars.empty())
   {
     Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
-    std::vector<Node> attr_val_bvl;
-    attr_val_bvl.push_back(bvl);
-    te->setUserAttribute("sygus-synth-fun-var-list", fn, attr_val_bvl, "");
+    // use an attribute to mark its bound variable list
+    SygusSynthFunVarListAttribute ssfvla;
+    fn.setAttribute(ssfvla, bvl);
   }
   // whether sygus type encodes syntax restrictions
   if (sygusType.isDatatype() && sygusType.getDType().isSygus())
   {
     Node sym = nm->mkBoundVar("sfproxy", sygusType);
-    std::vector<Node> attr_value;
-    attr_value.push_back(sym);
-    te->setUserAttribute("sygus-synth-grammar", fn, attr_value, "");
+    // use an attribute to mark its grammar
+    SygusSynthGrammarAttribute ssfga;
+    fn.setAttribute(ssfga, sym);
   }
 
   // sygus conjecture is now stale
@@ -207,8 +206,8 @@ Result SygusSolver::checkSynth(Assertions& as)
     Trace("smt") << "...constructed forall " << body << std::endl;
 
     // set attribute for synthesis conjecture
-    TheoryEngine* te = d_smtSolver.getTheoryEngine();
-    te->setUserAttribute("sygus", sygusVar, {}, "");
+    SygusAttribute sa;
+    sygusVar.setAttribute(sa, true);
 
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
     if (Dump.isOn("raw-benchmark"))

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 808137fd6354165843459d5c6120b9b223e2bd13..0f5ada5491323505311842f9442dde89bd852714 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -46,10 +46,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
     FunDefAttribute fda;
     n.setAttribute( fda, true );
-  }else if( attr=="sygus" ){
-    Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
-    SygusAttribute ca;
-    n.setAttribute( ca, true );
   }
   else if (attr == "qid")
   {
@@ -57,17 +53,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
     QuantNameAttribute qna;
     n.setAttribute(qna, true);
-  } else if (attr == "sygus-synth-grammar") {
-    Assert(node_values.size() == 1);
-    Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to "
-                              << node_values[0] << std::endl;
-    SygusSynthGrammarAttribute ssg;
-    n.setAttribute(ssg, node_values[0]);
-  }else if( attr=="sygus-synth-fun-var-list" ){
-    Assert(node_values.size() == 1);
-    Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to "  << node_values[0] << std::endl;
-    SygusSynthFunVarListAttribute ssfvla;
-    n.setAttribute( ssfvla, node_values[0] );
   }else if( attr=="quant-inst-max-level" ){
     Assert(node_values.size() == 1);
     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index cc2e410326af379eeabc499297f1cf97f4d05bcf..387a3e9d8598a95cb8fe94623d248fcbee92984d 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -46,10 +46,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
       d_qstate(c, u, valuation)
 {
   out.handleUserAttribute( "fun-def", this );
-  out.handleUserAttribute( "sygus", this );
   out.handleUserAttribute("qid", this);
-  out.handleUserAttribute("sygus-synth-grammar", this);
-  out.handleUserAttribute( "sygus-synth-fun-var-list", this );
   out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "quant-elim", this );
   out.handleUserAttribute( "quant-elim-partial", this );