namespace quantifiers {
Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
- : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false)
+ : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false)
{
- if (options::sygusEvalUnfold())
- {
- d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
- }
+ d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
}
bool Cegis::initialize(Node conj,
for (unsigned i = 0; i < csize; i++)
{
Trace("cegis") << "...register enumerator " << candidates[i];
- bool do_repair_const = false;
+ bool useSymCons = false;
if (options::sygusRepairConst())
{
TypeNode ctn = candidates[i].getType();
SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
if (cti.hasSubtermSymbolicCons())
{
- do_repair_const = true;
- // remember that we are doing grammar-based repair
- d_using_gr_repair = true;
- Trace("cegis") << " (using repair)";
+ useSymCons = true;
+ // remember that we are using symbolic constructors
+ d_usingSymCons = true;
+ Trace("cegis") << " (using symbolic constructors)";
}
}
Trace("cegis") << std::endl;
d_tds->registerEnumerator(
- candidates[i], candidates[i], d_parent, erole, do_repair_const);
+ candidates[i], candidates[i], d_parent, erole, useSymCons);
}
return true;
}
}
NodeManager* nm = NodeManager::currentNM();
bool addedEvalLemmas = false;
- if (options::sygusRefEval())
+ // Refinement evaluation should not be done for grammars with symbolic
+ // constructors.
+ bool doRefEval = options::sygusRefEval() && !d_usingSymCons;
+ if (doRefEval)
{
Trace("cegqi-engine") << " *** Do refinement lemma evaluation"
<< (doGen ? " with conjecture-specific refinement"
}
}
// we only do evaluation unfolding for passive enumerators
- if (doGen && d_eval_unfold != nullptr)
+ bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
+ if (doEvalUnfold)
{
Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl;
std::vector<Node> eager_terms, eager_vals, eager_exps;
}
}
// if we are using grammar-based repair
- if (d_using_gr_repair)
+ if (d_usingSymCons && options::sygusRepairConst())
{
SygusRepairConst* src = d_parent->getRepairConst();
Assert(src != nullptr);
*/
std::unordered_set<unsigned> d_cegis_sample_refine;
- //---------------------------------for sygus repair
- /** are we using grammar-based repair?
+ //---------------------------------for symbolic constructors
+ /** are we using symbolic constants?
*
* This flag is set ot true if at least one of the enumerators allocated
* by this class has been configured to allow model values with symbolic
* constructors, such as the "any constant" constructor.
*/
- bool d_using_gr_repair;
- //---------------------------------end for sygus repair
+ bool d_usingSymCons;
+ //---------------------------------end for symbolic constructors
};
} /* CVC4::theory::quantifiers namespace */
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
+#include "expr/sygus_datatype.h"
#include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace std;
antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
// Node antec = n.eqNode( vn );
TypeNode tn = n.getType();
+ // Check if the sygus type has any symbolic constructors. This will
+ // impact how the unfolding is computed below.
+ SygusTypeInfo& sti = d_tds->getTypeInfo(tn);
+ bool hasSymCons = sti.hasSubtermSymbolicCons();
// n occurs as an evaluation head, thus it has sygus datatype type
Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
do_unfold = true;
}
}
- if (do_unfold)
+ if (do_unfold || hasSymCons)
{
// note that this is replicated for different values
std::map<Node, Node> vtm;
eval_children.end(), it->second[i].begin(), it->second[i].end());
Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
eval_children.resize(1);
- res = d_tds->unfold(eval_fun, vtm, exp);
+ // If we explicitly asked to unfold, we use single step, otherwise
+ // we use multi step.
+ res = unfold(eval_fun, vtm, exp, true, !do_unfold);
+ Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl;
expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
}
else
eval_children[0] = vn;
Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
res = d_tds->evaluateWithUnfolding(eval_fun);
+ Trace("sygus-eval-unfold")
+ << "Evaluate with unfolding returns " << res << std::endl;
esit.init(conj, n, res);
eval_children.resize(1);
eval_children[0] = n;
}
}
+Node SygusEvalUnfold::unfold(Node en,
+ std::map<Node, Node>& vtm,
+ std::vector<Node>& exp,
+ bool track_exp,
+ bool doRec)
+{
+ if (en.getKind() != DT_SYGUS_EVAL)
+ {
+ Assert(en.isConst());
+ return en;
+ }
+ Trace("sygus-eval-unfold-debug")
+ << "Unfold : " << en << ", track exp is " << track_exp << ", doRec is "
+ << doRec << std::endl;
+ Node ev = en[0];
+ if (track_exp)
+ {
+ std::map<Node, Node>::iterator itv = vtm.find(en[0]);
+ Assert(itv != vtm.end());
+ if (itv != vtm.end())
+ {
+ ev = itv->second;
+ }
+ Assert(en[0].getType() == ev.getType());
+ Assert(ev.isConst());
+ }
+ Trace("sygus-eval-unfold-debug")
+ << "Unfold model value is : " << ev << std::endl;
+ AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR);
+ std::vector<Node> args;
+ for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
+ {
+ args.push_back(en[i]);
+ }
+
+ TypeNode headType = en[0].getType();
+ Type headTypeT = headType.toType();
+ NodeManager* nm = NodeManager::currentNM();
+ const Datatype& dt = headType.getDatatype();
+ unsigned i = datatypes::utils::indexOf(ev.getOperator());
+ if (track_exp)
+ {
+ // explanation
+ Node ee =
+ nm->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
+ if (std::find(exp.begin(), exp.end(), ee) == exp.end())
+ {
+ exp.push_back(ee);
+ }
+ }
+ // if we are a symbolic constructor, unfolding returns the subterm itself
+ Node sop = Node::fromExpr(dt[i].getSygusOp());
+ if (sop.getAttribute(SygusAnyConstAttribute()))
+ {
+ Trace("sygus-eval-unfold-debug")
+ << "...it is an any-constant constructor" << std::endl;
+ Assert(dt[i].getNumArgs() == 1);
+ // If the argument to evaluate is itself concrete, then we use its
+ // argument; otherwise we return its selector.
+ if (en[0].getKind() == APPLY_CONSTRUCTOR)
+ {
+ Trace("sygus-eval-unfold-debug")
+ << "...return (from constructor) " << en[0][0] << std::endl;
+ return en[0][0];
+ }
+ else
+ {
+ Node ret = nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, 0), en[0]);
+ Trace("sygus-eval-unfold-debug")
+ << "...return (from constructor) " << ret << std::endl;
+ return ret;
+ }
+ }
+
+ Assert(!dt.isParametric());
+ std::map<int, Node> pre;
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ std::vector<Node> cc;
+ Node s;
+ // get the j^th subfield of en
+ if (en[0].getKind() == APPLY_CONSTRUCTOR)
+ {
+ // if it is a concrete constructor application, as an optimization,
+ // just return the argument
+ s = en[0][j];
+ }
+ else
+ {
+ s = nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, j), en[0]);
+ }
+ cc.push_back(s);
+ if (track_exp)
+ {
+ // update vtm map
+ vtm[s] = ev[j];
+ }
+ cc.insert(cc.end(), args.begin(), args.end());
+ Node argj = nm->mkNode(DT_SYGUS_EVAL, cc);
+ if (doRec)
+ {
+ Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl;
+ // evaluate recursively
+ argj = unfold(argj, vtm, exp, track_exp, doRec);
+ }
+ pre[j] = argj;
+ }
+ Node ret = d_tds->mkGeneric(dt, i, pre);
+ // apply the appropriate substitution to ret
+ ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
+ // rewrite
+ ret = Rewriter::rewrite(ret);
+ 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 CVC4
std::vector<Node>& exps,
std::vector<Node>& terms,
std::vector<Node>& vals);
+ /** unfold
+ *
+ * This method is called when a sygus term d (typically a variable for a SyGuS
+ * enumerator) has a model value specified by the map vtm. The argument en
+ * is an application of kind DT_SYGUS_EVAL, i.e. eval( d, c1, ..., cm ).
+ * Typically, d is a shared selector chain, although it may also be a
+ * non-constant application of a constructor.
+ *
+ * If doRec is false, this method returns the one-step unfolding of this
+ * evaluation function application. An example of a one step unfolding is:
+ * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) )
+ *
+ * This function does this unfolding for a (possibly symbolic) evaluation
+ * head, where the argument "variable to model" vtm stores the model value of
+ * variables from this head. This allows us to track an explanation of the
+ * unfolding in the vector exp when track_exp is true.
+ *
+ * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then
+ * this method applied to eval( d, t ) will return
+ * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp.
+ *
+ * If the argument doRec is true, we do a multi-step unfolding instead of
+ * a single-step unfolding. For example, if vtm[d] = C_+( C_x(), C_0() ),
+ * then this method applied to eval(d,5) will return 5+0 = 0.
+ *
+ * Furthermore, notice that any-constant constructors are *never* expanded to
+ * their concrete model values. This means that the multi-step unfolding when
+ * vtm[d] = C_+( C_x(), any_constant(n) ), then this method applied to
+ * eval(d,5) will return 5 + d.2.1, where the latter term is a shared selector
+ * chain. In other words, this unfolding elaborates the connection between
+ * the builtin integer field d.2.1 of d and the builtin interpretation of
+ * this sygus term, for the given argument.
+ */
+ Node unfold(Node en,
+ std::map<Node, Node>& vtm,
+ 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 */
{
TNode cand = n[0];
Node tmp = n.substitute(cand, it->second);
- nv = d_tds->evaluateWithUnfolding(tmp);
+ // should be concrete, can just use the rewriter
+ nv = Rewriter::rewrite(tmp);
Trace("sygus-unif-rl-purify")
<< "PurifyLemma : model value for " << tmp << " is " << nv << "\n";
}
#include "theory/quantifiers/sygus/sygus_unif_strat.h"
#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "theory/quantifiers/sygus/sygus_unif.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
<< std::endl;
- eut = d_qe->getTermDatabaseSygus()->unfold(eut);
+ eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut);
Trace("sygus-unif-debug2") << " ...got " << eut;
Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
bool addedLemma = false;
for (const Node& lem : cclems)
{
- Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem
- << std::endl;
if (d_quantEngine->addLemma(lem))
{
++(d_statistics.d_cegqi_lemmas_ce);
}
}
-Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
- if (en.getKind() != DT_SYGUS_EVAL)
- {
- Assert(en.isConst());
- return en;
- }
- Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
- Node ev = en[0];
- if (track_exp)
- {
- std::map<Node, Node>::iterator itv = vtm.find(en[0]);
- Assert(itv != vtm.end());
- if (itv != vtm.end())
- {
- ev = itv->second;
- }
- Assert(en[0].getType() == ev.getType());
- Assert(ev.isConst());
- }
- Assert(ev.getKind() == kind::APPLY_CONSTRUCTOR);
- std::vector<Node> args;
- for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
- {
- args.push_back(en[i]);
- }
-
- Type headType = en[0].getType().toType();
- NodeManager* nm = NodeManager::currentNM();
- const Datatype& dt = static_cast<DatatypeType>(headType).getDatatype();
- unsigned i = datatypes::utils::indexOf(ev.getOperator());
- if (track_exp)
- {
- // explanation
- Node ee = nm->mkNode(
- kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
- if (std::find(exp.begin(), exp.end(), ee) == exp.end())
- {
- exp.push_back(ee);
- }
- }
- // if we are a symbolic constructor, unfolding returns the subterm itself
- Node sop = Node::fromExpr(dt[i].getSygusOp());
- if (sop.getAttribute(SygusAnyConstAttribute()))
- {
- Trace("sygus-db-debug") << "...it is an any-constant constructor"
- << std::endl;
- Assert(dt[i].getNumArgs() == 1);
- if (en[0].getKind() == APPLY_CONSTRUCTOR)
- {
- return en[0][0];
- }
- else
- {
- return nm->mkNode(
- APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
- }
- }
-
- Assert(!dt.isParametric());
- std::map<int, Node> pre;
- for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
- {
- std::vector<Node> cc;
- Node s;
- // get the j^th subfield of en
- if (en[0].getKind() == kind::APPLY_CONSTRUCTOR)
- {
- // if it is a concrete constructor application, as an optimization,
- // just return the argument
- s = en[0][j];
- }
- else
- {
- s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
- dt[i].getSelectorInternal(headType, j),
- en[0]);
- }
- cc.push_back(s);
- if (track_exp)
- {
- // update vtm map
- vtm[s] = ev[j];
- }
- cc.insert(cc.end(), args.begin(), args.end());
- pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc);
- }
- Node ret = mkGeneric(dt, i, pre);
- // apply the appropriate substitution to ret
- ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
- // rewrite
- ret = Rewriter::rewrite(ret);
- return ret;
-}
-
-Node TermDbSygus::unfold(Node en)
-{
- std::map<Node, Node> vtm;
- std::vector<Node> exp;
- return unfold(en, vtm, exp, false);
-}
-
Node TermDbSygus::evaluateBuiltin(TypeNode tn,
Node bn,
std::vector<Node>& args,
Trace("dt-eval-unfold-debug")
<< "Optimize: evaluate constant head " << ret << std::endl;
// can just do direct evaluation here
+ // notice we prefer this code to the rewriter since it may use
+ // the evaluator
std::vector<Node> args;
bool success = true;
for (unsigned i = 1, nchild = ret.getNumChildren(); i < nchild; i++)
return rete;
}
}
- ret = unfold( ret );
+ ret = d_eval_unfold->unfold(ret);
}
if( ret.getNumChildren()>0 ){
std::vector< Node > children;
}
bool childChanged = false;
for( unsigned i=0; i<ret.getNumChildren(); i++ ){
- Node nc = evaluateWithUnfolding( ret[i], visited );
+ Node nc = evaluateWithUnfolding(ret[i], visited);
childChanged = childChanged || nc!=ret[i];
children.push_back( nc );
}
}
}
-Node TermDbSygus::evaluateWithUnfolding( Node n ) {
+Node TermDbSygus::evaluateWithUnfolding(Node n)
+{
std::unordered_map<Node, Node, NodeHashFunction> visited;
- return evaluateWithUnfolding( n, visited );
+ return evaluateWithUnfolding(n, visited);
}
bool TermDbSygus::isEvaluationPoint(Node n) const
static Node getAnchor( Node n );
static unsigned getAnchorDepth( Node n );
- public:
- /** unfold
- *
- * This method returns the one-step unfolding of an evaluation function
- * application. An example of a one step unfolding is:
- * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) )
- *
- * This function does this unfolding for a (possibly symbolic) evaluation
- * head, where the argument "variable to model" vtm stores the model value of
- * variables from this head. This allows us to track an explanation of the
- * unfolding in the vector exp when track_exp is true.
- *
- * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then
- * this method applied to eval( d, t ) will return
- * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp.
- */
- Node unfold(Node en,
- std::map<Node, Node>& vtm,
- std::vector<Node>& exp,
- bool track_exp = true);
- /**
- * Same as above, but without explanation tracking. This is used for concrete
- * evaluation heads
- */
- Node unfold(Node en);
};
}/* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff