diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-15 15:19:08 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-15 15:19:08 -0600 |
commit | 8c4598683e4edd217ed524d47c68a053b6881f4c (patch) | |
tree | 5fe19c4d5e0fba6800ba2b3f853617f2b6e390ec /src/preprocessing | |
parent | 35f58d81fb57608d52884f560ff281fe52c7b18f (diff) |
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.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 10 | ||||
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 10 |
2 files changed, 4 insertions, 16 deletions
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index ea767e771..caf63b0ec 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/smt_engine_subsolver.h" using namespace std; @@ -293,15 +294,8 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, // sygus attribute to mark the conjecture as a sygus conjecture Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl; - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - theory::SygusAttribute ca; - sygusVar.setAttribute(ca, true); - Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); - Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); - Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars); - - body = nm->mkNode(FORALL, fbvl, body, instAttrList); + body = quantifiers::SygusUtils::mkSygusConjecture(ff_vars, body); Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; 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); |