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.

1 files changed, 10 insertions, 11 deletions

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 3073ef0fe..0b40bf894 100644
--- 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"))