Home
last modified time | relevance | path

Searched refs:constructProof (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dsat_proof.h197 void constructProof(ClauseId id);
198 void constructProof() { constructProof(d_emptyClauseId); } in constructProof() function
H A Dresolution_bitvector_proof.cpp135 d_resolutionProof->constructProof(); in finalizeConflicts()
H A Dproof_manager.cpp373 d_satProof->constructProof(); in constructSatProof()
567 d_satProof->constructProof(); in toStream()
H A Dsat_proof_implementation.h924 void TSatProof<Solver>::constructProof(ClauseId conflict) { in constructProof() function