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/theory_proof.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/theory_proof.cpp')
| -rw-r--r-- | src/proof/theory_proof.cpp | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 1912dbada..156c90e47 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -856,9 +856,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro case kind::EQUAL: os << "("; - os << "= "; - printSort(term[0].getType(), os); - os << " "; + if( term[0].getType().isBoolean() ){ + os << "iff "; + }else{ + os << "= "; + printSort(term[0].getType(), os); + os << " "; + } printBoundTerm(term[0], os, map); os << " "; printBoundTerm(term[1], os, map); @@ -912,6 +916,12 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro // LFSC doesn't allow declarations with variable numbers of // arguments, so we have to flatten chained operators, like =. Kind op = term.getOperator().getConst<Chain>().getOperator(); + std::string op_str; + if( op==kind::EQUAL && term[0].getType().isBoolean() ){ + op_str = "iff"; + }else{ + op_str = utils::toLFSCKind(op); + } size_t n = term.getNumChildren(); std::ostringstream paren; for(size_t i = 1; i < n; ++i) { @@ -919,7 +929,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro os << "(" << utils::toLFSCKind(kind::AND) << " "; paren << ")"; } - os << "(" << utils::toLFSCKind(op) << " "; + os << "(" << op_str << " "; printBoundTerm(term[i - 1], os, map); os << " "; printBoundTerm(term[i], os, map); @@ -1096,7 +1106,6 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe // If letification is off or there were 2 children, same treatment as the other cases. // (No break is intentional). case kind::XOR: - case kind::IFF: case kind::IMPLIES: case kind::NOT: // print the Boolean operators |