Home
last modified time | relevance | path

Searched refs:letMap (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dclausal_bitvector_proof.cpp114 ProofLetMap& letMap) in printBBDeclarationAndCnf() argument
120 d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); in printBBDeclarationAndCnf()
H A Dcnf_proof.h166 ProofLetMap &letMap) = 0;
202 ProofLetMap& letMap) override;
H A Dresolution_bitvector_proof.h104 ProofLetMap& letMap) override;
H A Dclausal_bitvector_proof.h87 ProofLetMap& letMap) override;
H A Dproof_manager.cpp1034 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 Dresolution_bitvector_proof.cpp475 ProofLetMap& letMap) in printBBDeclarationAndCnf() argument
500 d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); in printBBDeclarationAndCnf()
H A Dbitvector_proof.h162 ProofLetMap& letMap) = 0;
H A Dproof_manager.h297 ProofLetMap& letMap,
H A Dcnf_proof.cpp408 ProofLetMap &letMap) { in printAtomMapping() argument
419 pe->printBoundTerm(atom.toExpr(), os, letMap); in printAtomMapping()