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/compat | |
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/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index e681b831b..4f4101d7e 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -290,7 +290,7 @@ Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { } Expr Expr::iffExpr(const Expr& right) const { - return getEM()->mkExpr(CVC4::kind::IFF, *this, right); + return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right); } Expr Expr::impExpr(const Expr& right) const { @@ -434,9 +434,11 @@ bool Expr::isAtomicFormula() const { case CVC4::kind::AND: case CVC4::kind::OR: case CVC4::kind::ITE: - case CVC4::kind::IFF: case CVC4::kind::IMPLIES: return false; + case CVC4::kind::EQUAL: + return (*this)[0].getType().isBool(); + break; default: ; /* fall through */ } @@ -469,10 +471,12 @@ bool Expr::isBoolConnective() const { case CVC4::kind::AND: case CVC4::kind::OR: case CVC4::kind::IMPLIES: - case CVC4::kind::IFF: case CVC4::kind::XOR: case CVC4::kind::ITE: return true; + case CVC4::kind::EQUAL: + return (*this)[0].getType().isBool(); + break; default: return false; } @@ -547,7 +551,7 @@ bool Expr::isITE() const { } bool Expr::isIff() const { - return getKind() == CVC4::kind::IFF; + return getKind() == CVC4::kind::EQUAL && (*this)[0].getType().isBool();; } bool Expr::isImpl() const { @@ -1663,7 +1667,7 @@ Expr ValidityChecker::impliesExpr(const Expr& hyp, const Expr& conc) { } Expr ValidityChecker::iffExpr(const Expr& left, const Expr& right) { - return d_em->mkExpr(CVC4::kind::IFF, left, right); + return d_em->mkExpr(CVC4::kind::EQUAL, left, right); } Expr ValidityChecker::eqExpr(const Expr& child0, const Expr& child1) { |