summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_conjecture.cpp8
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp322
-rw-r--r--src/theory/quantifiers/sygus/cegis.h29
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp3
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.h2
-rw-r--r--src/theory/quantifiers/sygus/sygus_module.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_module.h2
-rw-r--r--src/theory/quantifiers/sygus/sygus_pbe.cpp1
-rw-r--r--src/theory/quantifiers/sygus/sygus_pbe.h2
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.cpp27
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.h6
11 files changed, 273 insertions, 131 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index cc12fdf17..6f5709fc2 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -367,11 +367,9 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
{
lem = Rewriter::rewrite( lem );
//eagerly unfold applications of evaluation function
- if( options::sygusDirectEval() ){
- Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
- std::map< Node, Node > visited_n;
- lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n );
- }
+ Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
+ std::map<Node, Node> visited_n;
+ lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n);
// record the instantiation
// this is used for remembering the solution
recordInstantiation(candidate_values);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index e8d29835a..47053080a 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -51,10 +51,9 @@ bool Cegis::initialize(Node n,
}
// initialize an enumerator for each candidate
- TermDbSygus* tds = d_qe->getTermDatabaseSygus();
for (unsigned i = 0; i < candidates.size(); i++)
{
- tds->registerEnumerator(candidates[i], candidates[i], d_parent);
+ d_tds->registerEnumerator(candidates[i], candidates[i], d_parent);
}
return true;
}
@@ -68,10 +67,6 @@ void Cegis::getTermList(const std::vector<Node>& candidates,
bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values)
{
- if (!options::sygusDirectEval())
- {
- return false;
- }
NodeManager* nm = NodeManager::currentNM();
bool addedEvalLemmas = false;
if (options::sygusCRefEval())
@@ -96,18 +91,21 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
add the lemmas below as well, in parallel. */
}
}
+ if (!options::sygusDirectEval())
+ {
+ return addedEvalLemmas;
+ }
Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl;
std::vector<Node> eager_terms, eager_vals, eager_exps;
- TermDbSygus* tds = d_qe->getTermDatabaseSygus();
for (unsigned i = 0, size = candidates.size(); i < size; ++i)
{
Trace("cegqi-debug") << " register " << candidates[i] << " -> "
<< candidate_values[i] << std::endl;
- tds->registerModelValue(candidates[i],
- candidate_values[i],
- eager_terms,
- eager_vals,
- eager_exps);
+ d_tds->registerModelValue(candidates[i],
+ candidate_values[i],
+ eager_terms,
+ eager_vals,
+ eager_exps);
}
Trace("cegqi-debug") << "...produced " << eager_terms.size()
<< " eager evaluation lemmas.\n";
@@ -148,11 +146,136 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
return true;
}
+void Cegis::addRefinementLemma(Node lem)
+{
+ d_refinement_lemmas.push_back(lem);
+ // apply existing substitution
+ Node slem = lem;
+ if (!d_rl_eval_hds.empty())
+ {
+ slem = lem.substitute(d_rl_eval_hds.begin(),
+ d_rl_eval_hds.end(),
+ d_rl_vals.begin(),
+ d_rl_vals.end());
+ }
+ // rewrite with extended rewriter
+ slem = d_tds->getExtRewriter()->extendedRewrite(slem);
+ std::vector<Node> waiting;
+ waiting.push_back(lem);
+ unsigned wcounter = 0;
+ // while we are not done adding lemmas
+ while (wcounter < waiting.size())
+ {
+ // add the conjunct, possibly propagating
+ addRefinementLemmaConjunct(wcounter, waiting);
+ wcounter++;
+ }
+}
+
+void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
+ std::vector<Node>& waiting)
+{
+ Node lem = waiting[wcounter];
+ lem = Rewriter::rewrite(lem);
+ // apply substitution and rewrite if applicable
+ if (lem.isConst())
+ {
+ if (!lem.getConst<bool>())
+ {
+ // conjecture is infeasible
+ }
+ else
+ {
+ return;
+ }
+ }
+ // break into conjunctions
+ if (lem.getKind() == AND)
+ {
+ for (const Node& lc : lem)
+ {
+ waiting.push_back(lc);
+ }
+ return;
+ }
+ // does this correspond to a substitution?
+ NodeManager* nm = NodeManager::currentNM();
+ TNode term;
+ TNode val;
+ if (lem.getKind() == EQUAL)
+ {
+ for (unsigned i = 0; i < 2; i++)
+ {
+ if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i]))
+ {
+ term = lem[1 - i];
+ val = lem[i];
+ break;
+ }
+ }
+ }
+ else
+ {
+ term = lem.getKind() == NOT ? lem[0] : lem;
+ // predicate case: the conjunct is a (negated) evaluation point
+ if (d_tds->isEvaluationPoint(term))
+ {
+ val = nm->mkConst(lem.getKind() != NOT);
+ }
+ }
+ if (!val.isNull())
+ {
+ if (d_refinement_lemma_unit.find(lem) != d_refinement_lemma_unit.end())
+ {
+ // already added
+ return;
+ }
+ Trace("cegis-rl") << "* cegis-rl: propagate: " << term << " -> " << val
+ << std::endl;
+ d_rl_eval_hds.push_back(term);
+ d_rl_vals.push_back(val);
+ d_refinement_lemma_unit.insert(lem);
+ // apply to waiting lemmas beyond this one
+ for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++)
+ {
+ waiting[i] = waiting[i].substitute(term, val);
+ }
+ // apply to all existing refinement lemmas
+ std::vector<Node> to_rem;
+ for (const Node& rl : d_refinement_lemma_conj)
+ {
+ Node srl = rl.substitute(term, val);
+ if (srl != rl)
+ {
+ Trace("cegis-rl") << "* cegis-rl: replace: " << rl << " -> " << srl
+ << std::endl;
+ waiting.push_back(srl);
+ to_rem.push_back(rl);
+ }
+ }
+ for (const Node& tr : to_rem)
+ {
+ d_refinement_lemma_conj.erase(tr);
+ }
+ }
+ else
+ {
+ if (Trace.isOn("cegis-rl"))
+ {
+ if (d_refinement_lemma_conj.find(lem) == d_refinement_lemma_conj.end())
+ {
+ Trace("cegis-rl") << "cegis-rl: add: " << lem << std::endl;
+ }
+ }
+ d_refinement_lemma_conj.insert(lem);
+ }
+}
+
void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
Node lem,
std::vector<Node>& lems)
{
- d_refinement_lemmas.push_back(lem);
+ addRefinementLemma(lem);
// Make the refinement lemma and add it to lems.
// This lemma is guarded by the parent's guard, which has the semantics
// "this conjecture has a solution", hence this lemma states:
@@ -168,118 +291,93 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
std::vector<Node>& lems)
{
Trace("sygus-cref-eval") << "Cref eval : conjecture has "
- << getNumRefinementLemmas() << " refinement lemmas."
+ << d_refinement_lemma_unit.size() << " unit and "
+ << d_refinement_lemma_conj.size()
+ << " non-unit refinement lemma conjunctions."
<< std::endl;
- unsigned nlemmas = getNumRefinementLemmas();
- if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE)
- {
- Assert(vs.size() == ms.size());
+ Assert(vs.size() == ms.size());
- TermDbSygus* tds = d_qe->getTermDatabaseSygus();
- NodeManager* nm = NodeManager::currentNM();
+ NodeManager* nm = NodeManager::currentNM();
- Node nfalse = nm->mkConst(false);
- Node neg_guard = d_parent->getGuard().negate();
- for (unsigned i = 0; i <= nlemmas; i++)
+ Node nfalse = nm->mkConst(false);
+ Node neg_guard = d_parent->getGuard().negate();
+ for (unsigned r = 0; r < 2; r++)
+ {
+ std::unordered_set<Node, NodeHashFunction>& rlemmas =
+ r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
+ for (const Node& lem : rlemmas)
{
- if (i == nlemmas)
- {
- bool addedSample = false;
- // find a new one by sampling, if applicable
- if (options::cegisSample() != CEGIS_SAMPLE_NONE)
- {
- addedSample = sampleAddRefinementLemma(vs, ms, lems);
- }
- if (!addedSample)
- {
- return;
- }
- }
- Node lem;
+ Assert(!lem.isNull());
std::map<Node, Node> visited;
std::map<Node, std::vector<Node> > exp;
- lem = getRefinementLemma(i);
- if (!lem.isNull())
+ EvalSygusInvarianceTest vsit;
+ Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem
+ << " against current model." << std::endl;
+ Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem
+ << " against current model." << std::endl;
+ Node cre_lem;
+ Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
+ Trace("sygus-cref-eval2")
+ << "...under substitution it is : " << lemcs << std::endl;
+ Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs);
+ Trace("sygus-cref-eval2")
+ << "...after unfolding is : " << lemcsu << std::endl;
+ if (lemcsu.isConst() && !lemcsu.getConst<bool>())
{
- std::vector<Node> lem_conj;
- // break into conjunctions
- if (lem.getKind() == kind::AND)
+ std::vector<Node> msu;
+ std::vector<Node> mexp;
+ msu.insert(msu.end(), ms.begin(), ms.end());
+ std::map<TypeNode, int> var_count;
+ for (unsigned k = 0; k < vs.size(); k++)
{
- for (unsigned i = 0; i < lem.getNumChildren(); i++)
- {
- lem_conj.push_back(lem[i]);
- }
+ vsit.setUpdatedTerm(msu[k]);
+ msu[k] = vs[k];
+ // substitute for everything except this
+ Node sconj =
+ lem.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
+ vsit.init(sconj, vs[k], nfalse);
+ // get minimal explanation for this
+ Node ut = vsit.getUpdatedTerm();
+ Trace("sygus-cref-eval2-debug")
+ << " compute min explain of : " << vs[k] << " = " << ut
+ << std::endl;
+ d_tds->getExplain()->getExplanationFor(
+ vs[k], ut, mexp, vsit, var_count, false);
+ Trace("sygus-cref-eval2-debug") << "exp now: " << mexp << std::endl;
+ msu[k] = vsit.getUpdatedTerm();
+ Trace("sygus-cref-eval2-debug")
+ << "updated term : " << msu[k] << std::endl;
}
- else
+ if (!mexp.empty())
{
- lem_conj.push_back(lem);
+ Node en = mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp);
+ cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard);
}
- EvalSygusInvarianceTest vsit;
- for (unsigned j = 0; j < lem_conj.size(); j++)
+ else
{
- Node lemc = lem_conj[j];
- Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc
- << " against current model." << std::endl;
- Trace("sygus-cref-eval2") << "Check refinement lemma conjunct "
- << lemc << " against current model."
- << std::endl;
- Node cre_lem;
- Node lemcs =
- lemc.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
- Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs
- << std::endl;
- Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs);
- Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu
- << std::endl;
- if (lemcsu.isConst() && !lemcsu.getConst<bool>())
- {
- std::vector<Node> msu;
- std::vector<Node> mexp;
- msu.insert(msu.end(), ms.begin(), ms.end());
- std::map<TypeNode, int> var_count;
- for (unsigned k = 0; k < vs.size(); k++)
- {
- vsit.setUpdatedTerm(msu[k]);
- msu[k] = vs[k];
- // substitute for everything except this
- Node sconj =
- lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
- vsit.init(sconj, vs[k], nfalse);
- // get minimal explanation for this
- Node ut = vsit.getUpdatedTerm();
- Trace("sygus-cref-eval2-debug")
- << " compute min explain of : " << vs[k] << " = " << ut
- << std::endl;
- tds->getExplain()->getExplanationFor(
- vs[k], ut, mexp, vsit, var_count, false);
- Trace("sygus-cref-eval2-debug")
- << "exp now: " << mexp << std::endl;
- msu[k] = vsit.getUpdatedTerm();
- Trace("sygus-cref-eval2-debug")
- << "updated term : " << msu[k] << std::endl;
- }
- if (!mexp.empty())
- {
- Node en =
- mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp);
- cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard);
- }
- else
- {
- cre_lem = neg_guard;
- }
- }
- if (!cre_lem.isNull())
- {
- if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
- {
- Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
- << std::endl;
- lems.push_back(cre_lem);
- }
- }
+ cre_lem = neg_guard;
}
}
+ if (!cre_lem.isNull()
+ && std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
+ {
+ Trace("sygus-cref-eval")
+ << "...produced lemma : " << cre_lem << std::endl;
+ lems.push_back(cre_lem);
+ }
+ }
+ if (!lems.empty())
+ {
+ break;
+ }
+ }
+ // if we didn't add a lemma, trying sampling to add one
+ if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
+ {
+ if (sampleAddRefinementLemma(vs, ms, lems))
+ {
+ // restart (should be guaranteed to add evaluation lemmas
+ getRefinementEvalLemmas(vs, ms, lems);
}
}
}
@@ -344,7 +442,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
Trace("cegis-sample") << std::endl;
}
Trace("cegqi-engine") << " *** Refine by sampling" << std::endl;
- d_refinement_lemmas.push_back(rlem);
+ addRefinementLemma(rlem);
// if trust, we are not interested in sending out refinement lemmas
if (options::cegisSample() != CEGIS_SAMPLE_TRUST)
{
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 7500abb78..cbd563e07 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -76,14 +76,31 @@ class Cegis : public SygusModule
//-----------------------------------refinement lemmas
/** refinement lemmas */
std::vector<Node> d_refinement_lemmas;
- /** get number of refinement lemmas we have added so far */
- unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
- /** get refinement lemma
+ /** (processed) conjunctions of refinement lemmas that are not unit */
+ std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_conj;
+ /** (processed) conjunctions of refinement lemmas that are unit */
+ std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_unit;
+ /** substitution entailed by d_refinement_lemma_unit */
+ std::vector<Node> d_rl_eval_hds;
+ std::vector<Node> d_rl_vals;
+ /** adds lem as a refinement lemma */
+ void addRefinementLemma(Node lem);
+ /** add refinement lemma conjunct
*
- * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement
- * lemma is one of the form ~P( d_candidates, c ) for some c.
+ * This is a helper function for addRefinementLemma.
+ *
+ * This adds waiting[wcounter] to the proper vector (d_refinement_lemma_conj
+ * or d_refinement_lemma_unit). In the case that waiting[wcounter] corresponds
+ * to a value propagation, e.g. it is of the form:
+ * (eval x c1...cn) = c
+ * then it is added to d_refinement_lemma_unit, (eval x c1...cn) -> c is added
+ * as a substitution in d_rl_eval_hds/d_rl_eval_vals, and applied to previous
+ * lemmas in d_refinement_lemma_conj and lemmas waiting[k] for k>wcounter.
+ * Each lemma in d_refinement_lemma_conj that is modifed in this process is
+ * moved to the vector waiting.
*/
- Node getRefinementLemma(unsigned i) { return d_refinement_lemmas[i]; }
+ void addRefinementLemmaConjunct(unsigned wcounter,
+ std::vector<Node>& waiting);
/** sample add refinement lemma
*
* This function will check if there is a sample point in d_sampler that
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index ab9834254..20f062722 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -30,7 +30,6 @@ namespace quantifiers {
CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
: Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
{
- d_tds = d_qe->getTermDatabaseSygus();
}
CegisUnif::~CegisUnif() {}
@@ -254,7 +253,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
// Notify lemma to unification utility and get its purified form
std::map<Node, std::vector<Node>> eval_pts;
Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
- d_refinement_lemmas.push_back(plem);
+ addRefinementLemma(plem);
Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n";
// Notify the enumeration manager if there are new evaluation points
for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 735477821..ecaec4129 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -249,8 +249,6 @@ class CegisUnif : public Cegis
Node getNextDecisionRequest(unsigned& priority) override;
private:
- /** sygus term database of d_qe */
- TermDbSygus* d_tds;
/**
* Sygus unif utility. This class implements the core algorithm (e.g. decision
* tree learning) that this module relies upon.
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 19e064350..11747830d 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -19,7 +19,7 @@ namespace theory {
namespace quantifiers {
SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p)
- : d_qe(qe), d_parent(p)
+ : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
{
}
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 07f5aec9d..75be570e6 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -126,6 +126,8 @@ class SygusModule
protected:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
+ /** sygus term database of d_qe */
+ quantifiers::TermDbSygus* d_tds;
/** reference to the parent conjecture */
CegConjecture* d_parent;
};
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index cd011ef44..9919dff49 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -31,7 +31,6 @@ namespace quantifiers {
CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
: SygusModule(qe, p)
{
- d_tds = d_qe->getTermDatabaseSygus();
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
d_is_pbe = false;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index fbf89fee9..dc61f459b 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -188,8 +188,6 @@ class CegConjecturePbe : public SygusModule
Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
private:
- /** sygus term database of d_qe */
- quantifiers::TermDbSygus* d_tds;
/** true and false nodes */
Node d_true;
Node d_false;
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 3d88cbe5d..0b7841170 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1597,6 +1597,33 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) {
return evaluateWithUnfolding( n, visited );
}
+bool TermDbSygus::isEvaluationPoint(Node n) const
+{
+ if (n.getKind() != APPLY_UF || n.getNumChildren() == 0 || !n[0].isVar())
+ {
+ return false;
+ }
+ for (unsigned i = 1, nchild = n.getNumChildren(); i < nchild; i++)
+ {
+ if (!n[i].isConst())
+ {
+ return false;
+ }
+ }
+ TypeNode tn = n[0].getType();
+ if (!tn.isDatatype())
+ {
+ return false;
+ }
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ if (!dt.isSygus())
+ {
+ return false;
+ }
+ Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
+ return eval_op == n.getOperator();
+}
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 4a3dcb8d6..9466a6a10 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -183,6 +183,12 @@ class TermDbSygus {
/** same as above, but with a cache of visited nodes */
Node evaluateWithUnfolding(
Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
+ /** is evaluation point?
+ *
+ * Returns true if n is of the form eval( x, c1...cn ) for some variable x
+ * and constants c1...cn.
+ */
+ bool isEvaluationPoint(Node n) const;
//-----------------------------end conversion from sygus to builtin
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback