summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_conjecture.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp141
1 files changed, 106 insertions, 35 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 469775a46..7955d59a8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -53,7 +53,8 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe)
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
- d_refine_count(0)
+ d_refine_count(0),
+ d_guarded_stream_exc(false)
{
if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
{
@@ -240,10 +241,6 @@ bool SynthConjecture::isSingleInvocation() const
bool SynthConjecture::needsCheck()
{
- if (isSingleInvocation() && !d_ceg_si->needsCheck())
- {
- return false;
- }
bool value;
Assert(!d_feasible_guard.isNull());
// non or fully single invocation : look at guard only
@@ -254,6 +251,11 @@ bool SynthConjecture::needsCheck()
Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
return false;
}
+ else
+ {
+ Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard
+ << " assigned true." << std::endl;
+ }
}
else
{
@@ -273,7 +275,7 @@ void SynthConjecture::doSingleInvCheck(std::vector<Node>& lems)
}
bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
-void SynthConjecture::doCheck(std::vector<Node>& lems)
+bool SynthConjecture::doCheck(std::vector<Node>& lems)
{
Assert(d_master != nullptr);
@@ -288,24 +290,10 @@ void SynthConjecture::doCheck(std::vector<Node>& lems)
// we have a new guard, print and continue the stream
printAndContinueStream();
d_current_stream_guard = currGuard;
- return;
+ return true;
}
}
- bool checkSuccess = false;
- do
- {
- Trace("cegqi-check-debug") << "doCheckNext..." << std::endl;
- checkSuccess = doCheckNext(lems);
- Trace("cegqi-check-debug")
- << "...finished " << lems.empty() << " " << !needsRefinement() << " "
- << !d_qe->getTheoryEngine()->needCheck() << " " << checkSuccess
- << std::endl;
- } while (lems.empty() && !needsRefinement()
- && !d_qe->getTheoryEngine()->needCheck() && checkSuccess);
-}
-bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
-{
// get the list of terms that the master strategy is interested in
std::vector<Node> terms;
d_master->getTermList(d_candidates, terms);
@@ -364,7 +352,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
{
// we retain the values in d_ev_active_gen_waiting
Trace("cegqi-engine") << "...partial model, fail." << std::endl;
- return false;
+ return true;
}
// the waiting values are passed to the module below, clear
d_ev_active_gen_waiting.clear();
@@ -407,7 +395,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
if (emptyModel)
{
Trace("cegqi-engine") << "...empty model, fail." << std::endl;
- return false;
+ return true;
}
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
@@ -462,7 +450,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
{
if (!constructed_cand)
{
- return true;
+ return false;
}
}
@@ -502,7 +490,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
if (lem.isNull())
{
// no lemma to check
- return true;
+ return false;
}
lem = Rewriter::rewrite(lem);
@@ -557,7 +545,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
Assert(squery.isConst() && squery.getConst<bool>());
#endif
- return true;
+ return false;
}
else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
@@ -577,7 +565,7 @@ bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
// if we were successful, we immediately print the current solution.
// this saves us from introducing a verification lemma and a new guard.
printAndContinueStream();
- return true;
+ return false;
}
lem = getStreamGuardedLemma(lem);
lems.push_back(lem);
@@ -662,30 +650,101 @@ void SynthConjecture::preregisterConjecture(Node q)
bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
std::vector<Node>& v)
{
+ std::vector<Node> ncheck = n;
+ n.clear();
bool ret = true;
- for (unsigned i = 0; i < n.size(); i++)
+ for (unsigned i = 0, size = ncheck.size(); i < size; i++)
{
- Node nv = getEnumeratedValue(n[i]);
+ Node e = ncheck[i];
+ // if it is not active, we return null
+ Node g = d_tds->getActiveGuardForEnumerator(e);
+ if (!g.isNull())
+ {
+ Node gstatus = d_qe->getValuation().getSatValue(g);
+ if (gstatus.isNull() || !gstatus.getConst<bool>())
+ {
+ Trace("cegqi-engine-debug")
+ << "Enumerator " << e << " is inactive." << std::endl;
+ continue;
+ }
+ }
+ Node nv = getEnumeratedValue(e);
+ n.push_back(e);
v.push_back(nv);
ret = ret && !nv.isNull();
}
return ret;
}
+/** A basic sygus value generator
+ *
+ * This class is a "naive" term generator for sygus conjectures, which invokes
+ * the type enumerator to generate a stream of (all) sygus terms of a given
+ * type.
+ */
+class EnumValGeneratorBasic : public EnumValGenerator
+{
+ public:
+ EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_te(tn) {}
+ ~EnumValGeneratorBasic() {}
+ /** initialize (do nothing) */
+ void initialize(Node e) override {}
+ /** initialize (do nothing) */
+ void addValue(Node v) override {}
+ /**
+ * Get next returns the next (T-rewriter-unique) value based on the type
+ * enumerator.
+ */
+ Node getNext() override
+ {
+ if (d_te.isFinished())
+ {
+ return Node::null();
+ }
+ Node next = *d_te;
+ ++d_te;
+ Node nextb = d_tds->sygusToBuiltin(next);
+ if (options::sygusSymBreakDynamic())
+ {
+ nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
+ }
+ if (d_cache.find(nextb) == d_cache.end())
+ {
+ d_cache.insert(nextb);
+ return next;
+ }
+ return getNext();
+ }
+
+ private:
+ /** pointer to term database sygus */
+ TermDbSygus* d_tds;
+ /** the type enumerator */
+ TypeEnumerator d_te;
+ /** cache of (enumerated) builtin values we have enumerated so far */
+ std::unordered_set<Node, NodeHashFunction> d_cache;
+};
+
Node SynthConjecture::getEnumeratedValue(Node e)
{
- if (e.getAttribute(SygusSymBreakExcAttribute()))
+ bool isEnum = d_tds->isEnumerator(e);
+
+ if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
{
- // if the current model value of e was excluded by symmetry breaking, then
- // it does not have a proper model value that we should consider, thus we
- // return null.
+ // if the current model value of e was not registered by the datatypes
+ // sygus solver, or was excluded by symmetry breaking, then it does not
+ // have a proper model value that we should consider, thus we return null.
+ Trace("cegqi-engine-debug")
+ << "Enumerator " << e << " does not have proper model value."
+ << std::endl;
return Node::null();
}
- if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e))
+ if (!isEnum || d_tds->isPassiveEnumerator(e))
{
return getModelValue(e);
}
+
// management of actively generated enumerators goes here
// initialize the enumerated value generator for e
@@ -693,7 +752,14 @@ Node SynthConjecture::getEnumeratedValue(Node e)
d_evg.find(e);
if (iteg == d_evg.end())
{
- d_evg[e].reset(new EnumStreamConcrete(d_tds));
+ if (d_tds->isVariableAgnosticEnumerator(e))
+ {
+ d_evg[e].reset(new EnumStreamConcrete(d_tds));
+ }
+ else
+ {
+ d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+ }
Trace("sygus-active-gen")
<< "Active-gen: initialize for " << e << std::endl;
d_evg[e]->initialize(e);
@@ -872,6 +938,11 @@ void SynthConjecture::printAndContinueStream()
}
if (!exp.empty())
{
+ if (!d_guarded_stream_exc)
+ {
+ d_guarded_stream_exc = true;
+ exp.push_back(d_feasible_guard);
+ }
Node exc_lem = exp.size() == 1
? exp[0]
: NodeManager::currentNM()->mkNode(kind::AND, exp);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback