theory/datatypes/theory_datatypes.cpp
theory/datatypes/theory_datatypes.h
theory/datatypes/theory_datatypes_type_rules.h
+ theory/datatypes/theory_datatypes_utils.cpp
+ theory/datatypes/theory_datatypes_utils.h
theory/datatypes/type_enumerator.cpp
theory/datatypes/type_enumerator.h
theory/decision_manager.cpp
#include "theory/datatypes/datatypes_rewriter.h"
#include "expr/node_algorithm.h"
+#include "options/datatypes_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
using namespace CVC4;
using namespace CVC4::kind;
}
}
TNode constructor = in[0].getOperator();
- size_t constructorIndex = indexOf(constructor);
+ size_t constructorIndex = utils::indexOf(constructor);
const Datatype& dt = Datatype::datatypeOf(constructor.toExpr());
const DatatypeConstructor& c = dt[constructorIndex];
unsigned weight = c.getWeight();
{
Trace("dt-sygus-util") << "Rewrite " << in << " by unfolding...\n";
const Datatype& dt = ev.getType().getDatatype();
- unsigned i = indexOf(ev.getOperator());
+ unsigned i = utils::indexOf(ev.getOperator());
Node op = Node::fromExpr(dt[i].getSygusOp());
// if it is the "any constant" constructor, return its argument
if (op.getAttribute(SygusAnyConstAttribute()))
cc.insert(cc.end(), args.begin(), args.end());
children.push_back(nm->mkNode(DT_SYGUS_EVAL, cc));
}
- Node ret = mkSygusTerm(dt, i, children);
+ Node ret = utils::mkSygusTerm(dt, i, children);
// apply the appropriate substitution
- ret = applySygusArgs(dt, op, ret, args);
+ ret = utils::applySygusArgs(dt, op, ret, args);
Trace("dt-sygus-util") << "...got " << ret << "\n";
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}
}
if (!cons.isNull())
{
- cases.push_back(mkTester(h, cindex, dt));
+ cases.push_back(utils::mkTester(h, cindex, dt));
}
else
{
return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
}
std::vector<Node> rew;
- if (checkClash(in[0], in[1], rew))
+ if (utils::checkClash(in[0], in[1], rew))
{
Trace("datatypes-rewrite")
<< "Rewrite clashing equality " << in << " to false" << std::endl;
return RewriteResponse(REWRITE_DONE, in);
}
-Node DatatypesRewriter::applySygusArgs(const Datatype& dt,
- Node op,
- Node n,
- const std::vector<Node>& args)
-{
- if (n.getKind() == BOUND_VARIABLE)
- {
- Assert(n.hasAttribute(SygusVarNumAttribute()));
- int vn = n.getAttribute(SygusVarNumAttribute());
- Assert(Node::fromExpr(dt.getSygusVarList())[vn] == n);
- return args[vn];
- }
- // n is an application of operator op.
- // We must compute the free variables in op to determine if there are
- // any substitutions we need to make to n.
- TNode val;
- if (!op.hasAttribute(SygusVarFreeAttribute()))
- {
- std::unordered_set<Node, NodeHashFunction> fvs;
- if (expr::getFreeVariables(op, fvs))
- {
- if (fvs.size() == 1)
- {
- for (const Node& v : fvs)
- {
- val = v;
- }
- }
- else
- {
- val = op;
- }
- }
- Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl;
- op.setAttribute(SygusVarFreeAttribute(), val);
- }
- else
- {
- val = op.getAttribute(SygusVarFreeAttribute());
- }
- if (val.isNull())
- {
- return n;
- }
- if (val.getKind() == BOUND_VARIABLE)
- {
- // single substitution case
- int vn = val.getAttribute(SygusVarNumAttribute());
- TNode sub = args[vn];
- return n.substitute(val, sub);
- }
- // do the full substitution
- std::vector<Node> vars;
- Node bvl = Node::fromExpr(dt.getSygusVarList());
- for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
- {
- vars.push_back(bvl[i]);
- }
- return n.substitute(vars.begin(), vars.end(), args.begin(), args.end());
-}
-
-Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op)
-{
- Assert(op.getKind() != BUILTIN);
- if (op.getKind() == LAMBDA)
- {
- 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 UNDEFINED_KIND;
-}
-
-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());
- Trace("dt-sygus-util") << "Operator is " << op << std::endl;
- if (children.empty())
- {
- // no children, return immediately
- Trace("dt-sygus-util") << "...return direct op" << std::endl;
- return op;
- }
- // 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 = NodeManager::operatorToKind(op);
- Trace("dt-sygus-util") << "operator kind is " << ok << std::endl;
- if (ok != UNDEFINED_KIND)
- {
- // If it is an APPLY_UF operator, we should have at least an operator and
- // a child.
- Assert(ok != APPLY_UF || schildren.size() != 1);
- ret = NodeManager::currentNM()->mkNode(ok, schildren);
- Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
- return ret;
- }
- Kind tok = getOperatorKindForSygusBuiltin(op);
- if (schildren.size() == 1 && tok == kind::UNDEFINED_KIND)
- {
- ret = schildren[0];
- }
- else
- {
- ret = NodeManager::currentNM()->mkNode(tok, schildren);
- }
- Trace("dt-sygus-util") << "...return " << ret << std::endl;
- return ret;
-}
-
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())[indexOf(op)];
+ Datatype::datatypeOf(op.toExpr())[utils::indexOf(op)];
// create ascribed constructor type
Node tc = NodeManager::currentNM()->mkConst(
AscriptionType(dtc.getSpecializedConstructorType(t)));
TypeNode argType = in[0].getType();
Expr selector = in.getOperator().toExpr();
TNode constructor = in[0].getOperator();
- size_t constructorIndex = indexOf(constructor);
+ size_t constructorIndex = utils::indexOf(constructor);
const Datatype& dt = Datatype::datatypeOf(selector);
const DatatypeConstructor& c = dt[constructorIndex];
Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : "
{
if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
{
- bool result = indexOf(in.getOperator()) == indexOf(in[0].getOperator());
+ bool result =
+ utils::indexOf(in.getOperator()) == utils::indexOf(in[0].getOperator());
Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
<< "Rewrite trivial tester " << in << " "
<< result << std::endl;
return RewriteResponse(REWRITE_DONE, in);
}
-bool DatatypesRewriter::checkClash(Node n1, Node n2, std::vector<Node>& rew)
-{
- Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2
- << std::endl;
- if (n1.getKind() == kind::APPLY_CONSTRUCTOR
- && n2.getKind() == kind::APPLY_CONSTRUCTOR)
- {
- if (n1.getOperator() != n2.getOperator())
- {
- Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " "
- << n2 << " " << n1.getOperator() << " "
- << n2.getOperator() << std::endl;
- return true;
- }
- Assert(n1.getNumChildren() == n2.getNumChildren());
- for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
- {
- if (checkClash(n1[i], n2[i], rew))
- {
- return true;
- }
- }
- }
- else if (n1 != n2)
- {
- if (n1.isConst() && n2.isConst())
- {
- Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " "
- << n2 << std::endl;
- return true;
- }
- else
- {
- Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
- rew.push_back(eq);
- }
- }
- return false;
-}
-/** get instantiate cons */
-Node DatatypesRewriter::getInstCons(Node n, const Datatype& dt, int index)
-{
- Assert(index >= 0 && index < (int)dt.getNumConstructors());
- std::vector<Node> children;
- NodeManager* nm = NodeManager::currentNM();
- children.push_back(Node::fromExpr(dt[index].getConstructor()));
- Type t = n.getType().toType();
- for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
- {
- Node nc = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[index].getSelectorInternal(t, i)),
- n);
- children.push_back(nc);
- }
- Node n_ic = nm->mkNode(kind::APPLY_CONSTRUCTOR, children);
- if (dt.isParametric())
- {
- TypeNode tn = TypeNode::fromType(t);
- // add type ascription for ambiguous constructor types
- if (!n_ic.getType().isComparableTo(tn))
- {
- Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for "
- << n_ic << ", ascribe to " << n.getType()
- << std::endl;
- Debug("datatypes-parametric") << "Constructor is " << dt[index]
- << std::endl;
- Type tspec =
- dt[index].getSpecializedConstructorType(n.getType().toType());
- Debug("datatypes-parametric") << "Type specification is " << tspec
- << std::endl;
- children[0] = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
- nm->mkConst(AscriptionType(tspec)),
- children[0]);
- n_ic = nm->mkNode(kind::APPLY_CONSTRUCTOR, children);
- Assert(n_ic.getType() == tn);
- }
- }
- Assert(isInstCons(n, n_ic, dt) == index);
- // n_ic = Rewriter::rewrite( n_ic );
- return n_ic;
-}
-
-int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt)
-{
- if (n.getKind() == kind::APPLY_CONSTRUCTOR)
- {
- 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[i].getKind() != kind::APPLY_SELECTOR_TOTAL
- || n[i].getOperator() != Node::fromExpr(c.getSelectorInternal(nt, i))
- || n[i][0] != t)
- {
- return -1;
- }
- }
- return index;
- }
- return -1;
-}
-
-int DatatypesRewriter::isTester(Node n, Node& a)
-{
- if (n.getKind() == kind::APPLY_TESTER)
- {
- a = n[0];
- return indexOf(n.getOperator());
- }
- return -1;
-}
-
-int DatatypesRewriter::isTester(Node n)
-{
- if (n.getKind() == kind::APPLY_TESTER)
- {
- return indexOf(n.getOperator().toExpr());
- }
- 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)
-{
- return NodeManager::currentNM()->mkNode(
- kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
-}
-
-Node DatatypesRewriter::mkSplit(Node n, const Datatype& dt)
-{
- std::vector<Node> splits;
- for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
- {
- Node test = mkTester(n, i, dt);
- splits.push_back(test);
- }
- NodeManager* nm = NodeManager::currentNM();
- return splits.size() == 1 ? splits[0] : nm->mkNode(kind::OR, splits);
-}
-
-bool DatatypesRewriter::isNullaryApplyConstructor(Node n)
-{
- Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
- for (unsigned i = 0; i < n.getNumChildren(); i++)
- {
- if (n[i].getType().isDatatype())
- {
- return false;
- }
- }
- return true;
-}
-
-bool DatatypesRewriter::isNullaryConstructor(const DatatypeConstructor& c)
-{
- for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
- {
- if (c[j].getType().getRangeType().isDatatype())
- {
- return false;
- }
- }
- return true;
-}
-
Node DatatypesRewriter::normalizeCodatatypeConstant(Node n)
{
Trace("dt-nconst") << "Normalize " << n << std::endl;
#define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
#include "expr/node_manager_attributes.h"
-#include "options/datatypes_options.h"
#include "theory/rewriter.h"
#include "theory/type_enumerator.h"
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;
-
-/**
- * Attribute true for enumerators whose current model values were registered by
- * the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
- * This is set by the datatypes sygus solver during LAST_CALL effort checks for
- * each active sygus enumerator.
- */
-struct SygusSymBreakOkAttributeId
-{
-};
-typedef expr::Attribute<SygusSymBreakOkAttributeId, bool>
- SygusSymBreakOkAttribute;
-
-/** sygus var free
- *
- * This attribute is used to mark whether sygus operators have free occurrences
- * of variables from the formal argument list of the function-to-synthesize.
- *
- * We store three possible cases for sygus operators op:
- * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null()
- * In this case, op has no free variables from the formal argument list of the
- * function-to-synthesize.
- * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable.
- * In this case, op has exactly one free variable, v.
- * (3) op.getAttribute(SygusVarFreeAttribute())==op
- * In this case, op has an arbitrary set (cardinality >1) of free variables from
- * the formal argument list of the function to synthesize.
- *
- * This attribute is used to compute applySygusArgs below.
- */
-struct SygusVarFreeAttributeId
-{
-};
-typedef expr::Attribute<SygusVarFreeAttributeId, Node> SygusVarFreeAttribute;
-
namespace datatypes {
class DatatypesRewriter {
static inline void init() {}
static inline void shutdown() {}
- /** get instantiate cons
- *
- * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
- * where C is the index^{th} constructor of datatype dt.
- */
- static Node getInstCons(Node n, const Datatype& dt, int index);
- /** is instantiation cons
- *
- * If this method returns a value >=0, then that value, call it index,
- * is such that n = C( sel^{C,1}( t ), ..., sel^{C,m}( t ) ),
- * where C is the index^{th} constructor of dt.
- */
- static int isInstCons(Node t, Node n, const Datatype& dt);
- /** is tester
- *
- * This method returns a value >=0 if n is a tester predicate. The return
- * value indicates the constructor index that the tester n is for. If this
- * method returns a value >=0, then it updates a to the argument that the
- * tester n applies to.
- */
- 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
- *
- * Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
- * are the constructors of n's type (dt).
- */
- static Node mkSplit(Node n, const Datatype& dt);
- /** returns true iff n is a constructor term with no datatype children */
- static bool isNullaryApplyConstructor(Node n);
- /** returns true iff c is a constructor with no datatype children */
- static bool isNullaryConstructor(const DatatypeConstructor& c);
+
/** normalize codatatype constant
*
* This returns the normal form of the codatatype constant n. This runs a
* on all top-level codatatype subterms of n.
*/
static Node normalizeConstant(Node n);
- /** check clash
- *
- * This method returns true if and only if n1 and n2 have a skeleton that has
- * conflicting constructors at some term position.
- * Examples of terms that clash are:
- * C( x, y ) and D( z )
- * C( D( x ), y ) and C( E( x ), y )
- * Examples of terms that do not clash are:
- * C( x, y ) and C( D( x ), y )
- * C( D( x ), y ) and C( x, E( z ) )
- * C( x, y ) and z
- */
- static bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
- /** get operator kind for sygus builtin
- *
- * This returns the Kind corresponding to applications of the operator op
- * when building the builtin version of sygus terms. This is used by the
- * function mkSygusTerm.
- */
- static Kind getOperatorKindForSygusBuiltin(Node op);
- /** 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);
- /**
- * n is a builtin term that is an application of operator op.
- *
- * This returns an n' such that (eval n args) is n', where n' is a instance of
- * n for the appropriate substitution.
- *
- * For example, given a function-to-synthesize with formal argument list (x,y),
- * say we have grammar:
- * A -> A+A | A+x | A+(x+y) | y
- * These lead to constructors with sygus ops:
- * C1 / (lambda w1 w2. w1+w2)
- * C2 / (lambda w1. w1+x)
- * C3 / (lambda w1. w1+(x+y))
- * C4 / y
- * Examples of calling this function:
- * applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } )
- * ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2).
- * applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } )
- * ... returns (APPLY_UF (lambda w1. w1+3) t1).
- * applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } )
- * ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1).
- * applySygusArgs( dt, C4, y, { 3, 5 } )
- * ... returns 5.
- * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4,
- * to cache the results of whether the evaluation of this constructor needs
- * a substitution over the formal argument list of the function-to-synthesize.
- */
- static Node applySygusArgs(const Datatype& dt,
- Node op,
- Node n,
- const std::vector<Node>& args);
- /**
- * 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 */
#include "expr/node_manager.h"
#include "options/base_options.h"
+#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/sygus_explain.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
std::vector<Node> case_conj;
for (unsigned k = 0; k < j; k++)
{
- case_conj.push_back(DatatypesRewriter::mkTester(n2, k, cdt).negate());
+ case_conj.push_back(utils::mkTester(n2, k, cdt).negate());
}
if (!case_conj.empty())
{
Node corder = nm->mkNode(
- kind::OR,
- DatatypesRewriter::mkTester(n1, j, cdt).negate(),
- case_conj.size() == 1 ? case_conj[0]
- : nm->mkNode(kind::AND, case_conj));
+ OR,
+ utils::mkTester(n1, j, cdt).negate(),
+ case_conj.size() == 1 ? case_conj[0] : nm->mkNode(AND, case_conj));
sz_eq_cases.push_back(corder);
}
}
int sindexi = dt[i].getSelectorIndexInternal(selExpr);
if (sindexi != -1)
{
- disj.push_back(DatatypesRewriter::mkTester(n[0], i, dt).negate());
+ disj.push_back(utils::mkTester(n[0], i, dt).negate());
}
else
{
}else{
int sindex = Datatype::cindexOf( selExpr );
Assert( sindex!=-1 );
- cond = DatatypesRewriter::mkTester(n[0], sindex, dt).negate();
+ cond = utils::mkTester(n[0], sindex, dt).negate();
}
Node c1 = getRelevancyCondition( n[0] );
if( cond.isNull() ){
if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant)
{
Node szl = nm->mkNode(DT_SIZE, n);
- Node szr =
- nm->mkNode(DT_SIZE, DatatypesRewriter::getInstCons(n, dt, tindex));
+ Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex));
szr = Rewriter::rewrite(szr);
sbp_conj.push_back(szl.eqNode(szr));
}
const Datatype& cdt =
static_cast<DatatypeType>(ctn.toType()).getDatatype();
Assert(i < static_cast<int>(cdt.getNumConstructors()));
- sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt));
+ sbp_conj.push_back(utils::mkTester(children[j], i, cdt));
}
}
{
Kind nck = cti.getConsNumKind(k);
bool red = false;
- Node tester = DatatypesRewriter::mkTester(nc, k, cdt);
+ Node tester = utils::mkTester(nc, k, cdt);
// check if the argument is redundant
if (static_cast<int>(k) == anyc_cons_num)
{
Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), 1)),
children[0]);
Assert(child11.getType() == children[1].getType());
- Node order_pred_trans = nm->mkNode(
- OR,
- DatatypesRewriter::mkTester(children[0], tindex, dt).negate(),
- getTermOrderPredicate(child11, children[1]));
+ Node order_pred_trans =
+ nm->mkNode(OR,
+ utils::mkTester(children[0], tindex, dt).negate(),
+ getTermOrderPredicate(child11, children[1]));
sbp_conj.push_back(order_pred_trans);
}
}
<< "Simple predicate for " << tn << " index " << tindex << " (" << nk
<< ") at depth " << depth << " : " << std::endl;
Trace("sygus-sb-simple") << " " << sb_pred << std::endl;
- sb_pred = nm->mkNode(
- kind::OR, DatatypesRewriter::mkTester(n, tindex, dt).negate(), sb_pred);
+ sb_pred = nm->mkNode(OR, utils::mkTester(n, tindex, dt).negate(), sb_pred);
}
d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = sb_pred;
return sb_pred;
// 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 ){
- unsigned cindex = DatatypesRewriter::indexOf(nv.getOperator());
+ unsigned cindex = utils::indexOf(nv.getOperator());
std::vector<Node> rcons_children;
rcons_children.push_back(nv.getOperator());
bool childrenChanged = false;
Assert(dt.isSygus());
// ensure that the expected size bound is met
- int cindex = DatatypesRewriter::indexOf(vn.getOperator());
- Node tst = DatatypesRewriter::mkTester( n, cindex, dt );
+ int cindex = utils::indexOf(vn.getOperator());
+ Node tst = utils::mkTester(n, cindex, dt);
bool hastst = d_td->getEqualityEngine()->hasTerm(tst);
Node tstrep;
if (hastst)
if( !hastst ){
// This should not happen generally, it is caused by a sygus term not
// being assigned a tester.
- Node split = DatatypesRewriter::mkSplit(n, dt);
+ Node split = utils::mkSplit(n, dt);
Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered "
"missing split for "
<< n << "." << std::endl;
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "options/theory_options.h"
#include "theory/datatypes/theory_datatypes_type_rules.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_model.h"
#include "theory/type_enumerator.h"
#include "theory/valuation.h"
-#include "options/theory_options.h"
-#include "options/quantifiers_options.h"
using namespace std;
using namespace CVC4::kind;
if( dt.getNumConstructors()==1 ){
//this may not be necessary?
//if only one constructor, then this term must be this constructor
- Node t = DatatypesRewriter::mkTester( n, 0, dt );
+ Node t = utils::mkTester(n, 0, dt);
d_pending.push_back( t );
d_pending_exp[ t ] = d_true;
Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
}else{
Assert( consIndex!=-1 || dt.isSygus() );
if( options::dtBinarySplit() && consIndex!=-1 ){
- Node test = DatatypesRewriter::mkTester( n, consIndex, dt );
+ Node test = utils::mkTester(n, consIndex, dt);
Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
test = Rewriter::rewrite( test );
NodeBuilder<> nb(kind::OR);
d_out->requirePhase( test, true );
}else{
Trace("dt-split") << "*************Split for constructors on " << n << endl;
- Node lemma = DatatypesRewriter::mkSplit(n, dt);
+ Node lemma = utils::mkSplit(n, dt);
Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
d_out->lemma( lemma, false, false, true );
d_addedLemma = true;
}
//add to tester if applicable
Node t_arg;
- int tindex = DatatypesRewriter::isTester( atom, t_arg );
+ int tindex = utils::isTester(atom, t_arg);
if (tindex >= 0)
{
Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
TypeNode ndt = n[0].getType();
if (options::dtSharedSelectors())
{
- size_t selectorIndex = DatatypesRewriter::indexOf(selector);
+ size_t selectorIndex = utils::indexOf(selector);
Trace("dt-expand") << "...selector index = " << selectorIndex
<< std::endl;
Assert(selectorIndex < c.getNumArgs());
if( in.getKind()==EQUAL ){
Node nn;
std::vector< Node > rew;
- if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
+ if (utils::checkClash(in[0], in[1], rew))
+ {
nn = NodeManager::currentNM()->mkConst(false);
- }else{
+ }
+ else
+ {
nn = rew.size()==0 ? d_true :
( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
}
Trace("datatypes-debug") << " constructors : " << cons1 << " " << cons2 << std::endl;
Node unifEq = cons1.eqNode( cons2 );
std::vector< Node > rew;
- if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
+ if (utils::checkClash(cons1, cons2, rew))
+ {
d_conflictNode = explain( unifEq );
Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
d_conflict = true;
return;
- }else{
-
+ }
+ else
+ {
//do unification
for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
if( !areEqual( cons1[i], cons2[i] ) ){
int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
if( eqc && !eqc->d_constructor.get().isNull() ){
- return DatatypesRewriter::indexOf(eqc->d_constructor.get().getOperator());
+ return utils::indexOf(eqc->d_constructor.get().getOperator());
}else{
Node lbl = getLabel( n );
if( lbl.isNull() ){
return -1;
}else{
- int tindex = DatatypesRewriter::isTester( lbl );
+ int tindex = utils::isTester(lbl);
Assert( tindex!=-1 );
return tindex;
}
{
if( i!=ttindex && neg_testers.find( i )==neg_testers.end() ){
Assert( n.getKind()!=APPLY_CONSTRUCTOR );
- Node infer = DatatypesRewriter::mkTester( n, i, dt ).negate();
+ Node infer = utils::mkTester(n, i, dt).negate();
Trace("datatypes-infer") << "DtInfer : neg label : " << infer << " by " << t << std::endl;
d_infer.push_back( infer );
d_infer_exp.push_back( t );
}
}
}
- Node t_concl = testerIndex==-1 ? NodeManager::currentNM()->mkConst( false ) : DatatypesRewriter::mkTester( t_arg, testerIndex, dt );
+ Node t_concl = testerIndex == -1
+ ? NodeManager::currentNM()->mkConst(false)
+ : utils::mkTester(t_arg, testerIndex, dt);
Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
d_pending.push_back( t_concl );
d_pending_exp[ t_concl ] = t_concl_exp;
//check labels
NodeUIntMap::iterator lbl_i = d_labels.find(n);
if( lbl_i != d_labels.end() ){
- size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
+ size_t constructorIndex = utils::indexOf(c.getOperator());
size_t n_lbl = (*lbl_i).second;
for (size_t i = 0; i < n_lbl; i++)
{
}
if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
Expr selectorExpr = s.getOperator().toExpr();
- size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
+ size_t constructorIndex = utils::indexOf(c.getOperator());
const Datatype& dt = Datatype::datatypeOf(selectorExpr);
const DatatypeConstructor& dtc = dt[constructorIndex];
int selectorIndex = dtc.getSelectorIndexInternal( selectorExpr );
//must try the infinite ones first
bool cfinite = dt[ i ].isInterpretedFinite( tt );
if( pcons[i] && (r==1)==cfinite ){
- neqc = DatatypesRewriter::getInstCons( eqc, dt, i );
+ neqc = utils::getInstCons(eqc, dt, i);
//for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
// //if( sels[i].find( j )==sels[i].end() && neqc[j].getType().isDatatype() ){
// if( !d_equalityEngine.hasTerm( neqc[j] ) && neqc[j].getType().isDatatype() ){
const Datatype& dt = n[0].getType().getDatatype();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
- if (DatatypesRewriter::isNullaryConstructor(dt[i]))
+ if (utils::isNullaryConstructor(dt[i]))
{
- Node test = DatatypesRewriter::mkTester(n[0], i, dt);
+ Node test = utils::mkTester(n[0], i, dt);
children.push_back(test);
}
}
}else{
//add constructor to equivalence class
Node k = getTermSkolemFor( n );
- n_ic = DatatypesRewriter::getInstCons( k, dt, index );
+ n_ic = utils::getInstCons(k, dt, index);
//Assert( n_ic==Rewriter::rewrite( n_ic ) );
n_ic = Rewriter::rewrite( n_ic );
collectTerms( n_ic );
Node r = d_equalityEngine.getRepresentative( n );
EqcInfo * ei = getOrMakeEqcInfo( r, false );
int l_index = getLabelIndex( ei, r );
- int t_index =
- static_cast<int>(DatatypesRewriter::indexOf(atom.getOperator()));
+ int t_index = static_cast<int>(utils::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;
--- /dev/null
+/********************* */
+/*! \file theory_datatypes_utils.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of rewriter for the theory of (co)inductive datatypes.
+ **
+ ** Implementation of rewriter for the theory of (co)inductive datatypes.
+ **/
+
+#include "theory/datatypes/theory_datatypes_utils.h"
+
+#include "expr/node_algorithm.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+namespace utils {
+
+Node applySygusArgs(const Datatype& dt,
+ Node op,
+ Node n,
+ const std::vector<Node>& args)
+{
+ if (n.getKind() == BOUND_VARIABLE)
+ {
+ Assert(n.hasAttribute(SygusVarNumAttribute()));
+ int vn = n.getAttribute(SygusVarNumAttribute());
+ Assert(Node::fromExpr(dt.getSygusVarList())[vn] == n);
+ return args[vn];
+ }
+ // n is an application of operator op.
+ // We must compute the free variables in op to determine if there are
+ // any substitutions we need to make to n.
+ TNode val;
+ if (!op.hasAttribute(SygusVarFreeAttribute()))
+ {
+ std::unordered_set<Node, NodeHashFunction> fvs;
+ if (expr::getFreeVariables(op, fvs))
+ {
+ if (fvs.size() == 1)
+ {
+ for (const Node& v : fvs)
+ {
+ val = v;
+ }
+ }
+ else
+ {
+ val = op;
+ }
+ }
+ Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl;
+ op.setAttribute(SygusVarFreeAttribute(), val);
+ }
+ else
+ {
+ val = op.getAttribute(SygusVarFreeAttribute());
+ }
+ if (val.isNull())
+ {
+ return n;
+ }
+ if (val.getKind() == BOUND_VARIABLE)
+ {
+ // single substitution case
+ int vn = val.getAttribute(SygusVarNumAttribute());
+ TNode sub = args[vn];
+ return n.substitute(val, sub);
+ }
+ // do the full substitution
+ std::vector<Node> vars;
+ Node bvl = Node::fromExpr(dt.getSygusVarList());
+ for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
+ {
+ vars.push_back(bvl[i]);
+ }
+ return n.substitute(vars.begin(), vars.end(), args.begin(), args.end());
+}
+
+Kind getOperatorKindForSygusBuiltin(Node op)
+{
+ Assert(op.getKind() != BUILTIN);
+ if (op.getKind() == LAMBDA)
+ {
+ 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 UNDEFINED_KIND;
+}
+
+Node 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());
+ Trace("dt-sygus-util") << "Operator is " << op << std::endl;
+ if (children.empty())
+ {
+ // no children, return immediately
+ Trace("dt-sygus-util") << "...return direct op" << std::endl;
+ return op;
+ }
+ // 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 = NodeManager::operatorToKind(op);
+ Trace("dt-sygus-util") << "operator kind is " << ok << std::endl;
+ if (ok != UNDEFINED_KIND)
+ {
+ // If it is an APPLY_UF operator, we should have at least an operator and
+ // a child.
+ Assert(ok != APPLY_UF || schildren.size() != 1);
+ ret = NodeManager::currentNM()->mkNode(ok, schildren);
+ Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
+ return ret;
+ }
+ Kind tok = getOperatorKindForSygusBuiltin(op);
+ if (schildren.size() == 1 && tok == UNDEFINED_KIND)
+ {
+ ret = schildren[0];
+ }
+ else
+ {
+ ret = NodeManager::currentNM()->mkNode(tok, schildren);
+ }
+ Trace("dt-sygus-util") << "...return " << ret << std::endl;
+ return ret;
+}
+
+/** get instantiate cons */
+Node getInstCons(Node n, const Datatype& dt, int index)
+{
+ Assert(index >= 0 && index < (int)dt.getNumConstructors());
+ std::vector<Node> children;
+ NodeManager* nm = NodeManager::currentNM();
+ children.push_back(Node::fromExpr(dt[index].getConstructor()));
+ Type t = n.getType().toType();
+ for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
+ {
+ Node nc = nm->mkNode(APPLY_SELECTOR_TOTAL,
+ Node::fromExpr(dt[index].getSelectorInternal(t, i)),
+ n);
+ children.push_back(nc);
+ }
+ Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
+ if (dt.isParametric())
+ {
+ TypeNode tn = TypeNode::fromType(t);
+ // add type ascription for ambiguous constructor types
+ if (!n_ic.getType().isComparableTo(tn))
+ {
+ Debug("datatypes-parametric")
+ << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to "
+ << n.getType() << std::endl;
+ Debug("datatypes-parametric")
+ << "Constructor is " << dt[index] << std::endl;
+ Type tspec =
+ dt[index].getSpecializedConstructorType(n.getType().toType());
+ Debug("datatypes-parametric")
+ << "Type specification is " << tspec << std::endl;
+ children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
+ nm->mkConst(AscriptionType(tspec)),
+ children[0]);
+ n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
+ Assert(n_ic.getType() == tn);
+ }
+ }
+ Assert(isInstCons(n, n_ic, dt) == index);
+ // n_ic = Rewriter::rewrite( n_ic );
+ return n_ic;
+}
+
+int isInstCons(Node t, Node n, const Datatype& dt)
+{
+ if (n.getKind() == APPLY_CONSTRUCTOR)
+ {
+ 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[i].getKind() != APPLY_SELECTOR_TOTAL
+ || n[i].getOperator() != Node::fromExpr(c.getSelectorInternal(nt, i))
+ || n[i][0] != t)
+ {
+ return -1;
+ }
+ }
+ return index;
+ }
+ return -1;
+}
+
+int isTester(Node n, Node& a)
+{
+ if (n.getKind() == APPLY_TESTER)
+ {
+ a = n[0];
+ return indexOf(n.getOperator());
+ }
+ return -1;
+}
+
+int isTester(Node n)
+{
+ if (n.getKind() == APPLY_TESTER)
+ {
+ return indexOf(n.getOperator());
+ }
+ return -1;
+}
+
+struct DtIndexAttributeId
+{
+};
+typedef expr::Attribute<DtIndexAttributeId, uint64_t> DtIndexAttribute;
+
+unsigned 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 mkTester(Node n, int i, const Datatype& dt)
+{
+ return NodeManager::currentNM()->mkNode(
+ APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
+}
+
+Node mkSplit(Node n, const Datatype& dt)
+{
+ std::vector<Node> splits;
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ Node test = mkTester(n, i, dt);
+ splits.push_back(test);
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits);
+}
+
+bool isNullaryApplyConstructor(Node n)
+{
+ Assert(n.getKind() == APPLY_CONSTRUCTOR);
+ for (const Node& nc : n)
+ {
+ if (nc.getType().isDatatype())
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+bool isNullaryConstructor(const DatatypeConstructor& c)
+{
+ for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+ {
+ if (c[j].getType().getRangeType().isDatatype())
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+bool checkClash(Node n1, Node n2, std::vector<Node>& rew)
+{
+ Trace("datatypes-rewrite-debug")
+ << "Check clash : " << n1 << " " << n2 << std::endl;
+ if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR)
+ {
+ if (n1.getOperator() != n2.getOperator())
+ {
+ Trace("datatypes-rewrite-debug")
+ << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator()
+ << " " << n2.getOperator() << std::endl;
+ return true;
+ }
+ Assert(n1.getNumChildren() == n2.getNumChildren());
+ for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
+ {
+ if (checkClash(n1[i], n2[i], rew))
+ {
+ return true;
+ }
+ }
+ }
+ else if (n1 != n2)
+ {
+ if (n1.isConst() && n2.isConst())
+ {
+ Trace("datatypes-rewrite-debug")
+ << "Clash constants : " << n1 << " " << n2 << std::endl;
+ return true;
+ }
+ else
+ {
+ Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2);
+ rew.push_back(eq);
+ }
+ }
+ return false;
+}
+
+} // namespace utils
+} // namespace datatypes
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file theory_datatypes_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Util functions for theory datatypes.
+ **
+ ** Util functions for theory datatypes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
+#define CVC4__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager_attributes.h"
+
+namespace CVC4 {
+namespace theory {
+
+// ----------------------- sygus datatype attributes
+/** 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;
+
+/**
+ * Attribute true for enumerators whose current model values were registered by
+ * the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
+ * This is set by the datatypes sygus solver during LAST_CALL effort checks for
+ * each active sygus enumerator.
+ */
+struct SygusSymBreakOkAttributeId
+{
+};
+typedef expr::Attribute<SygusSymBreakOkAttributeId, bool>
+ SygusSymBreakOkAttribute;
+
+/** sygus var free
+ *
+ * This attribute is used to mark whether sygus operators have free occurrences
+ * of variables from the formal argument list of the function-to-synthesize.
+ *
+ * We store three possible cases for sygus operators op:
+ * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null()
+ * In this case, op has no free variables from the formal argument list of the
+ * function-to-synthesize.
+ * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable.
+ * In this case, op has exactly one free variable, v.
+ * (3) op.getAttribute(SygusVarFreeAttribute())==op
+ * In this case, op has an arbitrary set (cardinality >1) of free variables from
+ * the formal argument list of the function to synthesize.
+ *
+ * This attribute is used to compute applySygusArgs below.
+ */
+struct SygusVarFreeAttributeId
+{
+};
+typedef expr::Attribute<SygusVarFreeAttributeId, Node> SygusVarFreeAttribute;
+// ----------------------- end sygus datatype attributes
+
+namespace datatypes {
+namespace utils {
+
+/** get instantiate cons
+ *
+ * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
+ * where C is the index^{th} constructor of datatype dt.
+ */
+Node getInstCons(Node n, const Datatype& dt, int index);
+/** is instantiation cons
+ *
+ * If this method returns a value >=0, then that value, call it index,
+ * is such that n = C( sel^{C,1}( t ), ..., sel^{C,m}( t ) ),
+ * where C is the index^{th} constructor of dt.
+ */
+int isInstCons(Node t, Node n, const Datatype& dt);
+/** is tester
+ *
+ * This method returns a value >=0 if n is a tester predicate. The return
+ * value indicates the constructor index that the tester n is for. If this
+ * method returns a value >=0, then it updates a to the argument that the
+ * tester n applies to.
+ */
+int isTester(Node n, Node& a);
+/** is tester, same as above but does not update an argument */
+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.)
+ */
+unsigned indexOf(Node n);
+/** make tester is-C( n ), where C is the i^{th} constructor of dt */
+Node mkTester(Node n, int i, const Datatype& dt);
+/** make tester split
+ *
+ * Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
+ * are the constructors of n's type (dt).
+ */
+Node mkSplit(Node n, const Datatype& dt);
+/** returns true iff n is a constructor term with no datatype children */
+bool isNullaryApplyConstructor(Node n);
+/** returns true iff c is a constructor with no datatype children */
+bool isNullaryConstructor(const DatatypeConstructor& c);
+/** check clash
+ *
+ * This method returns true if and only if n1 and n2 have a skeleton that has
+ * conflicting constructors at some term position.
+ * Examples of terms that clash are:
+ * C( x, y ) and D( z )
+ * C( D( x ), y ) and C( E( x ), y )
+ * Examples of terms that do not clash are:
+ * C( x, y ) and C( D( x ), y )
+ * C( D( x ), y ) and C( x, E( z ) )
+ * C( x, y ) and z
+ */
+bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
+
+// ------------------------ sygus utils
+
+/** get operator kind for sygus builtin
+ *
+ * This returns the Kind corresponding to applications of the operator op
+ * when building the builtin version of sygus terms. This is used by the
+ * function mkSygusTerm.
+ */
+Kind getOperatorKindForSygusBuiltin(Node op);
+/** 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.
+ */
+Node mkSygusTerm(const Datatype& dt,
+ unsigned i,
+ const std::vector<Node>& children);
+/**
+ * n is a builtin term that is an application of operator op.
+ *
+ * This returns an n' such that (eval n args) is n', where n' is a instance of
+ * n for the appropriate substitution.
+ *
+ * For example, given a function-to-synthesize with formal argument list (x,y),
+ * say we have grammar:
+ * A -> A+A | A+x | A+(x+y) | y
+ * These lead to constructors with sygus ops:
+ * C1 / (lambda w1 w2. w1+w2)
+ * C2 / (lambda w1. w1+x)
+ * C3 / (lambda w1. w1+(x+y))
+ * C4 / y
+ * Examples of calling this function:
+ * applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } )
+ * ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2).
+ * applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } )
+ * ... returns (APPLY_UF (lambda w1. w1+3) t1).
+ * applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } )
+ * ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1).
+ * applySygusArgs( dt, C4, y, { 3, 5 } )
+ * ... returns 5.
+ * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4,
+ * to cache the results of whether the evaluation of this constructor needs
+ * a substitution over the formal argument list of the function-to-synthesize.
+ */
+Node applySygusArgs(const Datatype& dt,
+ Node op,
+ Node n,
+ const std::vector<Node>& args);
+/**
+ * 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 +.
+ */
+Node getSygusOpForCTerm(Node n);
+
+// ------------------------ end sygus utils
+
+} // namespace utils
+} // namespace datatypes
+} // namespace theory
+} // namespace CVC4
+
+#endif
** Enumerators for datatypes.
**/
- #include "theory/datatypes/type_enumerator.h"
- #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/type_enumerator.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
using namespace CVC4;
using namespace theory;
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 = datatypes::DatatypesRewriter::indexOf(t.getOperator());
+ d_zeroCtor = datatypes::utils::indexOf(t.getOperator());
d_has_debruijn = 0;
}
Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
using namespace CVC4::kind;
if (sbl.getKind() == NOT)
{
Node a;
- int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a);
+ int tst = datatypes::utils::isTester(sbl[0], a);
if (tst >= 0)
{
if (a == e)
#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;
#include "theory/quantifiers/sygus/sygus_explain.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace CVC4::kind;
}
Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
- int i = datatypes::DatatypesRewriter::indexOf(vn.getOperator());
- Node tst = datatypes::DatatypesRewriter::mkTester(n, i, dt);
+ int i = datatypes::utils::indexOf(vn.getOperator());
+ Node tst = datatypes::utils::mkTester(n, i, dt);
exp.push_back(tst);
for (unsigned j = 0; j < vn.getNumChildren(); j++)
{
}
}
const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
- int cindex = datatypes::DatatypesRewriter::indexOf(vn.getOperator());
+ int cindex = datatypes::utils::indexOf(vn.getOperator());
Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
- Node tst = datatypes::DatatypesRewriter::mkTester(n, cindex, dt);
+ Node tst = datatypes::utils::mkTester(n, cindex, dt);
exp.push_back(tst);
// if the operator of vn is different than vnr, then disunification obligation
// is met
#include "options/quantifiers_options.h"
#include "printer/sygus_print_callback.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/sygus_process_conj.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#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/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "expr/datatype.h"
#include "options/quantifiers_options.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/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
return false;
}
Node op = n.getOperator();
- unsigned cindex = datatypes::DatatypesRewriter::indexOf(op);
+ unsigned cindex = datatypes::utils::indexOf(op);
Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
if (sygusOp.getAttribute(SygusAnyConstAttribute()))
{
#include "theory/quantifiers/sygus/sygus_unif.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/sygus/sygus_unif_io.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/evaluator.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "util/random.h"
#include "theory/quantifiers/sygus/sygus_unif_strat.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/sygus_unif.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
Assert(nc.first < dt.getNumConstructors());
if (!nc.second)
{
- Node tst =
- datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
+ Node tst = datatypes::utils::mkTester(em, nc.first, dt).negate();
if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
{
continue;
}
EnumTypeInfoStrat* etis = snode.d_strats[j];
- unsigned cindex = datatypes::DatatypesRewriter::indexOf(etis->d_cons);
+ unsigned cindex = datatypes::utils::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 "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "base/cvc4_check.h"
#include "options/base_options.h"
+#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "theory/arith/arith_msum.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
Assert( !a.isNull() );
children.push_back( a );
}
- return datatypes::DatatypesRewriter::mkSygusTerm(dt, c, children);
+ return datatypes::utils::mkSygusTerm(dt, c, children);
}
Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
}
if (n.getKind() == APPLY_CONSTRUCTOR)
{
- unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator());
+ unsigned i = datatypes::utils::indexOf(n.getOperator());
Assert(n.getNumChildren() == dt[i].getNumArgs());
std::map<int, Node> pre;
for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
sum += getSygusTermSize(n[i]);
}
const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
- int cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
+ int cindex = datatypes::utils::indexOf(n.getOperator());
Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
unsigned weight = dt[cindex].getWeight();
return weight + sum;
// 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);
+ Node exc_val = datatypes::utils::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
Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Assert(dt.isSygus());
- unsigned cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
+ unsigned cindex = datatypes::utils::indexOf(n.getOperator());
Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
// it is symbolic if it represents "any constant"
return sygusOp.getAttribute(SygusAnyConstAttribute());
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());
+ unsigned i = datatypes::utils::indexOf(ev.getOperator());
if (track_exp)
{
// explanation
}
Node ret = mkGeneric(dt, i, pre);
// apply the appropriate substitution to ret
- ret = datatypes::DatatypesRewriter::applySygusArgs(dt, sop, ret, args);
+ ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
// rewrite
ret = Rewriter::rewrite(ret);
return ret;
#include "theory/quantifiers/sygus/type_info.h"
#include "base/cvc4_check.h"
-#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace CVC4::kind;
projects / cvc5.git / commitdiff