You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In several cases (when we perform simplification) we must know the size of the root BVNODE. To do that, we must compute the AST. (c.f: concat, extract, bv, sx, zx).
The method node.getBitvectorSize() returns the current size of the root node. Which means that we can now perform simplification like this:
/* if (bvxor x x) -> (_ bv0 x_size) */
smt2lib::smtAstAbstractNode* xor_simplification(smt2lib::smtAstAbstractNode* node) {
if (node->getKind() == smt2lib::BVXOR_NODE) {
if (*(node->getChilds()[0]) == *(node->getChilds()[1]))
returnsmt2lib::bv(0, node->getBitvectorSize());
}
return node;
}
In several cases (when we perform simplification) we must know the size of the root
BVNODE
. To do that, we must compute the AST. (c.f: concat, extract, bv, sx, zx).The method
node.getBitvectorSize()
returns the current size of the root node. Which means that we can now perform simplification like this:Related to #226 and #93. Done with the next v0.3.
The text was updated successfully, but these errors were encountered: