From e202cfe4fded0a005d4da8d0e2da48595e10ce74 Mon Sep 17 00:00:00 2001 From: "lperron@google.com" Date: Fri, 13 Jul 2012 16:30:18 +0000 Subject: [PATCH] more tests on minisat --- examples/tests/boolean_test.cc | 24 +++++++++++++++++++++++- src/constraint_solver/booleans.cc | 2 +- 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/examples/tests/boolean_test.cc b/examples/tests/boolean_test.cc index 15acf35ee2..5bb300e148 100644 --- a/examples/tests/boolean_test.cc +++ b/examples/tests/boolean_test.cc @@ -105,7 +105,28 @@ void TestBoolEq() { solver.AddConstraint(reinterpret_cast(sat)); IntVar* const x = solver.MakeBoolVar("x"); IntVar* const y = solver.MakeBoolVar("y"); - CHECK(AddBoolEq(sat, x, solver.MakeDifference(1, y))); + CHECK(AddBoolEq(sat, x, y)); + DecisionBuilder* const db = + solver.MakePhase(x, y, + Solver::CHOOSE_FIRST_UNBOUND, + Solver::ASSIGN_MIN_VALUE); + solver.NewSearch(db); + while (solver.NextSolution()) { + LOG(INFO) << " x = " << x->Value() << ", y = " << y->Value(); + } + solver.EndSearch(); + CHECK_EQ(2, solver.solutions()); + LOG(INFO) << solver.DebugString(); +} + +void TestBoolNot() { + LOG(INFO) << "TestBoolNot"; + Solver solver("TestBoolNot"); + SatPropagator* const sat = MakeSatPropagator(&solver); + solver.AddConstraint(reinterpret_cast(sat)); + IntVar* const x = solver.MakeBoolVar("x"); + IntVar* const y = solver.MakeBoolVar("y"); + CHECK(AddBoolNot(sat, x, y)); DecisionBuilder* const db = solver.MakePhase(x, y, Solver::CHOOSE_FIRST_UNBOUND, @@ -240,6 +261,7 @@ int main(int argc, char** argv) { operations_research::TestConversions(); operations_research::TestBoolLe(); operations_research::TestBoolEq(); + operations_research::TestBoolNot(); operations_research::TestBoolAndEq(); operations_research::TestBoolOrEq(); operations_research::TestBoolIsEq(); diff --git a/src/constraint_solver/booleans.cc b/src/constraint_solver/booleans.cc index bd84e4e085..b931ac53cb 100644 --- a/src/constraint_solver/booleans.cc +++ b/src/constraint_solver/booleans.cc @@ -82,7 +82,7 @@ class SatPropagator : public Constraint { } void VariableBound(int index) { - if (num_bound_literals_.Value() <= minisat_.decisionLevel()) { + if (num_bound_literals_.Value() < minisat_.decisionLevel()) { minisat_.cancelUntil(num_bound_literals_.Value()); } VLOG(1) << "VariableBound: " << vars_[index]->DebugString();