diff options
| author | guykatzz <katz911@gmail.com> | 2017-03-09 12:13:12 -0800 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2017-03-09 12:14:15 -0800 |
| commit | 2f287a59e9c775d9087cddd8c72be5169c2706e1 (patch) | |
| tree | 95a6664e3b013929d9190cff2d1889045e1a2af2 /src/proof/array_proof.cpp | |
| parent | ab68adfc44049598ee79a3c8b4379694d786d9aa (diff) | |
better proof support for bools and formulas
Diffstat (limited to 'src/proof/array_proof.cpp')
| -rw-r--r-- | src/proof/array_proof.cpp | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index cc60d8c07..af158f37b 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -1197,8 +1197,11 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE)); switch (term.getKind()) { - case kind::SELECT: + case kind::SELECT: { Assert(term.getNumChildren() == 2); + + bool convertToBool = (term[1].getType().isBoolean() && !d_proofEngine->printsAsBool(term[1])); + os << "(apply _ _ (apply _ _ (read "; printSort(ArrayType(term[0].getType()).getIndexType(), os); os << " "; @@ -1206,9 +1209,12 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM os << ") "; printTerm(term[0], os, map); os << ") "; + if (convertToBool) os << "(f_to_b "; printTerm(term[1], os, map); + if (convertToBool) os << ")"; os << ") "; return; + } case kind::PARTIAL_SELECT_0: Assert(term.getNumChildren() == 1); @@ -1381,7 +1387,15 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p } void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { - // Nothing to do here at this point. + // Nothing to do here at this point. +} + +bool LFSCArrayProof::printsAsBool(const Node &n) +{ + if (n.getKind() == kind::SELECT) + return true; + + return false; } } /* CVC4 namespace */ |