diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-01 21:34:43 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-01 21:34:43 +0000 |
commit | acc653383ea5dbb3a4e9cffa5c2735a9d2f22dca (patch) | |
tree | 26cc244e1632cece509119fa4c6c928f56d9ad6c | |
parent | b8f8e92c5cdd2d556d06e722e2e27b7c18a36216 (diff) |
This commit is a fix for a bug in removeITEs(). The check that the then branch is a boolean should now be working. This fixes bug 138.
-rw-r--r-- | src/theory/theory_engine.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 476091723..1a0b25ade 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -98,10 +98,9 @@ Node TheoryEngine::removeITEs(TNode node) { } if(node.getKind() == kind::ITE){ - if(theoryOf(node[1]) != &d_bool && node[1].getKind() != kind::EQUAL) { - Assert( node.getNumChildren() == 3 ); - - Debug("ite") << theoryOf(node[1]) << " " << &d_bool <<endl; + Assert( node.getNumChildren() == 3 ); + TypeNode nodeType = node[1].getType(); + if(!nodeType.isBoolean()){ Node skolem = nodeManager->mkVar(node.getType()); Node newAssertion = @@ -112,6 +111,13 @@ Node TheoryEngine::removeITEs(TNode node) { nodeManager->mkNode(kind::EQUAL, skolem, node[2])); nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem); + if(debugTagIsOn("ite")){ + Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])" + << "->" + << "["<<newAssertion.getId() << "," << newAssertion << "]" + << endl; + } + Node preprocessed = rewrite(newAssertion); d_propEngine->assertFormula(preprocessed); |