Searched refs:letMap (Results 1 – 9 of 9) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | clausal_bitvector_proof.cpp | 114 ProofLetMap& letMap) in printBBDeclarationAndCnf() argument 120 d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); in printBBDeclarationAndCnf()
|
H A D | cnf_proof.h | 166 ProofLetMap &letMap) = 0; 202 ProofLetMap& letMap) override;
|
H A D | resolution_bitvector_proof.h | 104 ProofLetMap& letMap) override;
|
H A D | clausal_bitvector_proof.h | 87 ProofLetMap& letMap) override;
|
H A D | proof_manager.cpp | 1034 ProofLetMap& letMap, in printGlobalLetMap() argument 1040 bind(atom->toExpr(), letMap, letOrder); in printGlobalLetMap() 1046 bind(atom->toExpr(), letMap, letOrder); in printGlobalLetMap() 1052 ProofLetMap::iterator it = letMap.find(currentExpr); in printGlobalLetMap() 1053 Assert(it != letMap.end()); in printGlobalLetMap() 1055 d_theoryProof->printBoundTerm(currentExpr, out, letMap); in printGlobalLetMap()
|
H A D | resolution_bitvector_proof.cpp | 475 ProofLetMap& letMap) in printBBDeclarationAndCnf() argument 500 d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); in printBBDeclarationAndCnf()
|
H A D | bitvector_proof.h | 162 ProofLetMap& letMap) = 0;
|
H A D | proof_manager.h | 297 ProofLetMap& letMap,
|
H A D | cnf_proof.cpp | 408 ProofLetMap &letMap) { in printAtomMapping() argument 419 pe->printBoundTerm(atom.toExpr(), os, letMap); in printAtomMapping()
|