diff options
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 34248f7eb..bbdb7d6d7 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -151,9 +151,9 @@ public: void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); - virtual void treatBoolsAsFormulas(bool value) {}; - virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; + + bool printsAsBool(const Node &n); }; class LFSCTheoryProofEngine : public TheoryProofEngine { @@ -182,7 +182,6 @@ public: void performExtraRegistrations(); - void treatBoolsAsFormulas(bool value); void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os); private: @@ -294,7 +293,11 @@ public: */ virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); - virtual void treatBoolsAsFormulas(bool value) {} + // Return true if node prints as bool, false if it prints as a formula. + virtual bool printsAsBool(const Node &n) { + // Most nodes print as formulas, so this is the default. + return false; + } }; class BooleanProof : public TheoryProof { @@ -318,7 +321,7 @@ public: class LFSCBooleanProof : public BooleanProof { public: LFSCBooleanProof(TheoryProofEngine* proofEngine) - : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true) + : BooleanProof(proofEngine) {} virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); @@ -328,12 +331,7 @@ public: virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap); - void treatBoolsAsFormulas(bool value) { - d_treatBoolsAsFormulas = value; - } - -private: - bool d_treatBoolsAsFormulas; + bool printsAsBool(const Node &n); }; } /* CVC4 namespace */ |