From b0609b2d70220064a44bc99e396bf0d2d5ade531 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 28 Feb 2020 21:01:49 -0800
Subject: [PATCH] propEngine: Reorder class declaration according to code style
 guidelines. (#3846)

---
 src/prop/prop_engine.h | 86 +++++++++++++++++++++---------------------
 1 file changed, 43 insertions(+), 43 deletions(-)

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 42b3ce65f..061fbbca6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -53,46 +53,8 @@ class PropEngine;
  * PropEngine is the abstraction of a Sat Solver, providing methods for
  * solving the SAT problem and conversion to CNF (via the CnfStream).
  */
-class PropEngine {
-
-  /**
-   * Indicates that the SAT solver is currently solving something and we should
-   * not mess with it's internal state.
-   */
-  bool d_inCheckSat;
-
-  /** The theory engine we will be using */
-  TheoryEngine *d_theoryEngine;
-
-  /** The decision engine we will be using */
-  DecisionEngine *d_decisionEngine;
-
-  /** The context */
-  context::Context* d_context;
-
-  /** SAT solver's proxy back to theories; kept around for dtor cleanup */
-  TheoryProxy* d_theoryProxy;
-
-  /** The SAT solver proxy */
-  DPLLSatSolverInterface* d_satSolver;
-
-  /** List of all of the assertions that need to be made */
-  std::vector<Node> d_assertionList;
-
-  /** Theory registrar; kept around for destructor cleanup */
-  theory::TheoryRegistrar* d_registrar;
-
-  /** The CNF converter in use */
-  CnfStream* d_cnfStream;
-
-  /** Whether we were just interrupted (or not) */
-  bool d_interrupted;
-  /** Pointer to resource manager for associated SmtEngine */
-  ResourceManager* d_resourceManager;
-
-  /** Dump out the satisfying assignment (after SAT result) */
-  void printSatisfyingAssignment();
-
+class PropEngine
+{
  public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
@@ -248,9 +210,47 @@ class PropEngine {
    */
   bool properExplanation(TNode node, TNode expl) const;
 
-}; /* class PropEngine */
+ private:
+  /** Dump out the satisfying assignment (after SAT result) */
+  void printSatisfyingAssignment();
+  /**
+   * Indicates that the SAT solver is currently solving something and we should
+   * not mess with it's internal state.
+   */
+  bool d_inCheckSat;
+
+  /** The theory engine we will be using */
+  TheoryEngine* d_theoryEngine;
+
+  /** The decision engine we will be using */
+  DecisionEngine* d_decisionEngine;
+
+  /** The context */
+  context::Context* d_context;
+
+  /** SAT solver's proxy back to theories; kept around for dtor cleanup */
+  TheoryProxy* d_theoryProxy;
+
+  /** The SAT solver proxy */
+  DPLLSatSolverInterface* d_satSolver;
+
+  /** List of all of the assertions that need to be made */
+  std::vector<Node> d_assertionList;
+
+  /** Theory registrar; kept around for destructor cleanup */
+  theory::TheoryRegistrar* d_registrar;
+
+  /** The CNF converter in use */
+  CnfStream* d_cnfStream;
+
+  /** Whether we were just interrupted (or not) */
+  bool d_interrupted;
+  /** Pointer to resource manager for associated SmtEngine */
+  ResourceManager* d_resourceManager;
+
+};
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC4
 
 #endif /* CVC4__PROP_ENGINE_H */
-- 
2.30.2