fix style

4 files changed, 26 insertions, 30 deletions

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 5328206b1..77cc6be4d 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -58,6 +58,17 @@ void toInternalClause(SatClause& clause,
   Assert(clause.size() == internal_clause.size());
 }
 
+SatLiteral toSatLiteral(CMSat::Lit lit)
+{
+  if (lit == CMSat::lit_Undef)
+  {
+    return undefSatLiteral;
+  }
+
+  return SatLiteral(lit.var(), lit.sign());
+}
+}  // namespace
+
 }  // helper functions
 
 CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
@@ -176,7 +187,8 @@ SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
   return toSatLiteralValue(d_solver->solve(&assumpts));
 }
 
-SatValue CryptoMinisatSolver::simp(){
+SatValue CryptoMinisatSolver::simplify()
+{
   return toSatLiteralValue(d_solver->simplify());
 }
   
@@ -205,15 +217,6 @@ std::vector<SatLiteral> CryptoMinisatSolver::getTopLevelUnits(){
   return satLits;
 }
 
-SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) {
-  if (lit == CMSat::lit_Undef) {
-    return undefSatLiteral;
-  }
-
-  return SatLiteral(lit.var(),
-                    lit.sign());
-}
-
 // Satistics for CryptoMinisatSolver
 
 CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 2450c1736..13416bb3d 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -21,8 +21,6 @@
 
 #ifdef CVC4_USE_CRYPTOMINISAT
 
-#include <cryptominisat5/cryptominisat.h>  
-
 #include "prop/sat_solver.h"
 
 // Cryptominisat has name clashes with the other Minisat implementations since
@@ -80,8 +78,6 @@ public:
 
   std::vector<SatLiteral> getTopLevelUnits() override;
 
-  SatLiteral toSatLiteral(CMSat::Lit lit);
-
   class Statistics {
   public:
     StatisticsRegistry* d_registry;
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 25b2ccc39..2d8fd460a 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -83,11 +83,8 @@ public:
   };
 
   /** Simplify the formula **/
-  virtual SatValue simp(){
-    return SAT_VALUE_UNKNOWN;
-  };
+  virtual SatValue simplify() { return SAT_VALUE_UNKNOWN; };
 
-  
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 05f8fef61..f721b88ae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2195,7 +2195,7 @@ void SmtEngine::setDefaults() {
     {
       throw OptionException(std::string(
           "Cannot use MipLibTrick when using cryptominisat instead of circuit"
-          "propagators. Try turn off --skeletonPreprocessing"));
+          "propagators. Try turn off --skeleton-preprocessing"));
     }
     else if (options::skeletonPreprocessing.wasSetByUser()){
           setOption("skeleton-preprocessing", false);
@@ -2667,7 +2667,7 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("nl-ext-purify",
                                            std::move(nlExtPurify));
   d_preprocessingPassRegistry.registerPass("non-clausal-simp",
-                                            std::move(nonClausalSimp));
+                                           std::move(nonClausalSimp));
   d_preprocessingPassRegistry.registerPass("miplib-trick",
                                            std::move(mipLibTrick));
   d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
@@ -2909,9 +2909,9 @@ bool SmtEnginePrivate::simplifyAssertions()
             d_preprocessingPassRegistry.getPass("non-clausal-simp")
                 ->apply(&d_assertions);
         if (res == PreprocessingPassResult::CONFLICT)
-          {
-            return false;
-          }
+        {
+          return false;
+        }
       }
 
       // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
@@ -2975,13 +2975,13 @@ bool SmtEnginePrivate::simplifyAssertions()
         && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
         && !options::unsatCores() && !options::fewerPreprocessingHoles())
     {
-        PreprocessingPassResult res =
-            d_preprocessingPassRegistry.getPass("non-clausal-simp")
-                ->apply(&d_assertions);
-        if (res == PreprocessingPassResult::CONFLICT)
-        {
-          return false;
-        }
+      PreprocessingPassResult res =
+          d_preprocessingPassRegistry.getPass("non-clausal-simp")
+              ->apply(&d_assertions);
+      if (res == PreprocessingPassResult::CONFLICT)
+      {
+	return false;
+      }
     }
 
     dumpAssertions("post-repeatsimp", d_assertions);