| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | theory_proof.h | 113 …ntAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
153 …printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
186 const ProofLetMap& globalLetMap) override;
336 …ntAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
348 …printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
393 const ProofLetMap& globalLetMap) override;
399 const ProofLetMap& globalLetMap) override;
|
| H A D | uf_proof.h | 92 const ProofLetMap& globalLetMap) override;
99 const ProofLetMap& globalLetMap) override;
|
| H A D | proof_manager.cpp | 703 ProofLetMap globalLetMap; in toStream() local
705 ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren); in toStream()
709 d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap); in toStream()
715 printPreprocessedAssertions(used_assertions, out, paren, globalLetMap); in toStream()
719 d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap); in toStream()
732 d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap); in toStream()
751 ProofLetMap& globalLetMap) const in printPreprocessedAssertions()
814 ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap); in printPreprocessedAssertions()
837 ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap); in printPreprocessedAssertions()
1068 ProofLetMap& globalLetMap) in printTrustedTerm() argument
[all …]
|
| H A D | bitvector_proof.h | 264 const ProofLetMap& globalLetMap) override;
269 const ProofLetMap& globalLetMap) override;
|
| H A D | theory_proof.cpp | 169 …rintConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { in printConstantDisequalityProof() argument
174 …TheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2, globalLetMap); in printConstantDisequalityProof()
442 …printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { in printAliasingDeclarations() argument
448 it->second->printAliasingDeclarations(os, paren, globalLetMap); in printAliasingDeclarations()
1137 …rintConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { in printConstantDisequalityProof() argument
1257 …printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { in printAliasingDeclarations() argument
1281 …rintConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { in printConstantDisequalityProof() argument
1286 d_proofEngine->printBoundTerm(c1, os, globalLetMap); in printConstantDisequalityProof()
1288 d_proofEngine->printBoundTerm(c2, os, globalLetMap); in printConstantDisequalityProof()
|
| H A D | proof_manager.h | 248 ProofLetMap& globalLetMap);
339 ProofLetMap& globalLetMap) const;
|
| H A D | arith_proof.h | 169 const ProofLetMap& globalLetMap) override;
|
| H A D | array_proof.h | 112 const ProofLetMap& globalLetMap) override;
|
| H A D | bitvector_proof.cpp | 405 const ProofLetMap& globalLetMap) in printAliasingDeclarations() argument
423 d_proofEngine->printBoundTerm(it->first, os, globalLetMap); in printAliasingDeclarations()
740 std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap) in printConstantDisequalityProof() argument
|
| H A D | uf_proof.cpp | 721 …printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { in printAliasingDeclarations() argument
732 …rintConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { in printConstantDisequalityProof() argument
|
| H A D | arith_proof.cpp | 1187 …printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { in printAliasingDeclarations() argument
|
| H A D | array_proof.cpp | 1324 …printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { in printAliasingDeclarations() argument
|