diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/proof/proof_utils.cpp | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
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 */ |