[proof-new] Updating interfaces between prop engine and minisat (#5664)

This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".

Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.

1 files changed, 11 insertions, 5 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index a842647bd..10ee843df 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -24,9 +24,10 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "expr/proof_node_manager.h"
 #include "proof/clause_id.h"
-#include "prop/sat_solver_types.h"
 #include "prop/bv_sat_solver_notify.h"
+#include "prop/sat_solver_types.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -122,13 +123,15 @@ public:
 
 };/* class BVSatSolverInterface */
 
-class DPLLSatSolverInterface : public SatSolver
+class CDCLTSatSolverInterface : public SatSolver
 {
  public:
-  virtual ~DPLLSatSolverInterface(){};
+  virtual ~CDCLTSatSolverInterface(){};
 
   virtual void initialize(context::Context* context,
-                          prop::TheoryProxy* theoryProxy) = 0;
+                          prop::TheoryProxy* theoryProxy,
+                          CVC4::context::UserContext* userContext,
+                          ProofNodeManager* pnm) = 0;
 
   virtual void push() = 0;
 
@@ -145,7 +148,10 @@ class DPLLSatSolverInterface : public SatSolver
   virtual void requirePhase(SatLiteral lit) = 0;
 
   virtual bool isDecision(SatVariable decn) const = 0;
-}; /* class DPLLSatSolverInterface */
+
+  virtual std::shared_ptr<ProofNode> getProof() = 0;
+
+}; /* class CDCLTSatSolverInterface */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();