From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Oct 2020 13:40:06 +0000 (-0500)
Subject: Make SygusSolver use sygus attributes directly (#5172)
X-Git-Tag: cvc5-1.0.0~2776
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c2a0ef0f00696eb4bbffcbbf23a43508c1c3987;p=cvc5.git

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 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"))
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 808137fd6..0f5ada549 100644
--- 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 cc2e41032..387a3e9d8 100644
--- 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 );