diff options
Diffstat (limited to 'src/proof/proof_utils.cpp')
-rw-r--r-- | src/proof/proof_utils.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index fe0d42242..3ace236b5 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -41,7 +41,6 @@ std::string toLFSCKind(Kind kind) { case kind::AND: return "and"; case kind::XOR: return "xor"; case kind::EQUAL: return "="; - case kind::IFF: return "iff"; case kind::IMPLIES: return "impl"; case kind::NOT: return "not"; @@ -123,5 +122,18 @@ std::string toLFSCKind(Kind kind) { } } +std::string toLFSCKindTerm(Expr node) { + Kind k = node.getKind(); + if( k==kind::EQUAL ){ + if( node[0].getType().isBoolean() ){ + return "iff"; + }else{ + return "="; + } + }else{ + return toLFSCKind( k ); + } +} + } /* namespace CVC4::utils */ } /* namespace CVC4 */ |