diff options
Diffstat (limited to 'src/preprocessing/passes')
-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); |