From 225f4e77f3afdebdfa046834ef7c006b9b8ec77c Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 14 Apr 2011 20:57:28 +0000 Subject: [PATCH] reverting back the minisat code and adding a simpler one that shouldn't change the search --- src/prop/minisat/core/Solver.cc | 24 ++++++++---------------- src/prop/minisat/core/Solver.h | 3 --- src/prop/minisat/simp/SimpSolver.cc | 6 ------ 3 files changed, 8 insertions(+), 25 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 1e334f7e4..c2d53bef8 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -103,8 +103,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) -{ -} +{} Solver::~Solver() @@ -711,29 +710,22 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort) proxy->theoryCheck(effort, clause); int clause_size = clause.size(); if(clause_size > 0) { - // Do some normalization - sort(clause); - // Find the max level of the conflict and normalize the clause + // Find the max level of the conflict int max_level = 0; int max_intro_level = 0; - int i, j = 0; - Lit p = lit_Undef; - for (i = 0; i < clause_size; ++i) { - if (clause[i] == p) continue; + for (int i = 0; i < clause_size; ++i) { Var v = var(clause[i]); int current_level = level(v); int current_intro_level = intro_level(v); Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(v) << " at level " << current_level << std::endl; - Assert(value(clause[i]) == l_False, "Got an non-true literal in conflict!"); + Assert(value(clause[i]) != l_Undef, "Got an unassigned literal in conflict!"); if (current_level > max_level) max_level = current_level; if (current_intro_level > max_intro_level) max_intro_level = current_intro_level; - p = clause[j ++] = clause[i]; } - clause.shrink(i - j); - // If there is only one literal add an extra false literal - if (clause.size() == 1) { - Debug("unit-conflicts") << "Unit conflict!" << proxy->getNode(clause[0]) << std::endl; - clause.push(false_literal); + // Unit conflict, we just duplicate the first literal + if (clause_size == 1) { + clause.push(clause[0]); + Debug("unit-conflict") << "Unit conflict" << proxy->getNode(clause[0]) << std::endl; } // If smaller than the decision level then pop back so we can analyse Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 65fcf32a0..1eb407c62 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -82,9 +82,6 @@ protected: /** True if we are currently solving. */ bool in_solve; - /** The variable representing Boolean true value */ - Lit false_literal; - public: // Constructor/Destructor: diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 27ccaacfd..8bcd9fe76 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -67,12 +67,6 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. bwdsub_tmpunit = ca.alloc(0, dummy); remove_satisfied = false; - - // Add the true literal immediately - Var true_variable = newVar(false, false, false); - setFrozen(true_variable, true); - false_literal = mkLit(true_variable, true); - uncheckedEnqueue(~false_literal, CRef_Undef); } -- 2.30.2