item.getType().isSelector(),
item,
"arg must be a datatype constructor, selector, or tester");
+ return indexOfInternal(item);
+}
+
+size_t Datatype::indexOfInternal(Expr item)
+{
TNode n = Node::fromExpr(item);
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return indexOf( item[0] );
PrettyCheckArgument(item.getType().isSelector(),
item,
"arg must be a datatype selector");
+ return cindexOfInternal(item);
+}
+size_t Datatype::cindexOfInternal(Expr item)
+{
TNode n = Node::fromExpr(item);
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return cindexOf( item[0] );
*/
static size_t cindexOf(Expr item) CVC4_PUBLIC;
+ /**
+ * Same as above, but without checks. These methods should be used by
+ * internal (Node-level) code.
+ */
+ static size_t indexOfInternal(Expr item);
+ static size_t cindexOfInternal(Expr item);
+
/** The type for iterators over constructors. */
typedef DatatypeConstructorIterator iterator;
/** The (const) type for iterators over constructors. */
default = "-1"
read_only = true
help = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"
+
+[[option]]
+ name = "sygusEvalBuiltin"
+ category = "regular"
+ long = "sygus-eval-builtin"
+ type = "bool"
+ default = "true"
+ read_only = true
+ help = "use builtin kind for evaluation functions in sygus"
#include "theory/datatypes/datatypes_rewriter.h"
+using namespace CVC4;
+using namespace CVC4::kind;
+
namespace CVC4 {
namespace theory {
namespace datatypes {
}
}
TNode constructor = in[0].getOperator();
- size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+ size_t constructorIndex = indexOf(constructor);
const Datatype& dt = Datatype::datatypeOf(constructor.toExpr());
const DatatypeConstructor& c = dt[constructorIndex];
unsigned weight = c.getWeight();
return RewriteResponse(REWRITE_AGAIN_FULL, res);
}
}
+ else if (k == DT_SYGUS_EVAL)
+ {
+ // sygus evaluation function
+ Node ev = in[0];
+ if (ev.getKind() == APPLY_CONSTRUCTOR)
+ {
+ Trace("dt-sygus-util") << "Rewrite " << in << " by unfolding...\n";
+ const Datatype& dt =
+ static_cast<DatatypeType>(ev.getType().toType()).getDatatype();
+ unsigned i = indexOf(ev.getOperator());
+ Node op = Node::fromExpr(dt[i].getSygusOp());
+ // if it is the "any constant" constructor, return its argument
+ if (op.getAttribute(SygusAnyConstAttribute()))
+ {
+ Assert(ev.getNumChildren() == 1);
+ Assert(ev[0].getType().isComparableTo(in.getType()));
+ return RewriteResponse(REWRITE_AGAIN_FULL, ev[0]);
+ }
+ std::vector<Node> args;
+ for (unsigned j = 1, nchild = in.getNumChildren(); j < nchild; j++)
+ {
+ args.push_back(in[j]);
+ }
+ Assert(!dt.isParametric());
+ std::vector<Node> children;
+ for (const Node& evc : ev)
+ {
+ std::vector<Node> cc;
+ cc.push_back(evc);
+ cc.insert(cc.end(), args.begin(), args.end());
+ children.push_back(nm->mkNode(DT_SYGUS_EVAL, cc));
+ }
+ Node ret = mkSygusTerm(dt, i, children);
+ // if it is a variable, apply the substitution
+ if (ret.getKind() == BOUND_VARIABLE)
+ {
+ Assert(ret.hasAttribute(SygusVarNumAttribute()));
+ int vn = ret.getAttribute(SygusVarNumAttribute());
+ Assert(Node::fromExpr(dt.getSygusVarList())[vn] == ret);
+ ret = args[vn];
+ }
+ Trace("dt-sygus-util") << "...got " << ret << "\n";
+ return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+ }
+ }
if (k == kind::EQUAL)
{
return RewriteResponse(REWRITE_DONE, in);
}
+Kind getOperatorKindForSygusBuiltin(Node op)
+{
+ Assert(op.getKind() != BUILTIN);
+ if (op.getKind() == LAMBDA)
+ {
+ // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
+ // does beta-reduction but does not for APPLY
+ return APPLY_UF;
+ }
+ TypeNode tn = op.getType();
+ if (tn.isConstructor())
+ {
+ return APPLY_CONSTRUCTOR;
+ }
+ else if (tn.isSelector())
+ {
+ return APPLY_SELECTOR;
+ }
+ else if (tn.isTester())
+ {
+ return APPLY_TESTER;
+ }
+ else if (tn.isFunction())
+ {
+ return APPLY_UF;
+ }
+ return NodeManager::operatorToKind(op);
+}
+
+Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
+ unsigned i,
+ const std::vector<Node>& children)
+{
+ Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
+ << "] with children: " << children << std::endl;
+ Assert(i < dt.getNumConstructors());
+ Assert(dt.isSygus());
+ Assert(!dt[i].getSygusOp().isNull());
+ std::vector<Node> schildren;
+ Node op = Node::fromExpr(dt[i].getSygusOp());
+ // if it is the any constant, we simply return the child
+ if (op.getAttribute(SygusAnyConstAttribute()))
+ {
+ Assert(children.size() == 1);
+ return children[0];
+ }
+ if (op.getKind() != BUILTIN)
+ {
+ schildren.push_back(op);
+ }
+ schildren.insert(schildren.end(), children.begin(), children.end());
+ Node ret;
+ if (op.getKind() == BUILTIN)
+ {
+ ret = NodeManager::currentNM()->mkNode(op, schildren);
+ Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
+ return ret;
+ }
+ Kind ok = getOperatorKindForSygusBuiltin(op);
+ if (schildren.size() == 1 && ok == kind::UNDEFINED_KIND)
+ {
+ ret = schildren[0];
+ }
+ else
+ {
+ ret = NodeManager::currentNM()->mkNode(ok, schildren);
+ }
+ Trace("dt-sygus-util") << "...return " << ret << std::endl;
+ return ret;
+}
+Node DatatypesRewriter::mkSygusEvalApp(const std::vector<Node>& children)
+{
+ if (options::sygusEvalBuiltin())
+ {
+ return NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, children);
+ }
+ // otherwise, using APPLY_UF
+ Assert(!children.empty());
+ Assert(children[0].getType().isDatatype());
+ const Datatype& dt =
+ static_cast<DatatypeType>(children[0].getType().toType()).getDatatype();
+ Assert(dt.isSygus());
+ std::vector<Node> schildren;
+ schildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+ schildren.insert(schildren.end(), children.begin(), children.end());
+ return NodeManager::currentNM()->mkNode(APPLY_UF, schildren);
+}
+
+bool DatatypesRewriter::isSygusEvalApp(Node n)
+{
+ if (options::sygusEvalBuiltin())
+ {
+ return n.getKind() == DT_SYGUS_EVAL;
+ }
+ // otherwise, using APPLY_UF
+ if (n.getKind() != APPLY_UF || n.getNumChildren() == 0)
+ {
+ 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();
+}
+
RewriteResponse DatatypesRewriter::preRewrite(TNode in)
{
Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
Node op = in.getOperator();
// get the constructor object
const DatatypeConstructor& dtc =
- Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
+ Datatype::datatypeOf(op.toExpr())[indexOf(op)];
// create ascribed constructor type
Node tc = NodeManager::currentNM()->mkConst(
AscriptionType(dtc.getSpecializedConstructorType(t)));
TypeNode argType = in[0].getType();
TNode selector = in.getOperator();
TNode constructor = in[0].getOperator();
- size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+ size_t constructorIndex = indexOf(constructor);
const Datatype& dt = Datatype::datatypeOf(selector.toExpr());
const DatatypeConstructor& c = dt[constructorIndex];
Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : "
{
if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
{
- bool result = Datatype::indexOf(in.getOperator().toExpr())
- == Datatype::indexOf(in[0].getOperator().toExpr());
+ bool result = indexOf(in.getOperator()) == indexOf(in[0].getOperator());
Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
<< "Rewrite trivial tester " << in << " "
<< result << std::endl;
return RewriteResponse(REWRITE_DONE,
NodeManager::currentNM()->mkConst(true));
}
- // could try dt.getNumConstructors()==2 &&
- // Datatype::indexOf(in.getOperator())==1 ?
+ // could try dt.getNumConstructors()==2 && indexOf(in.getOperator())==1 ?
else if (!options::dtUseTesters())
{
- unsigned tindex = Datatype::indexOf(in.getOperator().toExpr());
+ unsigned tindex = indexOf(in.getOperator());
Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality "
<< in[0] << " " << tindex << std::endl;
Node neq = mkTester(in[0], tindex, dt);
{
if (n.getKind() == kind::APPLY_CONSTRUCTOR)
{
- int index = Datatype::indexOf(n.getOperator().toExpr());
+ int index = indexOf(n.getOperator());
const DatatypeConstructor& c = dt[index];
Type nt = n.getType().toType();
for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
if (n.getKind() == kind::APPLY_TESTER)
{
a = n[0];
- return Datatype::indexOf(n.getOperator().toExpr());
+ return indexOf(n.getOperator());
}
}
else
{
if (n.getKind() == kind::APPLY_TESTER)
{
- return Datatype::indexOf(n.getOperator().toExpr());
+ return indexOf(n.getOperator().toExpr());
}
}
else
return -1;
}
+struct DtIndexAttributeId
+{
+};
+typedef expr::Attribute<DtIndexAttributeId, uint64_t> DtIndexAttribute;
+
+unsigned DatatypesRewriter::indexOf(Node n)
+{
+ if (!n.hasAttribute(DtIndexAttribute()))
+ {
+ Assert(n.getType().isConstructor() || n.getType().isTester()
+ || n.getType().isSelector());
+ unsigned index = Datatype::indexOfInternal(n.toExpr());
+ n.setAttribute(DtIndexAttribute(), index);
+ return index;
+ }
+ return n.getAttribute(DtIndexAttribute());
+}
+
Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt)
{
if (options::dtUseTesters())
namespace CVC4 {
namespace theory {
+
+/** sygus var num */
+struct SygusVarNumAttributeId
+{
+};
+typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
+
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
namespace datatypes {
class DatatypesRewriter {
static int isTester(Node n, Node& a);
/** is tester, same as above but does not update an argument */
static int isTester(Node n);
+ /**
+ * Get the index of a constructor or tester in its datatype, or the
+ * index of a selector in its constructor. (Zero is always the
+ * first index.)
+ */
+ static unsigned indexOf(Node n);
/** make tester is-C( n ), where C is the i^{th} constructor of dt */
static Node mkTester(Node n, int i, const Datatype& dt);
/** make tester split
* C( x, y ) and z
*/
static bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
+ /** make sygus term
+ *
+ * This function returns a builtin term f( children[0], ..., children[n] )
+ * where f is the builtin op that the i^th constructor of sygus datatype dt
+ * encodes.
+ */
+ static Node mkSygusTerm(const Datatype& dt,
+ unsigned i,
+ const std::vector<Node>& children);
+ /** make sygus evaluation function application */
+ static Node mkSygusEvalApp(const std::vector<Node>& children);
+ /** is sygus evaluation function */
+ static bool isSygusEvalApp(Node n);
+ /**
+ * Get the builtin sygus operator for constructor term n of sygus datatype
+ * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus
+ * constructor whose sygus op is the builtin operator +, this method returns +.
+ */
+ static Node getSygusOpForCTerm(Node n);
private:
/** rewrite constructor term in */
}
void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) {
- d_active_terms.insert( n );
- Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp << std::endl;
-
TypeNode ntn = n.getType();
- const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
-
+ if (!ntn.isDatatype())
+ {
+ // nothing to do for non-datatype types
+ return;
+ }
+ const Datatype& dt = static_cast<DatatypeType>(ntn.toType()).getDatatype();
+ if (!dt.isSygus())
+ {
+ // nothing to do for non-sygus-datatype type
+ return;
+ }
+ d_active_terms.insert(n);
+ Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp
+ << std::endl;
+
// get the search size for this
Assert( d_term_to_anchor.find( n )!=d_term_to_anchor.end() );
Node a = d_term_to_anchor[n];
addSymBreakLemmasFor( ntn, n, d, lemmas );
}
+ Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n";
unsigned max_depth = ssz>=d ? ssz-d : 0;
unsigned min_depth = d_simple_proc[exp];
if( min_depth<=max_depth ){
for (unsigned ds = 0; ds <= max_depth; ds++)
{
// static conjecture-independent symmetry breaking
+ Trace("sygus-sb-debug") << " simple symmetry breaking...\n";
Node ipred = getSimpleSymBreakPred(ntn, tindex, ds, usingSymCons);
if (!ipred.isNull())
{
sb_lemmas.push_back(ipred);
}
// static conjecture-dependent symmetry breaking
+ Trace("sygus-sb-debug")
+ << " conjecture-dependent symmetry breaking...\n";
std::map<Node, quantifiers::CegConjecture*>::iterator itc =
d_anchor_to_conj.find(a);
if (itc != d_anchor_to_conj.end())
// now activate the children those testers were previously asserted in this
// context and are awaiting activation, if they exist.
if( options::sygusSymBreakLazy() ){
+ Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n );
Trace("sygus-sb-debug2") << " activate child sel : " << sel << std::endl;
assertTesterInternal( (*itt).second, sel, d_testers_exp[sel], lemmas );
}
}
+ Trace("sygus-sb-debug") << "...finished" << std::endl;
}
}
{
return it->second;
}
+ // this function is only called on sygus datatype types
+ Assert(tn.isDatatype());
NodeManager* nm = NodeManager::currentNM();
Node n = getFreeVar(tn);
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
Assert(tindex >= 0 && tindex < static_cast<int>(dt.getNumConstructors()));
+
+ Trace("sygus-sb-simple-debug")
+ << "Simple symmetry breaking for " << dt.getName() << ", constructor "
+ << dt[tindex].getName() << ", at depth " << depth << std::endl;
+
+ // if we are the "any constant" constructor, we do no symmetry breaking
+ // only do simple symmetry breaking up to depth 2
+ Node sop = Node::fromExpr(dt[tindex].getSygusOp());
+ if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2)
+ {
+ d_simple_sb_pred[tn][tindex][usingSymCons][depth] = Node::null();
+ return Node::null();
+ }
// conjunctive conclusion of lemma
std::vector<Node> sbp_conj;
if (depth == 0)
{
+ Trace("sygus-sb-simple-debug") << " Size..." << std::endl;
// fairness
if (options::sygusFair() == SYGUS_FAIR_DT_SIZE)
{
// symmetry breaking
Kind nk = d_tds->getConsNumKind(tn, tindex);
- // only do simple symmetry breaking up to depth 2
- if (options::sygusSymBreak() && depth < 2)
+ if (options::sygusSymBreak())
{
+ // the number of (sygus) arguments
unsigned dt_index_nargs = dt[tindex].getNumArgs();
+
// builtin type
TypeNode tnb = TypeNode::fromType(dt.getSygusType());
// get children
// direct solving for children
// for instance, we may want to insist that the LHS of MINUS is 0
+ Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl;
std::map<unsigned, unsigned> children_solved;
for (unsigned j = 0; j < dt_index_nargs; j++)
{
{
if (nk != UNDEFINED_KIND)
{
+ Trace("sygus-sb-simple-debug")
+ << " Equality reasoning about children..." << std::endl;
// commutative operators
if (quantifiers::TermUtil::isComm(nk))
{
{
const Datatype& cdt =
static_cast<DatatypeType>(tnc.toType()).getDatatype();
- Node guard_val = nm->mkNode(
- APPLY_CONSTRUCTOR,
- Node::fromExpr(cdt[anyc_cons_num_c].getConstructor()));
+ Node fv = d_tds->getFreeVar(tnc, 0);
+ Node guard_val = datatypes::DatatypesRewriter::getInstCons(
+ fv, cdt, anyc_cons_num_c);
Node exp = d_tds->getExplain()->getExplanationForEquality(
children[c1], guard_val);
sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq);
}
}
- Trace("sygus-sb-simple-debug") << "Process arguments for " << tn
- << " : " << nk << " : " << std::endl;
+ Trace("sygus-sb-simple-debug") << " Redundant operators..."
+ << std::endl;
// singular arguments (e.g. 0 for mult)
// redundant arguments (e.g. 0 for plus, 1 for mult)
// right-associativity
}
}
-bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, std::vector< Node >& lemmas ) {
- Assert( n.getType()==nv.getType() );
- Assert( nv.getKind()==APPLY_CONSTRUCTOR );
- TypeNode tn = n.getType();
- // currently bottom-up, could be top-down?
+Node SygusSymBreakNew::registerSearchValue(
+ Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas)
+{
+ Assert(n.getType().isComparableTo(nv.getType()));
+ TypeNode tn = n.getType();
+ if (!tn.isDatatype())
+ {
+ // don't register non-datatype terms, instead we return the
+ // selector chain n.
+ return n;
+ }
+ const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+ if (!dt.isSygus())
+ {
+ // don't register non-sygus-datatype terms
+ return n;
+ }
+ Assert(nv.getKind() == APPLY_CONSTRUCTOR);
+ NodeManager* nm = NodeManager::currentNM();
+ // we call the body of this function in a bottom-up fashion
+ // this ensures that the "abstraction" of the model value is available
if( nv.getNumChildren()>0 ){
- const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
- unsigned cindex = Datatype::indexOf( nv.getOperator().toExpr() );
- for( unsigned i=0; i<nv.getNumChildren(); i++ ){
- Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), n );
- if( !registerSearchValue( a, sel, nv[i], d+1, lemmas ) ){
- return false;
+ unsigned cindex = DatatypesRewriter::indexOf(nv.getOperator());
+ std::vector<Node> rcons_children;
+ rcons_children.push_back(nv.getOperator());
+ bool childrenChanged = false;
+ for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
+ {
+ Node sel = nm->mkNode(
+ APPLY_SELECTOR_TOTAL,
+ Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
+ n);
+ Node nvc = registerSearchValue(a, sel, nv[i], d + 1, lemmas);
+ if (nvc.isNull())
+ {
+ return Node::null();
}
+ rcons_children.push_back(nvc);
+ childrenChanged = childrenChanged || nvc != nv[i];
+ }
+ // reconstruct the value, which may be a skeleton
+ if (childrenChanged)
+ {
+ nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children);
}
}
Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl;
quantifiers::DivByZeroSygusInvarianceTest dbzet;
Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " << d_tds->sygusToBuiltin( nv ) << std::endl;
registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), lemmas);
- return false;
+ return Node::null();
}else{
std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv =
d_cache[a].d_search_val[tn].find(bvr);
Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
registerSymBreakLemmaForValue(a, bad_val, eset, bad_val_o, lemmas);
- return false;
+ return Node::null();
}
}
}
- return true;
+ return nv;
}
void SygusSymBreakNew::registerSymBreakLemmaForValue(
for( std::map< Node, bool >::iterator it = d_register_st.begin(); it != d_register_st.end(); ++it ){
if( it->second ){
Node prog = it->first;
+ Trace("dt-sygus-debug") << "Checking model value of " << prog << "..."
+ << std::endl;
+ Assert(prog.getType().isDatatype());
Node progv = d_td->getValuation().getModel()->getValue( prog );
if (Trace.isOn("dt-sygus"))
{
// register the search value ( prog -> progv ), this may invoke symmetry breaking
if( options::sygusSymBreakDynamic() ){
- if( !registerSearchValue( prog, prog, progv, 0, lemmas ) ){
+ Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas);
+ if (rsv.isNull())
+ {
Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
}
else
}
}
//register any measured terms that we haven't encountered yet (should only be invoked on first call to check
+ Trace("sygus-sb") << "Register size terms..." << std::endl;
std::vector< Node > mts;
d_tds->getEnumerators(mts);
for( unsigned i=0; i<mts.size(); i++ ){
int ind,
std::vector<Node>& lemmas)
{
- Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR );
+ if (vn.getKind() != kind::APPLY_CONSTRUCTOR)
+ {
+ // all datatype terms should be constant here
+ Assert(!vn.getType().isDatatype());
+ return true;
+ }
if( Trace.isOn("sygus-sb-warn") ){
Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n );
Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz );
}
TypeNode tn = n.getType();
const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
- int cindex = Datatype::indexOf( vn.getOperator().toExpr() );
+ int cindex = DatatypesRewriter::indexOf(vn.getOperator());
Node tst = DatatypesRewriter::mkTester( n, cindex, dt );
bool hastst = d_td->getValuation().getModel()->hasTerm( tst );
Node tstrep = d_td->getValuation().getModel()->getRepresentative( tst );
* z -> t for all terms t of appropriate depth, including d.
* This function strengthens blocking clauses using generalization techniques
* described in Reynolds et al SYNT 2017.
- */
- bool registerSearchValue( Node a, Node n, Node nv, unsigned d, std::vector< Node >& lemmas );
+ *
+ * The return value of this function is an abstraction of model assignment
+ * of nv to n, or null if we wish to exclude the model assignment nv to n.
+ * The return value of this method is different from nv itself, e.g. if it
+ * contains occurrences of the "any constant" constructor. For example, if
+ * nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this
+ * function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ),
+ * where n.1.0 is the appropriate selector chain applied to n. We build this
+ * abstraction since the semantics of C_{any_constant} is "any constant" and
+ * not "some constant". Thus, we should consider the subterm
+ * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented
+ * by a selector chain), instead of the concrete value 5.
+ */
+ Node registerSearchValue(
+ Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas);
/** Register symmetry breaking lemma
*
* This function adds the symmetry breaking lemma template lem for terms of
operator DT_SYGUS_BOUND 2 "datatypes sygus bound"
typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule
+operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function"
+typerule DT_SYGUS_EVAL ::CVC4::theory::datatypes::DtSyguEvalTypeRule
+
endtheory
d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
//d_equalityEngine.addFunctionKind(kind::DT_SIZE);
//d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND);
- //d_equalityEngine.addFunctionKind(kind::DT_SYGUS_TERM_ORDER);
- //d_equalityEngine.addFunctionKind(kind::DT_SYGUS_IS_CONST);
d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
//d_equalityEngine.addFunctionKind(kind::APPLY_UF);
quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
Assert( tds!=NULL );
d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() );
+ // do congruence on evaluation functions
+ d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL);
}
}
Node selector_use;
TypeNode ndt = n[0].getType();
if( options::dtSharedSelectors() ){
- size_t selectorIndex = Datatype::indexOf(selectorExpr);
+ size_t selectorIndex = DatatypesRewriter::indexOf(selector);
Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
Assert( selectorIndex<c.getNumArgs() );
selector_use = Node::fromExpr( c.getSelectorInternal( ndt.toType(), selectorIndex ) );
int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
if( eqc && !eqc->d_constructor.get().isNull() ){
- return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() );
+ return DatatypesRewriter::indexOf(eqc->d_constructor.get().getOperator());
}else{
Node lbl = getLabel( n );
if( lbl.isNull() ){
int tindex = DatatypesRewriter::isTester( lbl );
Assert( tindex!=-1 );
return tindex;
- //return Datatype::indexOf( getLabel( n ).getOperator().toExpr() );
}
}
}
for( int i=0; i<n_lbl; i++ ){
Node t = d_labels_data[n][i];
Assert( t.getKind()==NOT );
- //pcons[ Datatype::indexOf( t[0].getOperator().toExpr() ) ] = false;
int tindex = DatatypesRewriter::isTester( t[0] );
Assert( tindex!=-1 );
pcons[ tindex ] = false;
Assert( ti.getKind()==NOT );
j = ti;
jt = j[0];
- //int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
int jtindex = DatatypesRewriter::isTester( jt );
Assert( jtindex!=-1 );
if( jtindex==ttindex ){
//check labels
NodeIntMap::iterator lbl_i = d_labels.find( n );
if( lbl_i != d_labels.end() ){
- size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
+ size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
int n_lbl = (*lbl_i).second;
for( int i=0; i<n_lbl; i++ ){
Node t = d_labels_data[n][i];
}
if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
Expr selectorExpr = s.getOperator().toExpr();
- size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
+ size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
const Datatype& dt = Datatype::datatypeOf(selectorExpr);
const DatatypeConstructor& dtc = dt[constructorIndex];
int selectorIndex = dtc.getSelectorIndexInternal( selectorExpr );
//if( wrong ){
// return;
//}
- //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){
- // mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() );
- // r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
- //}else{
r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
if( options::dtRefIntro() ){
use_s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), use_s );
Node r = d_equalityEngine.getRepresentative( n );
EqcInfo * ei = getOrMakeEqcInfo( r, false );
int l_index = getLabelIndex( ei, r );
- int t_index = (int)Datatype::indexOf( atom.getOperator().toExpr() );
+ int t_index =
+ static_cast<int>(DatatypesRewriter::indexOf(atom.getOperator()));
Trace("dt-entail") << " Tester indices are " << t_index << " and " << l_index << std::endl;
if( l_index!=-1 && (l_index==t_index)==pol ){
std::vector< TNode > exp_c;
}
}; /* class DtSygusBoundTypeRule */
+class DtSyguEvalTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ TypeNode headType = n[0].getType(check);
+ if (!headType.isDatatype())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "datatype sygus eval takes a datatype head");
+ }
+ const Datatype& dt =
+ static_cast<DatatypeType>(headType.toType()).getDatatype();
+ if (!dt.isSygus())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "datatype sygus eval must have a datatype head that is sygus");
+ }
+ if (check)
+ {
+ Node svl = Node::fromExpr(dt.getSygusVarList());
+ if (svl.getNumChildren() + 1 != n.getNumChildren())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "wrong number of arguments to a "
+ "datatype sygus evaluation "
+ "function");
+ }
+ for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++)
+ {
+ TypeNode vtype = svl[i].getType(check);
+ TypeNode atype = n[i + 1].getType(check);
+ if (!vtype.isComparableTo(atype))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "argument type mismatch in a datatype sygus evaluation function");
+ }
+ }
+ }
+ return TypeNode::fromType(dt.getSygusType());
+ }
+}; /* class DtSygusBoundTypeRule */
+
} /* CVC4::theory::datatypes namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
Debug("dt-enum-debug") << "done : " << t << std::endl;
Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
// start with the constructor for which a ground term is constructed
- d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
+ d_zeroCtor = datatypes::DatatypesRewriter::indexOf(t.getOperator());
d_has_debruijn = 0;
}
Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
d_ceg_cegis(new Cegis(qe, this)),
d_ceg_cegisUnif(new CegisUnif(qe, this)),
d_master(nullptr),
+ d_set_ce_sk_vars(false),
d_repair_index(0),
d_refine_count(0),
d_syntax_guided(false)
}
}
-bool CegConjecture::needsRefinement() {
- return !d_ce_sk.empty();
-}
-
+bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
void CegConjecture::doCheck(std::vector<Node>& lems)
{
Assert(d_master != nullptr);
}
d_repair_index++;
if (d_sygus_rconst->repairSolution(
- d_candidates, fail_cvs, candidate_values))
+ d_candidates, fail_cvs, candidate_values, true))
{
constructed_cand = true;
}
recordInstantiation(candidate_values);
return;
}
- Assert( d_ce_sk.empty() );
+ Assert(!d_set_ce_sk_vars);
}else{
if( !constructed_cand ){
return;
}
//immediately skolemize inner existentials
- Node instr = Rewriter::rewrite(inst);
+ d_set_ce_sk_vars = sk_refine;
Node lem;
- if (instr.getKind() == NOT && instr[0].getKind() == FORALL)
+ if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
{
+ // introduce the skolem variables
+ std::vector<Node> sks;
if (constructed_cand)
{
- lem = d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate();
+ std::vector<Node> vars;
+ for (const Node& v : inst[0][0])
+ {
+ Node sk = nm->mkSkolem("rsk", v.getType());
+ sks.push_back(sk);
+ vars.push_back(v);
+ }
+ lem = inst[0][1].substitute(
+ vars.begin(), vars.end(), sks.begin(), sks.end());
+ lem = lem.negate();
}
if (sk_refine)
{
- Assert(!isGround());
- d_ce_sk.push_back(instr[0]);
+ d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
}
+ Assert(!isGround());
}
else
{
if (constructed_cand)
{
// use the instance itself
- lem = instr;
- }
- if (sk_refine)
- {
- // we add null so that one test of the conjecture for the empty
- // substitution is checked
- d_ce_sk.push_back(Node::null());
+ lem = inst;
}
+ // we add null so that one test of the conjecture for the empty
+ // substitution is checked
}
if (!lem.isNull())
{
void CegConjecture::doRefine( std::vector< Node >& lems ){
Assert( lems.empty() );
- Assert( d_ce_sk.size()==1 );
+ Assert(d_set_ce_sk_vars);
//first, make skolem substitution
Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl;
std::vector< Node > sk_vars;
std::vector< Node > sk_subs;
//collect the substitution over all disjuncts
- Node ce_q = d_ce_sk[0];
- if (!ce_q.isNull())
+ if (!d_ce_sk_vars.empty())
{
- std::vector<Node> skolems;
- d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems);
- Assert(d_inner_vars.size() == skolems.size());
+ Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
+ Assert(d_inner_vars.size() == d_ce_sk_vars.size());
std::vector<Node> model_values;
- getModelValues(skolems, model_values);
+ getModelValues(d_ce_sk_vars, model_values);
sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end());
sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end());
}
std::vector< Node > lem_c;
Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl;
Trace("cegqi-refine-debug")
- << " For counterexample point : " << ce_q << std::endl;
+ << " For counterexample skolems : " << d_ce_sk_vars << std::endl;
Node base_lem;
- if (!ce_q.isNull())
+ if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
{
- Assert(d_base_inst.getKind() == kind::NOT
- && d_base_inst[0].getKind() == kind::FORALL);
base_lem = d_base_inst[0][1];
}
else
Assert( sk_vars.size()==sk_subs.size() );
- Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl;
-
+ Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+ Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
base_lem = Rewriter::rewrite( base_lem );
+ Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
+ << "..." << std::endl;
d_master->registerRefinementLemma(sk_vars, base_lem, lems);
-
- d_ce_sk.clear();
+ Trace("cegqi-refine") << "doRefine : finished" << std::endl;
+ d_set_ce_sk_vars = false;
+ d_ce_sk_vars.clear();
}
void CegConjecture::preregisterConjecture( Node q ) {
void CegConjecture::debugPrint( const char * c ) {
Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
- Trace(c) << " * Candidate program/output symbol : ";
- for( unsigned i=0; i<d_candidates.size(); i++ ){
- Trace(c) << d_candidates[i] << " ";
- }
- Trace(c) << std::endl;
- Trace(c) << " * Candidate ce skolems : ";
- for( unsigned i=0; i<d_ce_sk.size(); i++ ){
- Trace(c) << d_ce_sk[i] << " ";
- }
+ Trace(c) << " * Candidate programs : " << d_candidates << std::endl;
+ Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl;
}
Node CegConjecture::getCurrentStreamGuard() const {
// We will not refine the current candidate solution since it is a solution
// thus, we clear information regarding the current refinement
- d_ce_sk.clear();
+ d_set_ce_sk_vars = false;
+ d_ce_sk_vars.clear();
// However, we need to exclude the current solution using an explicit
// blocking clause, so that we proceed to the next solution.
std::vector<Node> terms;
/** whether the conjecture is waiting for a call to doCheck below */
bool needsCheck( std::vector< Node >& lem );
/** whether the conjecture is waiting for a call to doRefine below */
- bool needsRefinement();
+ bool needsRefinement() const;
/** do single invocation check
* This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015.
*/
/** list of variables on inner quantification */
std::vector< Node > d_inner_vars;
/**
- * The set of current existentially quantified formulas whose couterexamples
- * we must refine. This may be added to during calls to doCheck(). The model
- * values for skolems of these formulas are analyzed during doRefine().
+ * The set of skolems for the current "verification" lemma, if one exists.
+ * This may be added to during calls to doCheck(). The model values for these
+ * skolems are analyzed during doRefine().
*/
- std::vector<Node> d_ce_sk;
+ std::vector<Node> d_ce_sk_vars;
+ /**
+ * Whether the above vector has been set. We have this flag since the above
+ * vector may be set to empty (e.g. for ground synthesis conjectures).
+ */
+ bool d_set_ce_sk_vars;
/** the asserted (negated) conjecture */
Node d_quant;
Node sc;
d_builtin_const_to_sygus[tn][c] = sc;
Assert(c.isConst());
- Assert(tn.isDatatype());
+ if (!tn.isDatatype())
+ {
+ // if we've traversed to a builtin type, simply return c
+ d_builtin_const_to_sygus[tn][c] = c;
+ return c;
+ }
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in "
<< dt.getName() << std::endl;
- Assert(dt.isSygus());
+ if (!dt.isSygus())
+ {
+ // if we've traversed to a builtin datatype type, simply return c
+ d_builtin_const_to_sygus[tn][c] = c;
+ return c;
+ }
// if we are not interested in reconstructing constants, or the grammar allows
// them, return a proxy
if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst())
}
TermDbSygus* tds = d_qe->getTermDatabaseSygus();
Assert(tds->isRegistered(tn));
- std::map<TypeNode, int> var_count;
- std::map<int, Node> pre;
- Node g = tds->mkGeneric(dt, c, var_count, pre);
+ Node g = tds->mkGeneric(dt, c);
Trace("csi-sol-debug") << "Generic is " << g << std::endl;
Node gr = Rewriter::rewrite(g);
Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl;
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace std;
void SygusEvalUnfold::registerEvalTerm(Node n)
{
Assert(options::sygusEvalUnfold());
- // is this an APPLY_UF term with head that is a sygus datatype term?
- if (n.getKind() != APPLY_UF)
+ // is this a sygus evaluation function application?
+ if (!datatypes::DatatypesRewriter::isSygusEvalApp(n))
{
return;
}
- TypeNode tn = n[0].getType();
- if (!tn.isDatatype())
- {
- return;
- }
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
- if (!dt.isSygus())
- {
- return;
- }
- Node f = n.getOperator();
- if (n[0].getKind() == APPLY_CONSTRUCTOR)
- {
- // constructors should be unfolded and reduced already
- return;
- }
if (d_eval_processed.find(n) != d_eval_processed.end())
{
return;
Trace("sygus-eval-unfold")
<< "SygusEvalUnfold: register eval term : " << n << std::endl;
d_eval_processed.insert(n);
- // is it the sygus evaluation function?
- Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
- if (n.getOperator() != eval_op)
+ TypeNode tn = n[0].getType();
+ // since n[0] is an evaluation head, we know tn is a sygus datatype
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ if (n[0].getKind() == APPLY_CONSTRUCTOR)
{
+ // constructors should be unfolded and reduced already
+ Assert(false);
return;
}
// register this evaluation term with its head
antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
// Node antec = n.eqNode( vn );
TypeNode tn = n.getType();
+ // n occurs as an evaluation head, thus it has sygus datatype type
Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Assert(dt.isSygus());
}
// evaluation children
std::vector<Node> eval_children;
- eval_children.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
eval_children.push_back(n);
// for each evaluation
for (unsigned i = start; i < curr_size; i++)
vtm[n] = vn;
eval_children.insert(
eval_children.end(), it->second[i].begin(), it->second[i].end());
- Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
- eval_children.resize(2);
+ Node eval_fun =
+ datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+ eval_children.resize(1);
res = d_tds->unfold(eval_fun, vtm, exp);
expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
}
EvalSygusInvarianceTest esit;
eval_children.insert(
eval_children.end(), it->second[i].begin(), it->second[i].end());
- Node conj = nm->mkNode(APPLY_UF, eval_children);
- eval_children[1] = vn;
- Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
+ Node conj =
+ datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+ eval_children[0] = vn;
+ Node eval_fun =
+ datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
res = d_tds->evaluateWithUnfolding(eval_fun);
esit.init(conj, n, res);
- eval_children.resize(2);
- eval_children[1] = n;
+ eval_children.resize(1);
+ eval_children[0] = n;
// evaluate with minimal explanation
std::vector<Node> mexp;
std::vector<Node>& exp,
std::map<unsigned, bool>& cexc)
{
- Assert(n.getType() == vn.getType());
+ // since builtin types occur in grammar, types are comparable but not
+ // necessarily equal
+ Assert(n.getType().isComparableTo(n.getType()));
if (n == vn)
{
return;
}
- Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
TypeNode tn = n.getType();
- Assert(tn.isDatatype());
+ if (!tn.isDatatype())
+ {
+ // sygus datatype fields that are not sygus datatypes are treated as
+ // abstractions only, hence we disregard this field
+ return;
+ }
+ Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
- int i = Datatype::indexOf(vn.getOperator().toExpr());
+ int i = datatypes::DatatypesRewriter::indexOf(vn.getOperator());
Node tst = datatypes::DatatypesRewriter::mkTester(n, i, dt);
exp.push_back(tst);
for (unsigned j = 0; j < vn.getNumChildren(); j++)
int& sz)
{
Assert(vnr.isNull() || vn != vnr);
+ Assert(n.getType().isComparableTo(vn.getType()));
+ TypeNode ntn = n.getType();
+ if (!ntn.isDatatype())
+ {
+ // sygus datatype fields that are not sygus datatypes are treated as
+ // abstractions only, hence we disregard this field
+ return;
+ }
Assert(vn.getKind() == APPLY_CONSTRUCTOR);
Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR);
- Assert(n.getType() == vn.getType());
- TypeNode ntn = n.getType();
std::map<unsigned, bool> cexc;
// for each child,
// check whether replacing that child by a fresh variable
}
}
const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
- int cindex = Datatype::indexOf(vn.getOperator().toExpr());
+ int cindex = datatypes::DatatypesRewriter::indexOf(vn.getOperator());
Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
Node tst = datatypes::DatatypesRewriter::mkTester(n, cindex, dt);
exp.push_back(tst);
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
-#include "theory/quantifiers/sygus/sygus_process_conj.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
+#include "theory/quantifiers/sygus/sygus_process_conj.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
op = cur;
}
// is the operator a synth function?
+ bool makeEvalFun = false;
if( !op.isNull() ){
std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
if( its!=synth_fun_vars.end() ){
- Assert( its->second.getType().isDatatype() );
- // will make into an application of an evaluation function
- const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
- Assert( dt.isSygus() );
- children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
children.push_back( its->second );
- childChanged = true;
- ret_k = kind::APPLY_UF;
+ makeEvalFun = true;
}
}
- if( !childChanged ){
+ if (!makeEvalFun)
+ {
// otherwise, we apply the previous operator
if( cur.getMetaKind() == kind::metakind::PARAMETERIZED ){
children.push_back( cur.getOperator() );
childChanged = childChanged || cur[i] != it->second;
children.push_back(it->second);
}
- if (childChanged) {
+ if (makeEvalFun)
+ {
+ // will make into an application of an evaluation function
+ ret = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
+ }
+ else if (childChanged)
+ {
ret = NodeManager::currentNM()->mkNode(ret_k, children);
}
visited[cur] = ret;
#include "printer/sygus_print_callback.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
std::stringstream ss;
ss << d_unres_tn << "_any_constant";
std::string cname(ss.str());
- std::vector<Type> empty_arg_types;
+ std::vector<Type> builtin_arg;
+ builtin_arg.push_back(dt.getSygusType());
// we add this constructor first since we use left associative chains
// and our symmetry breaking should group any constants together
// beneath the same application
- d_dt.addSygusConstructor(av.toExpr(), cname, empty_arg_types);
+ // we set its weight to zero since it should be considered at the
+ // same level as constants.
+ d_dt.addSygusConstructor(av.toExpr(), cname, builtin_arg, nullptr, 0);
}
}
for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
class SygusGrammarNorm;
-/** Attribute true for variables that represent any constant */
-struct SygusAnyConstAttributeId
-{
-};
-typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
-
/** Operator position trie class
*
* This data structure stores an unresolved type corresponding to the
visited[n] = true;
Node neval;
Node n_output;
- if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
+ bool neval_is_evalapp = false;
+ if (datatypes::DatatypesRewriter::isSygusEvalApp(n))
+ {
neval = n;
if( hasPol ){
n_output = !pol ? d_true : d_false;
}
+ neval_is_evalapp = true;
}else if( n.getKind()==EQUAL && hasPol && !pol ){
for( unsigned r=0; r<2; r++ ){
- if( n[r].getKind()==APPLY_UF && n[r].getNumChildren()>0 ){
+ if (datatypes::DatatypesRewriter::isSygusEvalApp(n[r]))
+ {
neval = n[r];
if( n[1-r].isConst() ){
n_output = n[1-r];
}
+ neval_is_evalapp = true;
}
}
}
- if( !neval.isNull() ){
- if( neval.getKind()==APPLY_UF && neval.getNumChildren()>0 ){
- // is it an evaluation function?
- if( d_examples.find( neval[0] )!=d_examples.end() ){
- std::map< Node, bool >::iterator itx = d_examples_invalid.find( neval[0] );
- if( itx==d_examples_invalid.end() ){
- //collect example
- bool success = true;
- std::vector< Node > ex;
- for( unsigned j=1; j<neval.getNumChildren(); j++ ){
- if( !neval[j].isConst() ){
- success = false;
- break;
- }else{
- ex.push_back( neval[j] );
- }
- }
- if( success ){
- d_examples[neval[0]].push_back( ex );
- d_examples_out[neval[0]].push_back( n_output );
- d_examples_term[neval[0]].push_back( neval );
- if( n_output.isNull() ){
- d_examples_out_invalid[neval[0]] = true;
- }else{
- Assert( n_output.isConst() );
- }
- //finished processing this node
- return;
- }else{
- d_examples_invalid[neval[0]] = true;
- d_examples_out_invalid[neval[0]] = true;
- }
+ // is it an evaluation function?
+ if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
+ {
+ // get the evaluation head
+ Node eh = neval[0];
+ std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
+ if (itx == d_examples_invalid.end())
+ {
+ // collect example
+ bool success = true;
+ std::vector<Node> ex;
+ for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
+ {
+ if (!neval[j].isConst())
+ {
+ success = false;
+ break;
+ }
+ ex.push_back(neval[j]);
+ }
+ if (success)
+ {
+ d_examples[eh].push_back(ex);
+ d_examples_out[eh].push_back(n_output);
+ d_examples_term[eh].push_back(neval);
+ if (n_output.isNull())
+ {
+ d_examples_out_invalid[eh] = true;
+ }
+ else
+ {
+ Assert(n_output.isConst());
}
+ // finished processing this node
+ return;
}
+ d_examples_invalid[eh] = true;
+ d_examples_out_invalid[eh] = true;
}
}
for( unsigned i=0; i<n.getNumChildren(); i++ ){
#include <stack>
#include "expr/datatype.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
if (tprocessed.find(tn) == tprocessed.end())
{
tprocessed[tn] = true;
- Assert(tn.isDatatype());
+ if (!tn.isDatatype())
+ {
+ // may have recursed to a non-datatype, e.g. in the case that we have
+ // "any constant" constructors
+ return;
+ }
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
- Assert(dt.isSygus());
+ if (!dt.isSygus())
+ {
+ // may have recursed to a non-sygus-datatype
+ return;
+ }
// check if this datatype allows all constants
if (dt.getSygusAllowConst())
{
TypeNode tn = n.getType();
Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
- Assert(dt.isSygus());
- Node op = n.getOperator();
- unsigned cindex = Datatype::indexOf(op.toExpr());
- if (dt[cindex].getNumArgs() > 0)
+ if (!dt.isSygus())
{
return false;
}
+ Node op = n.getOperator();
+ unsigned cindex = datatypes::DatatypesRewriter::indexOf(op);
Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
if (sygusOp.getAttribute(SygusAnyConstAttribute()))
{
// if it represents "any constant" then it is repairable
return true;
}
+ if (dt[cindex].getNumArgs() > 0)
+ {
+ return false;
+ }
if (useConstantsAsHoles && dt.getSygusAllowConst())
{
if (sygusOp.isConst())
if (it == visited.end())
{
visited[cur] = Node::null();
- if (cur.getKind() == APPLY_UF && cur.getNumChildren() > 0)
+ if (datatypes::DatatypesRewriter::isSygusEvalApp(cur))
{
Node v = cur[0];
if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
// We retrive model value now because purified node may not have a value
Node nv = n;
// Whether application of a function-to-synthesize
- bool fapp = k == APPLY_UF && size > 0;
+ bool fapp = datatypes::DatatypesRewriter::isSygusEvalApp(n);
bool u_fapp = false;
bool nu_fapp = false;
if (fapp)
Node nb;
if (childChanged)
{
- if (fapp && n.hasOperator())
+ if (n.getMetaKind() == metakind::PARAMETERIZED)
{
Trace("sygus-unif-rl-purify-debug") << "Node " << n
- << " has operator and fapp is true\n";
+ << " is parameterized\n";
children.insert(children.begin(), n.getOperator());
}
if (Trace.isOn("sygus-unif-rl-purify-debug"))
std::map<Node, Node>::const_iterator it = d_app_to_purified.find(nb);
if (it == d_app_to_purified.end())
{
- if (!childChanged)
- {
- Assert(nb.hasOperator());
- children.insert(children.begin(), n.getOperator());
- }
// Build purified head with fresh skolem and recreate node
std::stringstream ss;
ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
d_cand_to_eval_hds[nb[0]].push_back(new_f);
// Maps new enumerator to its respective tuple of arguments
d_hd_to_pt[new_f] =
- std::vector<Node>(children.begin() + 2, children.end());
+ std::vector<Node>(children.begin() + 1, children.end());
if (Trace.isOn("sygus-unif-rl-purify-debug"))
{
- Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> (";
+ Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> ( ";
for (const Node& pt_i : d_hd_to_pt[new_f])
{
Trace("sygus-unif-rl-purify-debug") << pt_i << " ";
Trace("sygus-unif-rl-purify-debug") << ")\n";
}
// replace first child and rebulid node
- children[1] = new_f;
- Assert(children.size() > 1);
- np = NodeManager::currentNM()->mkNode(k, children);
+ Assert(children.size() > 0);
+ children[0] = new_f;
+ Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children
+ << std::endl;
+ np = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
d_app_to_purified[nb] = np;
}
else
Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end());
std::vector<Node> pt = d_dt->d_unif->d_hd_to_pt[n];
// compute the result
- Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
if (Trace.isOn("sygus-unif-rl-sep"))
{
- Trace("sygus-unif-rl-sep") << "...got res = " << res << " from cond "
- << builtin_cond << " on pt " << n << " ( ";
+ Trace("sygus-unif-rl-sep") << "Evaluate cond " << builtin_cond << " on pt "
+ << n << " ( ";
for (const Node& pti : pt)
{
Trace("sygus-unif-rl-sep") << pti << " ";
}
Trace("sygus-unif-rl-sep") << ")\n";
}
+ Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
+ Trace("sygus-unif-rl-sep") << "...got res = " << res << "\n";
// If condition is templated, recompute result accordingly
Node templ = d_dt->d_template.first;
TNode templ_var = d_dt->d_template.second;
}
// look at information on how we will construct solutions for this type
+ // we know this is a sygus datatype since it is either the top-level type
+ // in the strategy graph, or was recursed by a strategy we inferred.
Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Assert(dt.isSygus());
}
Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
std::vector<Node> echildren;
- echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
echildren.push_back(ut);
Node sbvl = Node::fromExpr(dt.getSygusVarList());
for (const Node& sbv : sbvl)
{
echildren.push_back(sbv);
}
- Node eut = nm->mkNode(APPLY_UF, echildren);
+ Node eut = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren);
Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
<< std::endl;
eut = d_qe->getTermDatabaseSygus()->unfold(eut);
for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
{
Assert(sks[k].getType().isDatatype());
- const Datatype& cdt =
- static_cast<DatatypeType>(sks[k].getType().toType()).getDatatype();
- echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc());
- echildren[1] = sks[k];
+ echildren[0] = sks[k];
Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
<< std::endl;
- Node esk = nm->mkNode(APPLY_UF, echildren);
+ Node esk = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren);
vs.push_back(esk);
Node tvar = nm->mkSkolem("templ", esk.getType());
templ_var_index[tvar] = k;
continue;
}
EnumTypeInfoStrat* etis = snode.d_strats[j];
- unsigned cindex =
- static_cast<unsigned>(Datatype::indexOf(etis->d_cons.toExpr()));
+ unsigned cindex = datatypes::DatatypesRewriter::indexOf(etis->d_cons);
// constructors that correspond to strategies are not needed
// the intuition is that the strategy itself is responsible for constructing
// all terms that use the given constructor
#include "base/cvc4_check.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
Assert( dt.isSygus() );
Assert( !dt[c].getSygusOp().isNull() );
std::vector< Node > children;
- Node op = Node::fromExpr( dt[c].getSygusOp() );
- if( op.getKind()!=BUILTIN ){
- children.push_back( op );
- }
- Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl;
+ Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..."
+ << std::endl;
for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
{
- TypeNode tna = getArgType( dt[c], i );
Node a;
std::map< int, Node >::iterator it = pre.find( i );
if( it!=pre.end() ){
a = it->second;
}else{
+ TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
a = getFreeVarInc( tna, var_count, true );
}
Trace("sygus-db-debug")
Assert( !a.isNull() );
children.push_back( a );
}
- Node ret;
- if( op.getKind()==BUILTIN ){
- Trace("sygus-db-debug") << "Make builtin node..." << std::endl;
- ret = NodeManager::currentNM()->mkNode( op, children );
- }else{
- Kind ok = getOperatorKind( op );
- Trace("sygus-db-debug") << "Operator kind is " << ok << std::endl;
- if( children.size()==1 && ok==kind::UNDEFINED_KIND ){
- ret = children[0];
- }else{
- ret = NodeManager::currentNM()->mkNode( ok, children );
- }
- }
- Trace("sygus-db-debug") << "...returning " << ret << std::endl;
- return ret;
+ return datatypes::DatatypesRewriter::mkSygusTerm(dt, c, children);
}
Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
SygusToBuiltinAttribute;
-Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
- std::map<TypeNode, int> var_count;
- return sygusToBuiltin(n, tn, var_count);
-}
-
-Node TermDbSygus::sygusToBuiltin(Node n,
- TypeNode tn,
- std::map<TypeNode, int>& var_count)
+Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
{
Assert( n.getType()==tn );
- Assert( tn.isDatatype() );
-
+ if (!tn.isDatatype())
+ {
+ return n;
+ }
// has it already been computed?
- if (var_count.empty() && n.hasAttribute(SygusToBuiltinAttribute()))
+ if (n.hasAttribute(SygusToBuiltinAttribute()))
{
return n.getAttribute(SygusToBuiltinAttribute());
}
Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
<< ", type = " << tn << std::endl;
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ if (!dt.isSygus())
+ {
+ return n;
+ }
if (n.getKind() == APPLY_CONSTRUCTOR)
{
- bool var_count_empty = var_count.empty();
- unsigned i = Datatype::indexOf(n.getOperator().toExpr());
+ unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator());
Assert(n.getNumChildren() == dt[i].getNumArgs());
std::map<int, Node> pre;
for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
{
- // if the child is a symbolic constructor, do not include it
- if (!isSymbolicConsApp(n[j]))
- {
- pre[j] = sygusToBuiltin(
- n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count);
- }
+ pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
}
- Node ret = mkGeneric(dt, i, var_count, pre);
+ Node ret = mkGeneric(dt, i, pre);
Trace("sygus-db-debug")
<< "SygusToBuiltin : Generic is " << ret << std::endl;
- // cache if we had a fresh variable count
- if (var_count_empty)
- {
- n.setAttribute(SygusToBuiltinAttribute(), ret);
- }
+ // cache
+ n.setAttribute(SygusToBuiltinAttribute(), ret);
return ret;
}
if (n.hasAttribute(SygusPrintProxyAttribute()))
}
unsigned TermDbSygus::getSygusTermSize( Node n ){
- if( n.getNumChildren()==0 ){
+ if (n.getKind() != APPLY_CONSTRUCTOR)
+ {
return 0;
- }else{
- Assert(n.getKind() == APPLY_CONSTRUCTOR);
- unsigned sum = 0;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- sum += getSygusTermSize( n[i] );
- }
- const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
- int cindex = Datatype::indexOf(n.getOperator().toExpr());
- Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
- unsigned weight = dt[cindex].getWeight();
- return weight + sum;
}
+ unsigned sum = 0;
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ sum += getSygusTermSize(n[i]);
+ }
+ const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+ int cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
+ Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
+ unsigned weight = dt[cindex].getWeight();
+ return weight + sum;
}
class ReqTrie {
CVC4_CHECK(gtn.isSubtypeOf(btn))
<< "Sygus datatype " << dt.getName()
<< " encodes terms that are not of type " << btn << std::endl;
+ Trace("sygus-db") << "...done register Operator #" << i << std::endl;
}
// compute min type depth information
computeMinTypeDepthInternal(tn, tn, 0);
d_enum_to_active_guard[e] = eg;
}
+ Trace("sygus-db") << " registering symmetry breaking clauses..."
+ << std::endl;
d_enum_to_using_sym_cons[e] = useSymbolicCons;
// depending on if we are using symbolic constructors, introduce symmetry
// breaking lemma templates for each relevant subtype of the grammar
for (unsigned& rindex : rm_indices)
{
// make the apply-constructor corresponding to an application of the
- // "any constant" constructor
- Node exc_val = nm->mkNode(APPLY_CONSTRUCTOR,
- Node::fromExpr(dt[rindex].getConstructor()));
+ // constant or "any constant" constructor
+ // we call getInstCons since in the case of any constant constructors, it
+ // is necessary to generate a term of the form any_constant( x.0 ) for a
+ // fresh variable x.0.
+ Node fv = getFreeVar(stn, 0);
+ Node exc_val = datatypes::DatatypesRewriter::getInstCons(fv, dt, rindex);
// should not include the constuctor in any subterm
Node x = getFreeVar(stn, 0);
Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
}
}
+ Trace("sygus-db") << " ...finished" << std::endl;
}
bool TermDbSygus::isEnumerator(Node e) const
void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ) {
std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
if( it==d_min_type_depth[root_tn].end() || type_depth<it->second ){
+ if (!tn.isDatatype())
+ {
+ // do not recurse to non-datatype types
+ return;
+ }
d_min_type_depth[root_tn][tn] = type_depth;
- Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
//compute for connected types
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
return false;
}
TypeNode tn = n.getType();
+ Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Assert(dt.isSygus());
- unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+ unsigned cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
// it is symbolic if it represents "any constant"
return sygusOp.getAttribute(SygusAnyConstAttribute());
}
}
-Kind TermDbSygus::getOperatorKind( Node op ) {
- Assert( op.getKind()!=BUILTIN );
- if (op.getKind() == LAMBDA)
- {
- // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
- // does beta-reduction but does not for APPLY
- return APPLY_UF;
- }else{
- TypeNode tn = op.getType();
- if( tn.isConstructor() ){
- return APPLY_CONSTRUCTOR;
- }
- else if (tn.isSelector())
- {
- return APPLY_SELECTOR;
- }
- else if (tn.isTester())
- {
- return APPLY_TESTER;
- }
- else if (tn.isFunction())
- {
- return APPLY_UF;
- }
- return NodeManager::operatorToKind(op);
- }
-}
-
Node TermDbSygus::getAnchor( Node n ) {
if( n.getKind()==APPLY_SELECTOR_TOTAL ){
return getAnchor( n[0] );
}
Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
- if( en.getKind()==kind::APPLY_UF ){
- 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] );
- if( itv!=vtm.end() ){
- ev = itv->second;
- }else{
- Assert( false );
- }
- Assert( en[0].getType()==ev.getType() );
- Assert( ev.isConst() );
+ if (!datatypes::DatatypesRewriter::isSygusEvalApp(en))
+ {
+ 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( ev.getKind()==kind::APPLY_CONSTRUCTOR );
- std::vector< Node > args;
- for( unsigned i=1; i<en.getNumChildren(); i++ ){
- args.push_back( en[i] );
+ 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::DatatypesRewriter::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);
}
- const Datatype& dt = ((DatatypeType)(ev.getType()).toType()).getDatatype();
- unsigned i = Datatype::indexOf( ev.getOperator().toExpr() );
- if( track_exp ){
- //explanation
- Node ee = NodeManager::currentNM()->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];
}
- Assert( !dt.isParametric() );
- std::map< int, Node > pre;
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- std::vector< Node > cc;
- //get the evaluation argument for the selector
- Type rt = dt[i][j].getRangeType();
- const Datatype & ad = ((DatatypeType)dt[i][j].getRangeType()).getDatatype();
- cc.push_back( Node::fromExpr( ad.getSygusEvaluationFunc() ) );
- Node s;
- if( en[0].getKind()==kind::APPLY_CONSTRUCTOR ){
- s = en[0][j];
- }else{
- s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal( en[0].getType().toType(), 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] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc );
+ else
+ {
+ return nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
}
- Node ret = mkGeneric(dt, i, pre);
- // if it is a variable, apply the substitution
- if( ret.getKind()==kind::BOUND_VARIABLE ){
- Assert( ret.hasAttribute(SygusVarNumAttribute()) );
- int i = ret.getAttribute(SygusVarNumAttribute());
- Assert( Node::fromExpr( dt.getSygusVarList() )[i]==ret );
- ret = args[i];
+ }
+
+ 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
{
- ret = Rewriter::rewrite(ret);
+ s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
+ dt[i].getSelectorInternal(headType, j),
+ en[0]);
}
- return ret;
- }else{
- Assert( en.isConst() );
+ cc.push_back(s);
+ if (track_exp)
+ {
+ // update vtm map
+ vtm[s] = ev[j];
+ }
+ cc.insert(cc.end(), args.begin(), args.end());
+ pre[j] = datatypes::DatatypesRewriter::mkSygusEvalApp(cc);
+ }
+ Node ret = mkGeneric(dt, i, pre);
+ // if it is a variable, apply the substitution
+ if (ret.getKind() == kind::BOUND_VARIABLE)
+ {
+ Assert(ret.hasAttribute(SygusVarNumAttribute()));
+ int i = ret.getAttribute(SygusVarNumAttribute());
+ Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret);
+ return args[i];
}
- return en;
+ 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::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
std::map< Node, Node >::iterator itv = visited.find( n );
if( itv==visited.end() ){
Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
Node ret;
- if( n.getKind()==APPLY_UF ){
+ if (datatypes::DatatypesRewriter::isSygusEvalApp(n))
+ {
TypeNode tn = n[0].getType();
Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
if( tn.isDatatype() ){
visited.find(n);
if( it==visited.end() ){
Node ret = n;
- while( ret.getKind()==APPLY_UF && ret[0].getKind()==APPLY_CONSTRUCTOR ){
+ while (datatypes::DatatypesRewriter::isSygusEvalApp(ret)
+ && ret[0].getKind() == APPLY_CONSTRUCTOR)
+ {
ret = unfold( ret );
}
if( ret.getNumChildren()>0 ){
bool TermDbSygus::isEvaluationPoint(Node n) const
{
- if (n.getKind() != APPLY_UF || n.getNumChildren() == 0 || !n[0].isVar())
+ if (!datatypes::DatatypesRewriter::isSygusEvalApp(n))
+ {
+ return false;
+ }
+ if (!n[0].isVar())
{
return false;
}
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();
+ return true;
}
}/* CVC4::theory::quantifiers namespace */
*
* Given a sygus datatype term n of type tn, this function returns its analog,
* that is, the term that n encodes.
- *
- * Notice that each occurrence of a symbolic constructor application is
- * replaced by a unique variable. To track counters for introducing unique
- * variables, we use the var_count map.
*/
Node sygusToBuiltin(Node n, TypeNode tn);
- Node sygusToBuiltin(Node n, TypeNode tn, std::map<TypeNode, int>& var_count);
/** same as above, but without tn */
Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
/** evaluate builtin
Node getSemanticSkolem( TypeNode tn, Node n, bool doMk = true );
/** involves div-by-zero */
bool involvesDivByZero( Node n );
-
- /** get operator kind */
- static Kind getOperatorKind( Node op );
-
/** get anchor */
static Node getAnchor( Node n );
static unsigned getAnchorDepth( Node n );
bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg );
bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg );
int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg );
-public:
- Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp = true );
- Node unfold( Node en ){
- std::map< Node, Node > vtm;
- std::vector< Node > exp;
- return unfold( en, vtm, exp, false );
- }
+
+ 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);
Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
};
double rinc,
unsigned depth)
{
- Assert(tn.isDatatype());
+ if (!tn.isDatatype())
+ {
+ return getRandomValue(tn);
+ }
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
- Assert(dt.isSygus());
+ if (!dt.isSygus())
+ {
+ return getRandomValue(tn);
+ }
Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
Trace("sygus-sample-grammar")
<< "Sygus random value " << tn << ", depth = " << depth
if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end())
{
d_rvalue_cindices[tn].clear();
- Assert(tn.isDatatype());
+ if (!tn.isDatatype())
+ {
+ return;
+ }
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
- Assert(dt.isSygus());
+ if (!dt.isSygus())
+ {
+ return;
+ }
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
const DatatypeConstructor& dtc = dt[i];
struct QuantIdNumAttributeId {};
typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
-/** sygus var num */
-struct SygusVarNumAttributeId {};
-typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
-
/** Attribute to mark Skolems as virtual terms */
struct VirtualTermSkolemAttributeId {};
typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
projects / cvc5.git / commitdiff