SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, &nf , &(bm->UserFlags));
ASTNodeMap fromTo;
- bb.getConsts(simplified_solved_InputToSAT, fromTo);
+ ASTNodeMap equivs;
+ bb.getConsts(simplified_solved_InputToSAT, fromTo,equivs);
+ if (equivs.size() > 0)
+ {
+ /* These nodes have equivalent AIG representations, so even though they have different
+ * word level expressions they are identical semantically. So we pick one of the ASTnodes
+ * and replace the others with it.
+ * TODO: Currently only for booleans,
+ * TODO: Isn't applied transitively because it infinite loops.
+ * TODO: I replace with the lower id node, sometimes though we replace with much more
+ * difficult looking ASTNodes.
+ */
+ ASTNodeMap cache;
+ simplified_solved_InputToSAT = SubstitutionMap::simple_replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
+ bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
+ }
+
if (fromTo.size() > 0)
{
ASTNodeMap cache;
- simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
+ simplified_solved_InputToSAT = SubstitutionMap:: replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
}
actualBBSize = bbnm.totalNumberOfNodes();
return (loops);
}
+ASTNode
+SubstitutionMap::simple_replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory * nf)
+{
+ const Kind k = n.GetKind();
+ if (k == BVCONST || k == TRUE || k == FALSE)
+ return n;
+
+ ASTNodeMap::const_iterator it;
+
+ if ((it = cache.find(n)) != cache.end())
+ return it->second;
+
+ if ((it = fromTo.find(n)) != fromTo.end())
+ {
+ const ASTNode& r = it->second;
+ assert(r.GetIndexWidth() == n.GetIndexWidth());
+ cache.insert(make_pair(n, r));
+ return r;
+ }
+
+ // These can't be created like regular nodes are
+ if (k == SYMBOL)
+ return n;
+
+ const unsigned int indexWidth = n.GetIndexWidth();
+
+ const ASTVec& children = n.GetChildren();
+ assert(children.size() > 0);
+ // Should have no leaves left here.
+
+ ASTVec new_children;
+ new_children.reserve(children.size());
+
+ for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++)
+ {
+ new_children.push_back(simple_replace(*it, fromTo, cache, nf));
+ }
+
+ assert(new_children.size() == children.size());
+
+ // This code short-cuts if the children are the same. Nodes with the same children,
+ // won't have necessarily given the same node if the simplifyingNodeFactory is enabled
+ // now, but wasn't enabled when the node was created. Shortcutting saves lots of time.
+ if (new_children == children)
+ {
+ cache.insert(make_pair(n, n));
+ return n;
+ }
+
+ ASTNode result;
+ const unsigned int valueWidth = n.GetValueWidth();
+
+ if (valueWidth == 0) // n.GetType() == BOOLEAN_TYPE
+ {
+ result = nf->CreateNode(k, new_children);
+ }
+ else
+ {
+ // If the index and value width aren't saved, they are reset sometimes (??)
+ result = nf->CreateArrayTerm(k, indexWidth, valueWidth, new_children);
+ }
+
+ // We may have created something that should be mapped. For instance,
+ // if n is READ(A, x), and the fromTo is: {x==0, READ(A,0) == 1}, then
+ // by here the result will be READ(A,0). Which needs to be mapped again..
+ // I hope that this makes it idempotent.
+
+ assert(result.GetValueWidth() == valueWidth);
+ assert(result.GetIndexWidth() == indexWidth);
+
+ cache.insert(make_pair(n, result));
+ return result;
+}
+
};
// Replace any nodes in "n" that exist in the fromTo map.
// NB the fromTo map is changed.
+ static ASTNode simple_replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf);
static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf);
static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays);
void
Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key)
{
- AlwaysTrueHashSet.insert(key.GetNodeNum());
+ // The always true/ always false relies on the top level constraint not being removed.
+ // however with bb equivalence checking, AIGs can figure out that the outer constraint
+ // is unncessary because it's enforced by the implicit constraint---removing it. That
+ // leaves just one instance of the constraint, so it we replace it with true/false
+ // the constraint is lost. This is subsumed by constant bit propagation, so I suspect
+ // it's not a big loss.
+ if (!_bm->UserFlags.isSet("bb-equiv","0"))
+ AlwaysTrueHashSet.insert(key.GetNodeNum());
}
ASTNode
print(c1);
}
public:
+
+ intptr_t GetNodeNum() const
+ {
+ return (intptr_t)n;
+ }
+
// If the pointer is odd. Then it's the NOT of the pointer one less.
Aig_Obj_t * n;
bool operator==(const BBNodeAIG &other) const
{
- return n == other.n;
+ return n == other.n;
}
bool operator!=(const BBNodeAIG &other) const
// Look through the maps to see what the bitblaster has discovered (if anything) is constant.
template<class BBNode, class BBNodeManagerT>
void
- BitBlaster<BBNode, BBNodeManagerT>::getConsts(const ASTNode& form, ASTNodeMap& fromTo)
+ BitBlaster<BBNode, BBNodeManagerT>::getConsts(const ASTNode& form, ASTNodeMap& fromTo, ASTNodeMap& equivs)
{
assert(form.GetType() == BOOLEAN_TYPE);
fromTo.insert(make_pair(n, r));
}
+
+ if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","0"))
+ {
+ HASHMAP <intptr_t ,ASTNode> nodeToFn;
+ typename map<ASTNode, BBNode>::iterator it;
+ for (it = BBFormMemo.begin(); it != BBFormMemo.end(); it++)
+ {
+ const ASTNode& n = it->first;
+ if (n.isConstant())
+ continue;
+
+ const BBNode& x = it->second;
+ if (x == BBTrue || x == BBFalse)
+ continue;
+
+ if (nodeToFn.find(x.GetNodeNum()) == nodeToFn.end())
+ {
+ nodeToFn.insert(make_pair(x.GetNodeNum(),n));
+ }
+ else
+ {
+ const ASTNode other = (nodeToFn.find(x.GetNodeNum()))->second;
+ std::pair<ASTNode,ASTNode> p;
+ if (other.GetNodeNum() > n.GetNodeNum())
+ p = make_pair(other,n);
+ else
+ p = make_pair(n,other);
+
+ equivs.insert(p);
+ //std::cerr << "from" << p.first << " to" << p.second;
+ //ASTNode equals = ASTNF->CreateNode(NOT,ASTNF->CreateNode(EQ,p.first,p.second));
+ //printer::SMTLIB2_PrintBack(std::cerr,p.second);
+ }
+ }
+ }
}
template<class BBNode, class BBNodeManagerT>
BBForm(const ASTNode& form);
void
- getConsts(const ASTNode& n, ASTNodeMap& fromTo);
+ getConsts(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& equivs);
};
//end of class BitBlaster
projects / francis / stp.git / commitdiff