diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:19:22 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:19:22 +0000 |
commit | 04fd25e4201130776015fd3179631a97f27da12a (patch) | |
tree | d3559b078c2a1c0e95a1bf49142a81c80cf69814 /src | |
parent | cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 (diff) |
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/minisat/core/Solver.C | 9 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 3 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 4 |
3 files changed, 10 insertions, 6 deletions
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index 5ad647baa..e54884925 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -141,6 +141,7 @@ void Solver::attachClause(Clause& c) { void Solver::detachClause(Clause& c) { + Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); assert(find(watches[toInt(~c[0])], &c)); assert(find(watches[toInt(~c[1])], &c)); @@ -151,8 +152,10 @@ void Solver::detachClause(Clause& c) { void Solver::removeClause(Clause& c) { + Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl; detachClause(c); - free(&c); } + free(&c); +} bool Solver::satisfied(const Clause& c) const { @@ -440,8 +443,8 @@ Clause* Solver::propagateTheory() SatClause clause; proxy->theoryCheck(clause); if (clause.size() > 0) { - Clause* c = Clause_new(clause, false); - clauses.push(c); + c = Clause_new(clause, true); + learnts.push(c); attachClause(*c); } return c; diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index a2e46e2e4..057dfdbe2 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -65,7 +65,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { n_occ .push(0); n_occ .push(0); occurs .push(); - frozen .push((char)false); + frozen .push((char)theoryAtom); touched .push(0); elim_heap.insert(v); elimtable.push(); @@ -156,6 +156,7 @@ bool SimpSolver::addClause(vec<Lit>& ps) void SimpSolver::removeClause(Clause& c) { + Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl; assert(!c.learnt()); if (use_simplification) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 96154063d..ef28a4ac6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -66,14 +66,14 @@ void PropEngine::assertLemma(TNode node) { Result PropEngine::checkSat() { Assert(!d_inCheckSat, "Sat solver in solve()!"); - Debug("prop") << "solve()" << endl; + Debug("prop") << "PropEngine::checkSat()" << endl; // Mark that we are in the checkSat d_inCheckSat = true; // Check the problem bool result = d_satSolver->solve(); // Not in checkSat any more d_inCheckSat = false; - Debug("prop") << "solve() => " << (result ? "true" : "false") << endl; + Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl; return Result(result ? Result::SAT : Result::UNSAT); } |