diff options
Diffstat (limited to 'src/theory/bv/aig_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index bb2c403aa..934e2fffd 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -194,15 +194,6 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { } break; } - case kind::IFF: - { - Assert (node.getNumChildren() == 2); - Abc_Obj_t* child1 = bbFormula(node[0]); - Abc_Obj_t* child2 = bbFormula(node[1]); - - result = mkIff(child1, child2); - break; - } case kind::XOR: { result = bbFormula(node[0]); @@ -247,6 +238,18 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { result = mkInput(node); break; } + case kind::EQUAL: + { + if( node[0].getType().isBoolean() ){ + Assert (node.getNumChildren() == 2); + Abc_Obj_t* child1 = bbFormula(node[0]); + Abc_Obj_t* child2 = bbFormula(node[1]); + + result = mkIff(child1, child2); + break; + } + //else, continue... + } default: bbAtom(node); result = getBBAtom(node); |