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/parser/tptp | |
| 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/parser/tptp')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 4 | ||||
| -rw-r--r-- | src/parser/tptp/tptp.cpp | 1 |
2 files changed, 2 insertions, 3 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 414c2f6b0..4e73fa6cf 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -527,7 +527,7 @@ fofLogicFormula[CVC4::Expr& expr] ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2] { switch(na) { case tptp::NA_IFF: - expr = MK_EXPR(kind::IFF,expr,expr2); + expr = MK_EXPR(kind::EQUAL,expr,expr2); break; case tptp::NA_REVIFF: expr = MK_EXPR(kind::XOR,expr,expr2); @@ -662,7 +662,7 @@ tffLogicFormula[CVC4::Expr& expr] ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2] { switch(na) { case tptp::NA_IFF: - expr = MK_EXPR(kind::IFF,expr,expr2); + expr = MK_EXPR(kind::EQUAL,expr,expr2); break; case tptp::NA_REVIFF: expr = MK_EXPR(kind::XOR,expr,expr2); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index ba8eb7012..dcb23d3f2 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -78,7 +78,6 @@ void Tptp::addTheory(Theory theory) { defineVar("$false", em->mkConst(false)); addOperator(kind::AND); addOperator(kind::EQUAL); - addOperator(kind::IFF); addOperator(kind::IMPLIES); //addOperator(kind::ITE); //only for tff thf addOperator(kind::NOT); |