Consolidate basic sygus utilities regarding sygus conjectures (#5421)

This is required for new work on generalizing CAV 2015 single invocation techniques.

It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.

1 files changed, 2 insertions, 8 deletions

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 8465a63a0..ecf1e281d 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
@@ -429,12 +430,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 
   // sygus attribute to mark the conjecture as a sygus conjecture
   Trace("srs-input") << "Make sygus conjecture..." << std::endl;
-  Node iaVar = nm->mkSkolem("sygus", nm->booleanType());
-  // the attribute to mark the conjecture as being a sygus conjecture
-  theory::SygusAttribute ca;
-  iaVar.setAttribute(ca, true);
-  Node instAttr = nm->mkNode(INST_ATTRIBUTE, iaVar);
-  Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr);
   // we are "synthesizing" functions for each type of subterm
   std::vector<Node> synthConj;
   unsigned fCounter = 1;
@@ -451,10 +446,9 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     // this marks that the grammar used for solutions for sfun is the type of
     // gvar, which is the sygus datatype type constructed above.
     sfun.setAttribute(ssg, gvar);
-    Node fvarBvl = nm->mkNode(BOUND_VAR_LIST, sfun);
 
     Node body = nm->mkConst(false);
-    body = nm->mkNode(FORALL, fvarBvl, body, instAttrList);
+    body = theory::quantifiers::SygusUtils::mkSygusConjecture({sfun}, body);
     synthConj.push_back(body);
   }
   Node trueNode = nm->mkConst(true);