From: Dejan Jovanović Date: Wed, 13 Apr 2011 21:15:48 +0000 (+0000) Subject: adding support for unit conflicts in minisat... X-Git-Tag: cvc5-1.0.0~8600 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08c5c6410ab89ffc1b7326347d11009e216676aa;p=cvc5.git adding support for unit conflicts in minisat... --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 10cd02f94..02eecf858 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -103,7 +103,8 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) -{} +{ +} Solver::~Solver() @@ -709,19 +710,30 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort) SatClause clause; proxy->theoryCheck(effort, clause); int clause_size = clause.size(); - Assert(clause_size != 1, "Can't handle unit clause explanations"); if(clause_size > 0) { - // Find the max level of the conflict + // Do some normalization + sort(clause); + // Find the max level of the conflict and normalize the clause int max_level = 0; int max_intro_level = 0; - for (int i = 0; i < clause_size; ++i) { + int i, j = 0; + Lit p; + for (i = 0; i < clause_size; ++i) { + if (clause[i] == p) continue; 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_Undef, "Got an unassigned literal in conflict!"); + Assert(value(clause[i]) == l_False, "Got an non-true 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); } // 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 1eb407c62..65fcf32a0 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -82,6 +82,9 @@ 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 8bcd9fe76..27ccaacfd 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -67,6 +67,12 @@ 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); }