summaryrefslogtreecommitdiff
path: root/src/prop/prop_proof_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/prop_proof_manager.h')
-rw-r--r--src/prop/prop_proof_manager.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index f3deee5bc..fc0151bcd 100644
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -39,7 +39,7 @@ class PropPfManager
public:
PropPfManager(context::UserContext* userContext,
ProofNodeManager* pnm,
- SatProofManager* satPM,
+ CDCLTSatSolverInterface* satSolver,
ProofCnfStream* cnfProof);
/** Saves assertion for later checking whether refutation proof is closed.
@@ -78,9 +78,9 @@ class PropPfManager
/** The proof post-processor */
std::unique_ptr<prop::ProofPostproccess> d_pfpp;
/**
- * The SAT solver's proof manager, which will provide a refutation
- * proofresolution proof when requested */
- SatProofManager* d_satPM;
+ * The SAT solver of this prop engine, which should provide a refutation
+ * proof when requested */
+ CDCLTSatSolverInterface* d_satSolver;
/** Assertions corresponding to the leaves of the prop engine's proof.
*
* These are kept in a context-dependent manner since the prop engine's proof
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback