00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include "test.h"
00021 #include <clasp/solver.h>
00022 #include <clasp/clause.h>
00023 #include <algorithm>
00024 #ifdef _MSC_VER
00025 #pragma warning (disable : 4267) // conversion from 'size_t' to unsigned int
00026 #pragma once
00027 #endif
00028
00029
00030 namespace Clasp { namespace Test {
00031 using namespace Clasp::mt;
00032 class SharedClauseTest : public CppUnit::TestFixture {
00033 CPPUNIT_TEST_SUITE(SharedClauseTest);
00034 CPPUNIT_TEST(testClauseCtorAddsWatches);
00035 CPPUNIT_TEST(testPropSharedClauseConflict);
00036 CPPUNIT_TEST(testPropRandomClauses);
00037 CPPUNIT_TEST(testPropAlreadySatisfied);
00038 CPPUNIT_TEST(testReasonBumpsActivityIfLearnt);
00039 CPPUNIT_TEST(testSimplifySAT);
00040 CPPUNIT_TEST(testSimplifyUnique);
00041 CPPUNIT_TEST(testSimplifyShared);
00042
00043 CPPUNIT_TEST(testCloneShared);
00044 CPPUNIT_TEST_SUITE_END();
00045 public:
00046 SharedClauseTest() {
00047 a1 = posLit(ctx.addVar(Var_t::atom_var));
00048 a2 = posLit(ctx.addVar(Var_t::atom_var));
00049 a3 = posLit(ctx.addVar(Var_t::atom_var));
00050 b1 = posLit(ctx.addVar(Var_t::body_var));
00051 b2 = posLit(ctx.addVar(Var_t::body_var));
00052 b3 = posLit(ctx.addVar(Var_t::body_var));
00053
00054 for (int i = 6; i < 15; ++i) {
00055 ctx.addVar(Var_t::atom_var);
00056 }
00057 ctx.startAddConstraints(10);
00058 }
00059 void testClauseCtorAddsWatches() {
00060 makeLits(2, 2);
00061 ClauseHead* sharedCl= createShared(ctx, clLits, ClauseInfo());
00062 ctx.add(sharedCl);
00063 CPPUNIT_ASSERT_EQUAL(2, countWatches(*ctx.master(), sharedCl, clLits));
00064 }
00065
00066 void testPropSharedClauseConflict() {
00067 makeLits(2, 2);
00068 ClauseHead* c = createShared(ctx, clLits, ClauseInfo());
00069 simplePropTest(c);
00070 }
00071
00072 void testPropRandomClauses() {
00073 for (int i = 0; i != 100; ++i) {
00074 SharedContext cc;
00075 cc.master()->strategy.initWatches = SolverStrategies::watch_rand;
00076 for (int j = 0; j < 12; ++j) { cc.addVar(Var_t::atom_var); }
00077 cc.startAddConstraints(1);
00078
00079 makeRandomClause( (rand() % 10) + 2 );
00080 ClauseHead* c = createShared(cc, clLits, ClauseInfo());
00081 cc.add(c);
00082 check(*cc.master(), c);
00083 }
00084 }
00085
00086 void testPropAlreadySatisfied() {
00087 makeLits(2, 2);
00088 ClauseHead* c1 = createShared(ctx, clLits, ClauseInfo());
00089 ctx.add(c1);
00090
00091
00092 ctx.addUnary(clLits[3]);
00093 ctx.master()->propagate();
00094
00095
00096 ctx.addUnary(~clLits[0]);
00097 ctx.addUnary(~clLits[1]);
00098 ctx.master()->propagate();
00099
00100
00101 CPPUNIT_ASSERT(value_free == ctx.master()->value(clLits[2].var()));
00102 }
00103
00104 void testReasonBumpsActivityIfLearnt() {
00105 makeLits(4, 0);
00106 ctx.endInit();
00107 ClauseInfo e(Constraint_t::learnt_conflict);
00108 ClauseHead* c = createShared(ctx, clLits, e);
00109 Solver& solver= *ctx.master();
00110 solver.addLearnt(c, (uint32)clLits.size());
00111
00112 solver.assume(~clLits[0]);
00113 solver.propagate();
00114 solver.assume(~clLits[1]);
00115 solver.propagate();
00116 solver.assume(~clLits[2]);
00117 solver.propagate();
00118
00119 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue( clLits[3] ) );
00120 uint32 a = c->activity().activity();
00121 LitVec r;
00122 solver.reason(clLits[3], r);
00123 CPPUNIT_ASSERT_EQUAL(a+1, c->activity().activity());
00124 }
00125
00126 void testSimplifySAT() {
00127 makeLits(3, 2);
00128 ClauseHead* c1 = createShared(ctx, clLits, ClauseInfo());
00129 ctx.add(c1);
00130
00131 ctx.addUnary(~clLits[4]);
00132 ctx.addUnary(clLits[3]);
00133 ctx.master()->propagate();
00134
00135 CPPUNIT_ASSERT_EQUAL(true, c1->simplify(*ctx.master(), false));
00136 }
00137
00138 void testSimplifyUnique() {
00139 makeLits(3, 3);
00140 ClauseHead* c = createShared(ctx, clLits, ClauseInfo());
00141 ctx.add(c);
00142
00143 ctx.addUnary(~clLits[2]);
00144 ctx.addUnary(~clLits[3]);
00145 ctx.master()->propagate();
00146
00147 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*ctx.master(), false));
00148 CPPUNIT_ASSERT(4 == c->size());
00149 CPPUNIT_ASSERT_EQUAL(2, countWatches(*ctx.master(), c, clLits));
00150 }
00151
00152 void testSimplifyShared() {
00153 makeLits(3, 3);
00154 SharedLiterals* sLits = SharedLiterals::newShareable(clLits, Constraint_t::learnt_conflict);
00155 CPPUNIT_ASSERT(sLits->unique() && sLits->type() == Constraint_t::learnt_conflict && sLits->size() == 6);
00156 SharedLiterals* other = sLits->share();
00157 CPPUNIT_ASSERT(!sLits->unique());
00158
00159 ctx.addUnary(~clLits[2]);
00160 ctx.addUnary(~clLits[3]);
00161 ctx.master()->propagate();
00162
00163 CPPUNIT_ASSERT_EQUAL(uint32(4), sLits->simplify(*ctx.master()));
00164 CPPUNIT_ASSERT_EQUAL(uint32(6), sLits->size());
00165 sLits->release();
00166 other->release();
00167 }
00168
00169 void testCloneShared() {
00170 makeLits(3, 2);
00171 ClauseHead* c = createShared(ctx, clLits, ClauseInfo());
00172 ctx.setConcurrency(2);
00173 Solver& solver2 = ctx.addSolver();
00174 ctx.endInit(true);
00175 ClauseHead* clone = (ClauseHead*)c->cloneAttach(solver2);
00176 LitVec lits;
00177 clone->toLits(lits);
00178 CPPUNIT_ASSERT(lits == clLits);
00179 CPPUNIT_ASSERT(countWatches(solver2, clone, clLits) == 2);
00180 c->destroy(ctx.master(), true);
00181
00182 for (uint32 i = 0; i != clLits.size()-1; ++i) {
00183 solver2.assume(~clLits[i]);
00184 solver2.propagate();
00185 }
00186 CPPUNIT_ASSERT(solver2.isTrue(clLits.back()));
00187 CPPUNIT_ASSERT(solver2.reason(clLits.back()) == clone);
00188
00189 clone->destroy(&solver2, true);
00190
00191 }
00192 private:
00193 SharedContext ctx;
00194 LitVec clLits;
00195 Literal a1, a2, a3, b1, b2, b3;
00196 ClauseHead* createShared(SharedContext& ctx, const LitVec& lits, const ClauseInfo& e) {
00197 assert(lits.size() >= 2);
00198 SharedLiterals* shared_lits = SharedLiterals::newShareable(lits, e.type());
00199 return SharedLitsClause::newClause(*ctx.master(), shared_lits, e, &lits[0], false);
00200 }
00201
00202 void simplePropTest(ClauseHead* c) {
00203 Solver& solver = *ctx.master();
00204 solver.add(c);
00205 solver.assume(~clLits[0]);
00206 solver.propagate();
00207 solver.assume( ~clLits.back() );
00208 solver.propagate();
00209 solver.assume(~clLits[1]);
00210 solver.propagate();
00211
00212 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue( clLits[2] ) );
00213 CPPUNIT_ASSERT_EQUAL(true, c->locked(solver));
00214 Antecedent reason = solver.reason(clLits[2]);
00215 CPPUNIT_ASSERT(reason == c);
00216
00217 LitVec r;
00218 reason.reason(solver, clLits[2], r);
00219 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[0]) != r.end());
00220 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[1]) != r.end());
00221 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[3]) != r.end());
00222 }
00223 int countWatches(const Solver& s, ClauseHead* c, const LitVec& lits) {
00224 int w = 0;
00225 for (LitVec::size_type i = 0; i != lits.size(); ++i) {
00226 w += s.hasWatch(~lits[i], c);
00227 }
00228 return w;
00229 }
00230 void check(Solver& solver, ClauseHead* c) {
00231 std::string s = toString(clLits);
00232 std::random_shuffle(clLits.begin(), clLits.end());
00233 CPPUNIT_ASSERT( value_free == solver.value(clLits.back().var()) );
00234 for (LitVec::size_type i = 0; i != clLits.size() - 1; ++i) {
00235 CPPUNIT_ASSERT( value_free == solver.value(clLits[i].var()) );
00236 solver.force(~clLits[i], 0);
00237 solver.propagate();
00238 }
00239 CPPUNIT_ASSERT_EQUAL_MESSAGE(s.c_str(), true, solver.isTrue(clLits.back()));
00240
00241 Antecedent reason = solver.reason(clLits.back());
00242 CPPUNIT_ASSERT(reason == c);
00243 LitVec r;
00244 c->reason(solver, clLits.back(), r);
00245 for (LitVec::size_type i = 0; i != clLits.size() - 1; ++i) {
00246 LitVec::iterator it = std::find(r.begin(), r.end(), ~clLits[i]);
00247 CPPUNIT_ASSERT_MESSAGE(s.c_str(), it != r.end());
00248 r.erase(it);
00249 }
00250 while (!r.empty() && isSentinel(r.back())) r.pop_back();
00251 CPPUNIT_ASSERT(r.empty());
00252 }
00253 std::string toString(const LitVec& c) {
00254 std::string res="[";
00255 for (uint32 i = 0; i != c.size(); ++i) {
00256 if (c[i].sign()) {
00257 res += '~';
00258 }
00259 res += ('a' + i);
00260 res += ' ';
00261 }
00262 res+="]";
00263 return res;
00264 }
00265 void makeLits(int pos, int neg) {
00266 clLits.clear();
00267 int size = pos + neg;
00268 LitVec lit(size);
00269 for (int i = 0; i < pos; ++i) {
00270 lit[i] = posLit(i+1);
00271 clLits.push_back(lit[i]);
00272 }
00273 for (int i = pos; i < pos + neg; ++i) {
00274 lit[i] = negLit(i+1);
00275 clLits.push_back(lit[i]);
00276 }
00277 }
00278 void makeRandomClause(int size) {
00279 int pos = rand() % size + 1;
00280 makeLits( pos, size - pos );
00281 }
00282 };
00283 CPPUNIT_TEST_SUITE_REGISTRATION(SharedClauseTest);
00284 } }