Searched refs:cnfStream (Results 1 – 10 of 10) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | cnf_proof.h | 93 CnfProof(CVC4::prop::CnfStream* cnfStream,
188 LFSCCnfProof(CVC4::prop::CnfStream* cnfStream, in LFSCCnfProof() argument
191 : CnfProof(cnfStream, ctx, name) in LFSCCnfProof()
|
| H A D | clausal_bitvector_proof.cpp | 46 void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, in initCnfProof() argument
52 d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); in initCnfProof()
|
| H A D | resolution_bitvector_proof.h | 72 void initCnfProof(prop::CnfStream* cnfStream,
|
| H A D | clausal_bitvector_proof.h | 51 void initCnfProof(prop::CnfStream* cnfStream,
|
| H A D | resolution_bitvector_proof.cpp | 58 void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, in initCnfProof() argument
65 d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); in initCnfProof()
|
| H A D | bitvector_proof.h | 197 virtual void initCnfProof(prop::CnfStream* cnfStream,
|
| H A D | proof_manager.h | 183 static void initCnfProof(CVC4::prop::CnfStream* cnfStream,
|
| H A D | proof_manager.cpp | 150 void ProofManager::initCnfProof(prop::CnfStream* cnfStream, in initCnfProof() argument
156 CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, ""); in initCnfProof()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | theory_proxy.cpp | 42 CnfStream* cnfStream, in TheoryProxy() argument
47 d_cnfStream(cnfStream), in TheoryProxy()
|
| H A D | theory_proxy.h | 58 CnfStream* cnfStream,
|