RewriteResponse DatatypesRewriter::postRewrite(TNode in)
{
Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
- if (in.getKind() == kind::APPLY_CONSTRUCTOR)
+ Kind k = in.getKind();
+ NodeManager* nm = NodeManager::currentNM();
+ if (k == kind::APPLY_CONSTRUCTOR)
{
return rewriteConstructor(in);
}
- else if (in.getKind() == kind::APPLY_SELECTOR_TOTAL)
+ else if (k == kind::APPLY_SELECTOR_TOTAL)
{
return rewriteSelector(in);
}
- else if (in.getKind() == kind::APPLY_TESTER)
+ else if (k == kind::APPLY_TESTER)
{
return rewriteTester(in);
}
- else if (in.getKind() == kind::DT_SIZE)
+ else if (k == kind::DT_SIZE)
{
if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
{
std::vector<Node> children;
- for (unsigned i = 0; i < in[0].getNumChildren(); i++)
+ for (unsigned i = 0, size = in [0].getNumChildren(); i < size; i++)
{
if (in[0][i].getType().isDatatype())
{
- children.push_back(
- NodeManager::currentNM()->mkNode(kind::DT_SIZE, in[0][i]));
+ children.push_back(nm->mkNode(kind::DT_SIZE, in[0][i]));
}
}
TNode constructor = in[0].getOperator();
const Datatype& dt = Datatype::datatypeOf(constructor.toExpr());
const DatatypeConstructor& c = dt[constructorIndex];
unsigned weight = c.getWeight();
- children.push_back(NodeManager::currentNM()->mkConst(Rational(weight)));
- Node res = children.size() == 1
- ? children[0]
- : NodeManager::currentNM()->mkNode(kind::PLUS, children);
+ children.push_back(nm->mkConst(Rational(weight)));
+ Node res =
+ children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
Trace("datatypes-rewrite")
<< "DatatypesRewriter::postRewrite: rewrite size " << in << " to "
<< res << std::endl;
return RewriteResponse(REWRITE_AGAIN_FULL, res);
}
}
- else if (in.getKind() == kind::DT_HEIGHT_BOUND)
+ else if (k == kind::DT_HEIGHT_BOUND)
{
if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
{
Node res;
Rational r = in[1].getConst<Rational>();
Rational rmo = Rational(r - Rational(1));
- for (unsigned i = 0; i < in[0].getNumChildren(); i++)
+ for (unsigned i = 0, size = in [0].getNumChildren(); i < size; i++)
{
if (in[0][i].getType().isDatatype())
{
if (r.isZero())
{
- res = NodeManager::currentNM()->mkConst(false);
+ res = nm->mkConst(false);
break;
}
- else
- {
- children.push_back(NodeManager::currentNM()->mkNode(
- kind::DT_HEIGHT_BOUND,
- in[0][i],
- NodeManager::currentNM()->mkConst(rmo)));
- }
+ children.push_back(
+ nm->mkNode(kind::DT_HEIGHT_BOUND, in[0][i], nm->mkConst(rmo)));
}
}
if (res.isNull())
{
res = children.size() == 0
- ? NodeManager::currentNM()->mkConst(true)
+ ? nm->mkConst(true)
: (children.size() == 1 ? children[0]
- : NodeManager::currentNM()->mkNode(
- kind::AND, children));
+ : nm->mkNode(kind::AND, children));
}
Trace("datatypes-rewrite")
<< "DatatypesRewriter::postRewrite: rewrite height " << in << " to "
return RewriteResponse(REWRITE_AGAIN_FULL, res);
}
}
- else if (in.getKind() == kind::DT_SIZE_BOUND)
+ else if (k == kind::DT_SIZE_BOUND)
{
if (in[0].isConst())
{
- Node res = NodeManager::currentNM()->mkNode(
- kind::LEQ,
- NodeManager::currentNM()->mkNode(kind::DT_SIZE, in[0]),
- in[1]);
+ Node res = nm->mkNode(kind::LEQ, nm->mkNode(kind::DT_SIZE, in[0]), in[1]);
return RewriteResponse(REWRITE_AGAIN_FULL, res);
}
}
- if (in.getKind() == kind::EQUAL)
+ if (k == kind::EQUAL)
{
if (in[0] == in[1])
{
- return RewriteResponse(REWRITE_DONE,
- NodeManager::currentNM()->mkConst(true));
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
}
- else
+ std::vector<Node> rew;
+ if (checkClash(in[0], in[1], rew))
{
- std::vector<Node> rew;
- if (checkClash(in[0], in[1], rew))
- {
- Trace("datatypes-rewrite") << "Rewrite clashing equality " << in
- << " to false" << std::endl;
- return RewriteResponse(REWRITE_DONE,
- NodeManager::currentNM()->mkConst(false));
- //}else if( rew.size()==1 && rew[0]!=in ){
- // Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " <<
- // rew[0] << std::endl;
- // return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] );
- }
- else if (in[1] < in[0])
- {
- Node ins = NodeManager::currentNM()->mkNode(in.getKind(), in[1], in[0]);
- Trace("datatypes-rewrite") << "Swap equality " << in << " to " << ins
- << std::endl;
- return RewriteResponse(REWRITE_DONE, ins);
- }
- else
- {
- Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in
- << " " << in[0].getKind() << " "
- << in[1].getKind() << std::endl;
- }
+ Trace("datatypes-rewrite")
+ << "Rewrite clashing equality " << in << " to false" << std::endl;
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
+ //}else if( rew.size()==1 && rew[0]!=in ){
+ // Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " <<
+ // rew[0] << std::endl;
+ // return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] );
}
+ else if (in[1] < in[0])
+ {
+ Node ins = nm->mkNode(in.getKind(), in[1], in[0]);
+ Trace("datatypes-rewrite")
+ << "Swap equality " << in << " to " << ins << std::endl;
+ return RewriteResponse(REWRITE_DONE, ins);
+ }
+ Trace("datatypes-rewrite-debug")
+ << "Did not rewrite equality " << in << " " << in[0].getKind() << " "
+ << in[1].getKind() << std::endl;
}
return RewriteResponse(REWRITE_DONE, in);
<< inn << std::endl;
return RewriteResponse(REWRITE_DONE, inn);
}
- else
- {
- return RewriteResponse(REWRITE_DONE, in);
- }
+ return RewriteResponse(REWRITE_DONE, in);
}
return RewriteResponse(REWRITE_DONE, in);
}
return RewriteResponse(REWRITE_DONE,
NodeManager::currentNM()->mkConst(result));
}
- else
+ const Datatype& dt = static_cast<DatatypeType>(in[0].getType().toType()).getDatatype();
+ if (dt.getNumConstructors() == 1)
{
- const Datatype& dt = DatatypeType(in[0].getType().toType()).getDatatype();
- if (dt.getNumConstructors() == 1)
- {
- // only one constructor, so it must be
- Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
- << "only one ctor for " << dt.getName()
- << " and that is " << dt[0].getName()
- << std::endl;
- return RewriteResponse(REWRITE_DONE,
- NodeManager::currentNM()->mkConst(true));
- }
- // could try dt.getNumConstructors()==2 &&
- // Datatype::indexOf(in.getOperator())==1 ?
- else if (!options::dtUseTesters())
- {
- unsigned tindex = Datatype::indexOf(in.getOperator().toExpr());
- Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality "
- << in[0] << " " << tindex << std::endl;
- Node neq = mkTester(in[0], tindex, dt);
- Assert(neq != in);
- Trace("datatypes-rewrite")
- << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to "
- << neq << std::endl;
- return RewriteResponse(REWRITE_AGAIN_FULL, neq);
- }
+ // only one constructor, so it must be
+ Trace("datatypes-rewrite")
+ << "DatatypesRewriter::postRewrite: "
+ << "only one ctor for " << dt.getName() << " and that is "
+ << dt[0].getName() << std::endl;
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(true));
+ }
+ // could try dt.getNumConstructors()==2 &&
+ // Datatype::indexOf(in.getOperator())==1 ?
+ else if (!options::dtUseTesters())
+ {
+ unsigned tindex = Datatype::indexOf(in.getOperator().toExpr());
+ Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality "
+ << in[0] << " " << tindex << std::endl;
+ Node neq = mkTester(in[0], tindex, dt);
+ Assert(neq != in);
+ Trace("datatypes-rewrite")
+ << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to "
+ << neq << std::endl;
+ return RewriteResponse(REWRITE_AGAIN_FULL, neq);
}
return RewriteResponse(REWRITE_DONE, in);
}
return true;
}
Assert(n1.getNumChildren() == n2.getNumChildren());
- for (unsigned i = 0; i < n1.getNumChildren(); i++)
+ for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
{
if (checkClash(n1[i], n2[i], rew))
{
{
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; i < dt[index].getNumArgs(); i++)
+ for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
{
- Node nc = NodeManager::currentNM()->mkNode(
- kind::APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[index].getSelectorInternal(t, i)),
- n);
+ Node nc = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
+ Node::fromExpr(dt[index].getSelectorInternal(t, i)),
+ n);
children.push_back(nc);
}
- Node n_ic =
- NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, children);
+ Node n_ic = nm->mkNode(kind::APPLY_CONSTRUCTOR, children);
if (dt.isParametric())
{
TypeNode tn = TypeNode::fromType(t);
dt[index].getSpecializedConstructorType(n.getType().toType());
Debug("datatypes-parametric") << "Type specification is " << tspec
<< std::endl;
- children[0] = NodeManager::currentNM()->mkNode(
- kind::APPLY_TYPE_ASCRIPTION,
- NodeManager::currentNM()->mkConst(AscriptionType(tspec)),
- children[0]);
- n_ic =
- NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, children);
+ 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);
}
}
int index = Datatype::indexOf(n.getOperator().toExpr());
const DatatypeConstructor& c = dt[index];
Type nt = n.getType().toType();
- for (unsigned i = 0; i < n.getNumChildren(); i++)
+ 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))
return NodeManager::currentNM()->mkNode(
kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
}
- else
- {
#ifdef CVC4_ASSERTIONS
- Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
- Node a;
- int ii = isTester(ret, a);
- Assert(ii == i);
- Assert(a == n);
- return ret;
+ Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
+ Node a;
+ int ii = isTester(ret, a);
+ Assert(ii == i);
+ Assert(a == n);
+ return ret;
#else
- return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
+ return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
#endif
- }
}
bool DatatypesRewriter::isNullaryApplyConstructor(Node n)
bool DatatypesRewriter::isNullaryConstructor(const DatatypeConstructor& c)
{
- for (unsigned j = 0; j < c.getNumArgs(); j++)
+ for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
{
if (c[j].getType().getRangeType().isDatatype())
{
std::map<Node, int> eqc;
std::map<int, std::vector<Node> > eqc_nodes;
// partition based on top symbol
- for (unsigned j = 0; j < terms.size(); j++)
+ for (unsigned j = 0, size = terms.size(); j < size; j++)
{
Node t = terms[j];
Trace("dt-nconst") << " " << t << ", cdt=" << cdts[t] << std::endl;
prt.clear();
// partition based on children : for the first child that causes a
// split, break
- for (unsigned k = 0; k < eqc_nodes[eqc_curr].size(); k++)
+ for (unsigned k = 0, size = eqc_nodes[eqc_curr].size(); k < size;
+ k++)
{
Node t = eqc_nodes[eqc_curr][k];
Assert(t.getNumChildren() == nchildren);
}
}
// move into new eqc(s)
- for (std::map<int, std::vector<Node> >::iterator it = prt.begin();
- it != prt.end();
- ++it)
+ for (const std::pair<const int, std::vector<Node> >& p : prt)
{
int e = eqc_count;
- for (unsigned j = 0; j < it->second.size(); j++)
+ for (unsigned j = 0, size = p.second.size(); j < size; j++)
{
- Node t = it->second[j];
+ Node t = p.second[j];
eqc[t] = e;
eqc_nodes[e].push_back(t);
}
std::map<int, int> eqc_stack;
return normalizeCodatatypeConstantEqc(s, eqc_stack, eqc, 0);
}
- else
- {
- Trace("dt-nconst") << "...invalid." << std::endl;
- return Node::null();
- }
+ Trace("dt-nconst") << "...invalid." << std::endl;
+ return Node::null();
}
// normalize constant : apply to top-level codatatype constants
{
std::vector<Node> children;
bool childrenChanged = false;
- for (unsigned i = 0; i < n.getNumChildren(); i++)
+ for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
{
Node nc = normalizeConstant(n[i]);
children.push_back(nc);
{
return NodeManager::currentNM()->mkNode(n.getKind(), children);
}
- else
- {
- return n;
- }
}
}
- else
- {
- return n;
- }
+ return n;
}
Node DatatypesRewriter::collectRef(Node n,
std::vector<Node> children;
children.push_back(n.getOperator());
bool childChanged = false;
- for (unsigned i = 0; i < n.getNumChildren(); i++)
+ for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
{
Node nc = collectRef(n[i], sk, rf, rf_pending, terms, cdts);
if (nc.isNull())
{
return Node::null();
}
- else
+ Assert(sk.size() == rf_pending.size());
+ Node r = rf_pending[rf_pending.size() - 1 - index];
+ if (r.isNull())
{
- Assert(sk.size() == rf_pending.size());
- Node r = rf_pending[rf_pending.size() - 1 - index];
- if (r.isNull())
- {
- r = NodeManager::currentNM()->mkBoundVar(
- sk[rf_pending.size() - 1 - index].getType());
- rf_pending[rf_pending.size() - 1 - index] = r;
- }
- return r;
+ r = NodeManager::currentNM()->mkBoundVar(
+ sk[rf_pending.size() - 1 - index].getType());
+ rf_pending[rf_pending.size() - 1 - index] = r;
}
+ return r;
}
}
}
{
Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n
<< " depth=" << depth << std::endl;
- if (eqc.find(n) == eqc.end())
- {
- return n;
- }
- else
+ if (eqc.find(n) != eqc.end())
{
int e = eqc[n];
std::map<int, int>::iterator it = eqc_stack.find(e);
return NodeManager::currentNM()->mkConst(
UninterpretedConstant(n.getType().toType(), debruijn));
}
- else
+ std::vector<Node> children;
+ bool childChanged = false;
+ eqc_stack[e] = depth;
+ for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
{
- std::vector<Node> children;
- bool childChanged = false;
- eqc_stack[e] = depth;
- for (unsigned i = 0; i < n.getNumChildren(); i++)
- {
- Node nc =
- normalizeCodatatypeConstantEqc(n[i], eqc_stack, eqc, depth + 1);
- children.push_back(nc);
- childChanged = childChanged || nc != n[i];
- }
- eqc_stack.erase(e);
- if (childChanged)
- {
- Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
- children.insert(children.begin(), n.getOperator());
- return NodeManager::currentNM()->mkNode(n.getKind(), children);
- }
- else
- {
- return n;
- }
+ Node nc = normalizeCodatatypeConstantEqc(n[i], eqc_stack, eqc, depth + 1);
+ children.push_back(nc);
+ childChanged = childChanged || nc != n[i];
+ }
+ eqc_stack.erase(e);
+ if (childChanged)
+ {
+ Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
+ children.insert(children.begin(), n.getOperator());
+ return NodeManager::currentNM()->mkNode(n.getKind(), children);
}
}
+ return n;
}
Node DatatypesRewriter::replaceDebruijn(Node n,
{
std::vector<Node> children;
bool childChanged = false;
- for (unsigned i = 0; i < n.getNumChildren(); i++)
+ for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
{
Node nc = replaceDebruijn(n[i], orig, orig_tn, depth + 1);
children.push_back(nc);
*
* This returns the normal form of the codatatype constant n. This runs a
* DFA minimization algorithm based on the private functions below.
+ *
+ * In particular, we first call collectRefs to setup initial information
+ * about what terms occur in n. Then, we run a DFA minimization algorithm to
+ * partition these subterms in equivalence classes. Finally, we call
+ * normalizeCodatatypeConstantEqc to construct the normalized codatatype
+ * constant that is equivalent to n.
*/
static Node normalizeCodatatypeConstant(Node n);
/** normalize constant
/** rewrite tester term in */
static RewriteResponse rewriteTester(TNode in);
- /** TODO (#1436) document these */
+ /** collect references
+ *
+ * This function, given as input a codatatype term n, collects the necessary
+ * information for constructing a (canonical) codatatype constant that is
+ * equivalent to n if one exists, or null otherwise.
+ *
+ * In particular it returns a term ret such that all non-codatatype datatype
+ * subterms of n are replaced by a constant that is equal to them via a
+ * (mutually) recursive call to normalizeConstant above. Additionally, this
+ * function replaces references to mu-binders with fresh variables.
+ * In detail, mu-terms are represented by uninterpreted constants of datatype
+ * type that carry their Debruijn index.
+ *
+ * Consider the example of a codatatype representing a stream of integers:
+ * Stream := cons( head : Int, tail : Stream )
+ * The stream 1,0,1,0,1,0... when written in mu-notation is the term:
+ * mu x. cons( 1, mu y. cons( 0, x ) )
+ * This is represented in CVC4 by the Node:
+ * cons( 1, cons( 0, c[1] ) )
+ * where c[1] is a uninterpreted constant datatype with Debruijn index 1,
+ * indicating that c[1] is nested underneath 1 level on the path to the
+ * term which it binds. On the other hand, the stream 1,0,0,0,0,... is
+ * represented by the codatatype term:
+ * cons( 1, cons( 0, c[0] ) )
+ *
+ * Subterms that are references to mu-binders in n are replaced by a new
+ * variable. If n contains any subterm that is a reference to a mu-binder not
+ * bound in n, then we return null. For example we return null when n is:
+ * cons( 1, cons( 0, c[2] ) )
+ * since c[2] is not bound by this codatatype term.
+ *
+ * All valid references to mu-binders are replaced by a variable that is unique
+ * for the term it references. For example, for the infinite tree codatatype:
+ * Tree : node( data : Int, left : Tree, right : Tree )
+ * If n is the term:
+ * node( 0, c[0], node( 1, c[0], c[1] ) )
+ * then the return value ret of this function is:
+ * node( 0, x, node( 1, y, x ) )
+ * where x refers to the root of the term and y refers to the right tree of the
+ * root.
+ *
+ * The argument sk stores the current set of node that we are traversing
+ * beneath. The argument rf_pending stores, for each node that we are
+ * traversing beneath either null or the free variable that we are using to
+ * refer to its mu-binder. The remaining arguments store information that is
+ * relevant when performing normalization of n using the value of ret:
+ *
+ * rf : maps subterms of n to the corresponding term in ret for all subterms
+ * where the corresponding term in ret is different.
+ * terms : stores all subterms of ret.
+ * cdts : for each term t in terms, stores whether t is a codatatype.
+ */
static Node collectRef(Node n,
std::vector<Node>& sk,
std::map<Node, Node>& rf,
std::vector<Node>& rf_pending,
std::vector<Node>& terms,
std::map<Node, bool>& cdts);
- // eqc_stack stores depth
+ /** normalize codatatype constant eqc
+ *
+ * This recursive function returns a codatatype constant that is equivalent to
+ * n based on a pre-computed partition of the subterms of n into equivalence
+ * classes, as stored in the mapping eqc, which maps the subterms of n to
+ * equivalence class ids. The arguments eqc_stack and depth store information
+ * about the traversal in a term we have recursed, where
+ *
+ * eqc_stack : maps the depth of each term we have traversed to its equivalence
+ * class id.
+ * depth : the number of levels which we have traversed.
+ */
static Node normalizeCodatatypeConstantEqc(Node n,
std::map<int, int>& eqc_stack,
std::map<Node, int>& eqc,
int depth);
+ /** replace debruijn
+ *
+ * This function, given codatatype term n, returns a node
+ * where all subterms of n that have Debruijn indices that refer to a
+ * term of input depth are replaced by orig. For example, for the infinite Tree
+ * datatype,
+ * replaceDebruijn( node( 0, c[0], node( 1, c[0], c[1] ) ), t, Tree, 0 )
+ * returns
+ * node( 0, t, node( 1, c[0], t ) ).
+ */
static Node replaceDebruijn(Node n,
Node orig,
TypeNode orig_tn,
projects / cvc5.git / commitdiff