Documentation fixes, some code typo fixes, file perms, other minor things.

6 files changed, 20 insertions, 21 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index cacde258d..36e196821 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -231,7 +231,7 @@ CRef Solver::reason(Var x) {
     int i, j;
     Lit prev = lit_Undef;
     for (i = 0, j = 0; i < explanation.size(); ++ i) {
-      // This clause is valid theory propagation, so it's level is the level of the top literal
+      // This clause is valid theory propagation, so its level is the level of the top literal
       explLevel = std::max(explLevel, intro_level(var(explanation[i])));
 
       Assert(value(explanation[i]) != l_Undef);
@@ -348,7 +348,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
           PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } )
-          return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef);
+          return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef);
         } else return ok;
       }
     }
@@ -806,7 +806,7 @@ CRef Solver::propagate(TheoryCheckType type)
         // Propagate on the clauses
         confl = propagateBool();
         // If no conflict, do the theory check
-        if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
+        if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
             // Do the theory check
             if (type == CHECK_FINAL_FAKE) {
               theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
@@ -1019,8 +1019,8 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (c.level() > level) {
-          assert(!locked(c));
-          removeClause(cs[i]);
+            assert(!locked(c));
+            removeClause(cs[i]);
         } else {
             cs[j++] = cs[i];
         }
@@ -1050,7 +1050,7 @@ bool Solver::simplify()
 {
     assert(decisionLevel() == 0);
 
-    if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef)
+    if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef)
         return ok = false;
 
     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
@@ -1212,7 +1212,7 @@ lbool Solver::search(int nof_conflicts)
 
                 if (next == lit_Undef) {
                     // We need to do a full theory check to confirm
-                  Debug("minisat::search") << "Doing a full theoy check..."
+                  Debug("minisat::search") << "Doing a full theory check..."
                                            << std::endl;
                     check_type = CHECK_FINAL;
                     continue;
@@ -1492,7 +1492,7 @@ void Solver::pop()
     Debug("minisat") << "== unassigning " << trail.last() << std::endl;
     Var      x  = var(trail.last());
     if (user_level(x) > assertionLevel) {
-      assigns [x] = l_Undef;
+      assigns[x] = l_Undef;
       vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1);
       if(phase_saving >= 1 && (polarity[x] & 0x2) == 0)
         polarity[x] = sign(trail.last());
@@ -1505,7 +1505,7 @@ void Solver::pop()
   // The head should be at the trail top
   qhead = trail.size();
 
-  // Remove the clause
+  // Remove the clauses
   removeClausesAboveLevel(clauses_persistent, assertionLevel);
   removeClausesAboveLevel(clauses_removable, assertionLevel);
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 55780479a..30d72ac75 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -266,7 +266,7 @@ protected:
       int level;
       // User level when the literal was added to the trail
       int user_level;
-      // Use level at which this literal was introduced
+      // User level at which this literal was introduced
       int intro_level;
       // The index in the trail
       int trail_index;
@@ -335,7 +335,7 @@ protected:
 
     enum TheoryCheckType {
       // Quick check, but don't perform theory reasoning
-      CHECK_WITHOUTH_THEORY,
+      CHECK_WITHOUT_THEORY,
       // Check and perform theory reasoning
       CHECK_WITH_THEORY,
       // The SAT abstraction of the problem is satisfiable, perform a full theory check
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 37e471846..ec49b5f71 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -30,16 +30,15 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
   /** The SatSolver used */
   Minisat::SimpSolver* d_minisat;
 
-
   /** The SatSolver uses this to communicate with the theories */
   TheoryProxy* d_theoryProxy;
 
-  /** Context we will be using to synchronzie the sat solver */
+  /** Context we will be using to synchronize the sat solver */
   context::Context* d_context;
 
 public:
 
-  MinisatSatSolver ();
+  MinisatSatSolver();
   ~MinisatSatSolver();
 
   static SatVariable     toSatVariable(Minisat::Var var);
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 5d8c2850e..5f85f6fcd 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -86,7 +86,7 @@ public:
     const T& operator [] (int index) const { return data[index]; }
     T&       operator [] (int index)       { return data[index]; }
 
-    // Duplicatation (preferred instead):
+    // Duplication (preferred instead):
     void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 0e0e5d3ae..6dcdb76c7 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -67,7 +67,7 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c
     if(options::minisatUseElim() &&
        options::minisatUseElim.wasSetByUser() &&
        enableIncremental) {
-        WarningOnce() << "Incremental mode incompatible with --minisat-elimination" << std::endl;
+        WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl;
     }
 
     vec<Lit> dummy(1,lit_Undef);
@@ -239,7 +239,7 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l)
         updateElimHeap(var(l));
     }
 
-    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true;
+    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUT_THEORY) == CRef_Undef : true;
 }
 
 
@@ -346,7 +346,7 @@ bool SimpSolver::implied(const vec<Lit>& c)
             uncheckedEnqueue(~c[i]);
         }
 
-    bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef;
+    bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
     cancelUntil(0);
     return result;
 }
@@ -435,7 +435,7 @@ bool SimpSolver::asymm(Var v, CRef cr)
         else
             l = c[i];
 
-    if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){
+    if (propagate(CHECK_WITHOUT_THEORY) != CRef_Undef){
         cancelUntil(0);
         asymm_lits++;
         if (!strengthenClause(cr, l))
diff --git a/src/prop/options b/src/prop/options
index e3a0f814a..b300c3fb6 100644
--- a/src/prop/options
+++ b/src/prop/options
@@ -22,8 +22,8 @@ option satRestartFirst --restart-int-base=N unsigned :default 25
 option satRestartInc --restart-int-inc=F double :default 3.0 :predicate greater_equal(0.0)
  sets the restart interval increase factor for the sat solver (F=3.0 by default)
 
-option sat_refine_conflicts --refine-conflicts bool
- refine theory conflict clauses
+option sat_refine_conflicts --refine-conflicts bool :default false
+ refine theory conflict clauses (default false)
 
 option minisatUseElim --minisat-elimination bool :default true :read-write 
  use Minisat elimination