add documentations, fix space issues

3 files changed, 5 insertions, 8 deletions

diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index 8907dc72f..c849c8520 100644
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -49,9 +49,12 @@ class NonClausalSimp : public PreprocessingPass
   /** Learned literals */
   std::vector<Node> d_nonClausalLearnedLiterals;
 
+  /** Solve the boolean skeleton with Cryptominisat */
   SatValue solveByCryptominisat(CVC4::prop::TseitinCnfStream* d_cnfStream,
                                 AssertionPipeline* assertionsToPreprocess,
                                 unsigned substs_index);
+
+  /** Solve the boolean skeleton with circuit propagator */
   bool solveByCircuitPropagator(theory::booleans::CircuitPropagator* propagator,
                                 AssertionPipeline* assertionsToPreprocess,
                                 unsigned substs_index);
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e3ca04e64..cdb850ce2 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -675,13 +675,10 @@ void TseitinCnfStream::convertAndAssert(TNode node,
                                         bool negated,
                                         ProofRule proof_id,
                                         TNode from) {
-
   Debug("cnf") << "convertAndAssert(" << node
                << ", removable = " << (removable ? "true" : "false")
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
   d_removable = removable;
-
-
   PROOF
     (if (d_cnfProof) {
       Node assertion = negated ? node.notNode() : (Node)node;
@@ -698,12 +695,10 @@ void TseitinCnfStream::convertAndAssert(TNode node,
     });
 
   convertAndAssert(node, negated);
-
   PROOF
     (if (d_cnfProof) {
       d_cnfProof->popCurrentAssertion();
     });
-
 }
 
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index a775501ff..5328206b1 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -198,10 +198,9 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const {
 }
 
 std::vector<SatLiteral> CryptoMinisatSolver::getTopLevelUnits(){
-  std::vector<CMSat::Lit> lits = d_solver->get_zero_assigned_lits();
   std::vector<SatLiteral> satLits;
-  for (int i = 0; i < lits.size(); i++){
-    satLits.push_back(toSatLiteral(lits[i]));
+  for (const auto& lit : d_solver->get_zero_assigned_lits()){
+    satLits.push_back(toSatLiteral(lit));
   }
   return satLits;
 }