This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.
This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.
Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.
d_rl_vals.end());
}
// rewrite with extended rewriter
- slem = extendedRewrite(slem);
+ slem = d_tds->rewriteNode(slem);
// collect all variables in slem
expr::getSymbols(slem, d_refinement_lemma_vars);
std::vector<Node> waiting;
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);
+ Node lemcsu = d_tds->rewriteNode(lemcs);
Trace("sygus-cref-eval2")
<< "...after unfolding is : " << lemcsu << std::endl;
if (lemcsu.isConst() && !lemcsu.getConst<bool>())
Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
eval_children[0] = vn;
Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
- res = d_tds->evaluateWithUnfolding(eval_fun);
+ res = d_tds->rewriteNode(eval_fun);
Trace("sygus-eval-unfold")
<< "Evaluate with unfolding returns " << res << std::endl;
esit.init(conj, n, res);
return ret;
}
-Node SygusEvalUnfold::unfold(Node en)
-{
- std::map<Node, Node> vtm;
- std::vector<Node> exp;
- return unfold(en, vtm, exp, false, false);
-}
-
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
std::vector<Node>& exp,
bool track_exp = true,
bool doRec = false);
- /**
- * Same as above, but without explanation tracking. This is used for concrete
- * evaluation heads
- */
- Node unfold(Node en);
private:
/** sygus term database associated with this utility */
d_result = res;
}
-Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n)
-{
- return tds->evaluateWithUnfolding(n, d_visited);
-}
-
bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
{
TNode tnvn = nvn;
for (const Node& c : d_terms)
{
Node conj_subs = c.substitute(d_var, tnvn, cache);
- Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
+ Node conj_subs_unfold = tds->rewriteNode(conj_subs);
Trace("sygus-cref-eval2-debug")
<< " ...check unfolding : " << conj_subs_unfold << std::endl;
Trace("sygus-cref-eval2-debug")
*/
void init(Node conj, Node var, Node res);
- /** do evaluate with unfolding, using the cache of this class */
- Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);
-
protected:
/** does d_terms{ d_var -> nvn } still rewrite to d_result? */
bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
* disjunctively, i.e. if one child test succeeds, the overall test succeeds.
*/
bool d_is_conjunctive;
- /** cache of n -> the simplified form of eval( n ) */
- std::unordered_map<Node, Node> d_visited;
};
/** EquivSygusInvarianceTest
Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
- body = d_tds->evaluateWithUnfolding(body);
+ body = d_tds->rewriteNode(body);
Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
<< std::endl;
- eut = d_tds->getEvalUnfold()->unfold(eut);
+ eut = d_tds->rewriteNode(eut);
Trace("sygus-unif-debug2") << " ...got " << eut;
Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
Node TermDbSygus::rewriteNode(Node n) const
{
- Node res = Rewriter::rewrite(n);
+ Node res;
+ if (options().quantifiers.sygusExtRew)
+ {
+ res = extendedRewrite(n);
+ }
+ else
+ {
+ res = rewrite(n);
+ }
if (res.isConst())
{
// constant, we are done
return rewriteNode(res);
}
-Node TermDbSygus::evaluateWithUnfolding(Node n,
- std::unordered_map<Node, Node>& visited)
-{
- std::unordered_map<Node, Node>::iterator it = visited.find(n);
- if( it==visited.end() ){
- Node ret = n;
- while (ret.getKind() == DT_SYGUS_EVAL
- && ret[0].getKind() == APPLY_CONSTRUCTOR)
- {
- if (ret == n && ret[0].isConst())
- {
- // use rewriting, possibly involving recursive functions
- ret = rewriteNode(ret);
- }
- else
- {
- ret = d_eval_unfold->unfold(ret);
- }
- }
- if( ret.getNumChildren()>0 ){
- std::vector< Node > children;
- if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( ret.getOperator() );
- }
- bool childChanged = false;
- for( unsigned i=0; i<ret.getNumChildren(); i++ ){
- Node nc = evaluateWithUnfolding(ret[i], visited);
- childChanged = childChanged || nc!=ret[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( ret.getKind(), children );
- }
- if (options::sygusExtRew())
- {
- ret = extendedRewrite(ret);
- }
- // use rewriting, possibly involving recursive functions
- ret = rewriteNode(ret);
- }
- visited[n] = ret;
- return ret;
- }else{
- return it->second;
- }
-}
-
-Node TermDbSygus::evaluateWithUnfolding(Node n)
-{
- std::unordered_map<Node, Node> visited;
- return evaluateWithUnfolding(n, visited);
-}
-
bool TermDbSygus::isEvaluationPoint(Node n) const
{
if (n.getKind() != DT_SYGUS_EVAL)
Node bn,
const std::vector<Node>& args,
bool tryEval = true);
- /** evaluate with unfolding
- *
- * n is any term that may involve sygus evaluation functions. This function
- * returns the result of unfolding the evaluation functions within n and
- * rewriting the result. For example, if eval_A is the evaluation function
- * for the datatype:
- * A -> C_0 | C_1 | C_x | C_+( C_A, C_A )
- * corresponding to grammar:
- * A -> 0 | 1 | x | A + A
- * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y.
- * The node returned by this function is in (extended) rewritten form.
- */
- Node evaluateWithUnfolding(Node n);
- /** same as above, but with a cache of visited nodes */
- Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited);
/** is evaluation point?
*
* Returns true if n is of the form eval( x, c1...cn ) for some variable x
projects / cvc5.git / commitdiff