Suspected Bug in SimplifyingNodeFactory.cpp

[Jingyue Wu]

Hi,

I ran into a stack overflow issue, and it turned out that Line 850 and
852 in SimplifyingNodeFactory.cpp are calling each other infinitely.
These two lines optimize if-then-else expressions such as (5 == a ?
a : b) to (5 == a ? 5 : b). However, if <a> is also a constant,
there's a loop.

I fixed this problem using the following patch:

Index: src/AST/NodeFactory/SimplifyingNodeFactory.cpp
===================================================================
--- src/AST/NodeFactory/SimplifyingNodeFactory.cpp (revision 1376)
+++ src/AST/NodeFactory/SimplifyingNodeFactory.cpp (working copy)
@@ -846,9 +846,9 @@
result = NodeFactory::CreateTerm(BEEV::ITE,
width, children[0], children[1][1], children[2]);
else if (children[0].GetKind() == BEEV::NOT)
result = NodeFactory::CreateTerm(BEEV::ITE,
width, children[0][0], children[2], children[1]);
- else if (children[0].GetKind() ==BEEV::EQ &&
children[0][1] == children[1] && children[0][0].GetKind() ==
BEEV::BVCONST)
+ else if (children[0].GetKind() ==BEEV::EQ &&
children[0][1] == children[1] && children[0][0].GetKind() ==
BEEV::BVCONST && children[0][1].GetKind() != BEEV::BVCONST)
result = NodeFactory::CreateTerm(BEEV::ITE,
width, children[0], children[0][0], children[2]);
- else if (children[0].GetKind() == BEEV::EQ &&
children[0][0] == children[1] && children[0][1].GetKind() ==
BEEV::BVCONST)
+ else if (children[0].GetKind() == BEEV::EQ &&
children[0][0] == children[1] && children[0][1].GetKind() ==
BEEV::BVCONST && children[0][0].GetKind() != BEEV::BVCONST)
result = NodeFactory::CreateTerm(BEEV::ITE,
width, children[0], children[0][1], children[2]);
break;
}

However, I'm wondering if it's the right fix, because, in this case,
wouldn't you simplify the condition of the if-then-else expression
beforehand?

Thanks much,
Jingyue

[Trevor Hansen]

Hello Jingyue,

I've changed the c-interface now to use the SimplifyingNode factory by
default. It was the final place that was using the HashingNode factory
by default. The HashingNode factory only checks if the node has
already been created (structural hashing/ perfect sharing). The
simplifying node factory applies simple rewrites too. This means that
if you use STP revision 1381 or later to create a node via the c-
interface like (5=6), the node you receive back will be FALSE instead
of an equality node.

I haven't wanted to use the simplifying node factory in the c-
interface because it is even more confusing --- you don't get the node
back that you expect. The type will always be the same, but the number
of parameters may differ. For instance, asking for ITE(a,b,b) will
return the 'b' node now. But the bug you reported makes me think that
there are lots more cases where mixing the node factories will cause
problems. Most of the testing of STP we do is just with the
simplifyingnode factory.

I hope this doesn't break the interface between people's tools and
STP.

Thanks for the patch. I've applied it in revision 1382.

Trev.