diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-16 15:15:03 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-13 18:32:39 -0400 |
commit | 14776d0aeb833a7e728a27af6ef545f20b495f7f (patch) | |
tree | eccc91e0be00cfb9af7d757aae3dd07479c256fb /src/prop/minisat | |
parent | 09fc93244e10b4450592b4ede151873142d54b34 (diff) |
Documentation fixes, some code typo fixes, file perms, other minor things.
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 4 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 5 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Vec.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 8 |
5 files changed, 18 insertions, 19 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)) |