1 //
2 // Copyright (c) 2006-2017 Benjamin Kaufmann
3 //
4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
5 //
6 // Permission is hereby granted, free of charge, to any person obtaining a copy
7 // of this software and associated documentation files (the "Software"), to
8 // deal in the Software without restriction, including without limitation the
9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
10 // sell copies of the Software, and to permit persons to whom the Software is
11 // furnished to do so, subject to the following conditions:
12 //
13 // The above copyright notice and this permission notice shall be included in
14 // all copies or substantial portions of the Software.
15 //
16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
22 // IN THE SOFTWARE.
23 //
24 #include <clasp/weight_constraint.h>
25 #include <clasp/solver.h>
26 #include <algorithm>
27 #include "catch.hpp"
28 using namespace std;
29 
30 namespace Clasp { namespace Test {
newWeightConstraint(SharedContext & ctx,Literal W,WeightLitVec & lits,weight_t bound)31 static bool newWeightConstraint(SharedContext& ctx, Literal W, WeightLitVec& lits, weight_t bound) {
32 	return WeightConstraint::create(*ctx.master(), W, lits, bound).ok();
33 }
newCardinalityConstraint(SharedContext & ctx,const LitVec & lits,int bound)34 static bool newCardinalityConstraint(SharedContext& ctx, const LitVec& lits, int bound) {
35 	REQUIRE(lits.size() >  1);
36 	WeightLitVec wlits;
37 	for (LitVec::size_type i = 1; i < lits.size(); ++i) {
38 		wlits.push_back(WeightLiteral(lits[i], 1));
39 	}
40 	return newWeightConstraint(ctx, lits[0], wlits, bound);
41 }
checkPropagate(Solver & solver,LitVec & assume,const LitVec & expect)42 static bool checkPropagate(Solver& solver, LitVec& assume, const LitVec& expect) {
43 	std::sort(assume.begin(), assume.end());
44 	do {
45 		for (uint32 i = 0; i < assume.size(); ++i) {
46 			REQUIRE(solver.assume(assume[i]));
47 			REQUIRE(solver.propagate());
48 		}
49 		for (uint32 i = 0; i < expect.size(); ++i) {
50 			REQUIRE(solver.isTrue(expect[i]));
51 			LitVec reason;
52 			solver.reason(expect[i], reason);
53 			REQUIRE(assume.size() == reason.size());
54 			for (uint32 j = 0; j < assume.size(); ++j) {
55 				REQUIRE(find(reason.begin(), reason.end(), assume[j]) != reason.end());
56 			}
57 		}
58 		solver.undoUntil(0);
59 	} while (std::next_permutation(assume.begin(), assume.end()));
60 	return true;
61 }
62 TEST_CASE("Cardinality constraints", "[constraint][pb][asp]") {
63 	SharedContext ctx;
64 	Solver& solver = *ctx.master();
65 	Literal body = posLit(ctx.addVar(Var_t::Body));
66 	Literal a = posLit(ctx.addVar(Var_t::Atom));
67 	Literal b = posLit(ctx.addVar(Var_t::Atom));
68 	Literal c = posLit(ctx.addVar(Var_t::Atom));
69 	Literal d = posLit(ctx.addVar(Var_t::Atom));
70 	Literal e = posLit(ctx.addVar(Var_t::Atom));
71 	ctx.startAddConstraints(10);
72 	LitVec lits;
73 	lits.push_back(body);
74 	lits.push_back(a);
75 	lits.push_back(~b);
76 	lits.push_back(~c);
77 	lits.push_back(d);
78 	SECTION("testAssertTriviallySat") {
79 		lits.resize(2);
80 		REQUIRE(newCardinalityConstraint(ctx, lits, 0));
81 		REQUIRE(solver.isTrue(body));
82 		REQUIRE(ctx.numConstraints() == 0);
83 	}
84 	SECTION("testAssertTriviallyUnSat") {
85 		lits.resize(2);
86 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
87 		REQUIRE(solver.isFalse(body));
88 		REQUIRE(ctx.numConstraints() == 0);
89 	}
90 	SECTION("testAssertNotSoTriviallySat") {
91 		solver.force(lits[1], 0);
92 		solver.force(lits[2], 0);
93 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
94 		REQUIRE(solver.isTrue(body));
95 		REQUIRE(ctx.numConstraints() == 0);
96 	}
97 	SECTION("testAssertNotSoTriviallyUnSat") {
98 		solver.force(~lits[1], 0);
99 		solver.force(~lits[3], 0);
100 		REQUIRE(newCardinalityConstraint(ctx, lits, 3));
101 		REQUIRE(solver.isTrue(~body));
102 		REQUIRE(ctx.numConstraints() == 0);
103 	}
104 	SECTION("testTrivialBackpropFalse") {
105 		solver.force(~body, 0);
106 		REQUIRE(newCardinalityConstraint(ctx, lits, 1));
107 		REQUIRE(ctx.numConstraints() == 0);
108 		REQUIRE(solver.isFalse(lits[1]));
109 		REQUIRE(solver.isFalse(lits[2]));
110 		REQUIRE(solver.isFalse(lits[3]));
111 		REQUIRE(solver.isFalse(lits[4]));
112 	}
113 	SECTION("testIntegrateNewVars") {
114 		lits.resize(3);
115 		Literal f = posLit(ctx.addVar(Var_t::Atom));
116 		REQUIRE_FALSE(ctx.master()->validVar(f.var()));
117 		SECTION("body") {
118 			lits[0] = f;
119 		}
120 		SECTION("other") {
121 			lits[2] = f;
122 		}
123 		REQUIRE(newCardinalityConstraint(ctx, lits, 1));
124 		REQUIRE(ctx.master()->validVar(f.var()));
125 	}
126 
127 	SECTION("test propagate") {
128 		LitVec assume, expect;
129 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
130 		SECTION("forwardTrue") {
131 			assume.push_back(a);
132 			assume.push_back(~c);
133 			expect.push_back(body);
134 		}
135 		SECTION("forwardFalse") {
136 			assume.push_back(~a);
137 			assume.push_back(c);
138 			assume.push_back(~d);
139 			expect.push_back(~body);
140 		}
141 		SECTION("backwardTrue") {
142 			assume.push_back(body);
143 			assume.push_back(c);
144 			assume.push_back(~d);
145 			expect.push_back(a);
146 			expect.push_back(~b);
147 		}
148 		SECTION("backwardFalse") {
149 			assume.push_back(~body);
150 			assume.push_back(d);
151 			expect.push_back(~a);
152 			expect.push_back(b);
153 			expect.push_back(c);
154 		}
155 		REQUIRE(checkPropagate(solver, assume, expect));
156 	}
157 	SECTION("test propagate conflict") {
158 		LitVec assume;
159 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
160 		Literal cflLit;
161 		SECTION("forwardTrueConflict") {
162 			assume.push_back(a);
163 			assume.push_back(~c);
164 			cflLit = ~body;
165 		}
166 		SECTION("forwardFalseConflict") {
167 			assume.push_back(~a);
168 			assume.push_back(c);
169 			assume.push_back(~d);
170 			cflLit = body;
171 		}
172 		SECTION("backwardTrueConflict") {
173 			assume.push_back(body);
174 			assume.push_back(c);
175 			assume.push_back(~d);
176 			cflLit = b;
177 		}
178 		SECTION("backwardFalseConflict") {
179 			assume.push_back(~body);
180 			assume.push_back(d);
181 			cflLit = ~b;
182 		}
183 		do {
184 			for (uint32 i = 0; i < assume.size()-1; ++i) {
185 				REQUIRE(solver.assume(assume[i]));
186 				REQUIRE(solver.propagate());
187 			}
188 			REQUIRE(solver.assume(assume.back()));
189 			REQUIRE(solver.force(cflLit, 0));
190 			REQUIRE_FALSE(solver.propagate());
191 			LitVec cfl = solver.conflict();
192 			REQUIRE(assume.size() + 1 == cfl.size());
193 			for (uint32 i = 0; i < assume.size(); ++i) {
194 				REQUIRE(std::find(cfl.begin(), cfl.end(), assume[i]) != cfl.end());
195 			}
196 			REQUIRE(std::find(cfl.begin(), cfl.end(), cflLit) != cfl.end());
197 			solver.undoUntil(0);
198 		} while (std::next_permutation(assume.begin(), assume.end()));
199 	}
200 	SECTION("testReasonBug") {
201 		lits.push_back(~e);
202 		REQUIRE(newCardinalityConstraint(ctx, lits, 3));
203 		LitVec assume, reason;
204 		assume.push_back(a);
205 		assume.push_back(~b);
206 		assume.push_back(~d);
207 		assume.push_back(e);
208 		for (uint32 i = 0; i < assume.size(); ++i) {
209 			REQUIRE(solver.assume(assume[i]));
210 			REQUIRE(solver.propagate());
211 		}
212 		REQUIRE(assume.size() == solver.numAssignedVars());
213 
214 		// B -> ~c because of: ~d, e, B
215 		REQUIRE(solver.assume(body));
216 		REQUIRE(solver.propagate());
217 		REQUIRE(solver.isTrue(~c));
218 		//REQUIRE(con == solver.reason(c.var()).constraint());
219 		solver.reason(~c, reason);
220 		REQUIRE(LitVec::size_type(3) == reason.size());
221 		REQUIRE(std::find(reason.begin(), reason.end(), ~d) != reason.end());
222 		REQUIRE(std::find(reason.begin(), reason.end(), e) != reason.end());
223 		REQUIRE(std::find(reason.begin(), reason.end(), body) != reason.end());
224 		solver.undoUntil(solver.decisionLevel()-1);
225 		reason.clear();
226 
227 		// ~B -> c because of: a, ~b, ~B
228 		REQUIRE(solver.assume(~body));
229 		REQUIRE(solver.propagate());
230 		REQUIRE(solver.isTrue(c));
231 		// REQUIRE(con == solver.reason(c.var()).constraint());
232 		solver.reason(c, reason);
233 		REQUIRE(LitVec::size_type(3) == reason.size());
234 		REQUIRE(std::find(reason.begin(), reason.end(), a) != reason.end());
235 		REQUIRE(std::find(reason.begin(), reason.end(), ~b) != reason.end());
236 		REQUIRE(std::find(reason.begin(), reason.end(), ~body) != reason.end());
237 		solver.undoUntil(solver.decisionLevel()-1);
238 		reason.clear();
239 
240 		// ~c -> B because of: a, ~b, ~c
241 		REQUIRE(solver.assume(~c));
242 		REQUIRE(solver.propagate());
243 		REQUIRE(solver.isTrue(body));
244 		//REQUIRE(con == solver.reason(body.var()).constraint());
245 		solver.reason(body, reason);
246 		REQUIRE(LitVec::size_type(3) == reason.size());
247 		REQUIRE(std::find(reason.begin(), reason.end(), a) != reason.end());
248 		REQUIRE(std::find(reason.begin(), reason.end(), ~b) != reason.end());
249 		REQUIRE(std::find(reason.begin(), reason.end(), ~c) != reason.end());
250 		solver.undoUntil(solver.decisionLevel()-1);
251 
252 		// c -> ~B because of: ~d, e, c
253 		REQUIRE(solver.assume(c));
254 		REQUIRE(solver.propagate());
255 		REQUIRE(solver.isTrue(~body));
256 		//REQUIRE(con == solver.reason(body.var()).constraint());
257 		solver.reason(~body, reason);
258 		REQUIRE(LitVec::size_type(3) == reason.size());
259 		REQUIRE(std::find(reason.begin(), reason.end(), ~d) != reason.end());
260 		REQUIRE(std::find(reason.begin(), reason.end(), e) != reason.end());
261 		REQUIRE(std::find(reason.begin(), reason.end(), c) != reason.end());
262 		solver.undoUntil(solver.decisionLevel()-1);
263 		reason.clear();
264 	}
265 	SECTION("testOrderBug") {
266 		lits.clear();
267 		lits.push_back(body);
268 		lits.push_back(a);
269 		lits.push_back(b);
270 		REQUIRE(newCardinalityConstraint(ctx, lits, 1));
271 		solver.assume(e) && solver.propagate();
272 
273 		solver.force(~a, 0);
274 		solver.force(body, 0);
275 		REQUIRE(solver.propagate());
276 		REQUIRE(solver.isTrue(b));
277 		LitVec reason;
278 		solver.reason(b, reason);
279 		REQUIRE(LitVec::size_type(2) == reason.size());
280 		REQUIRE(std::find(reason.begin(), reason.end(), body) != reason.end());
281 		REQUIRE(std::find(reason.begin(), reason.end(), ~a) != reason.end());
282 	}
283 	SECTION("testBackwardAfterForward") {
284 		lits.clear();
285 		lits.push_back(body);
286 		lits.push_back(a);
287 		lits.push_back(b);
288 		REQUIRE(newCardinalityConstraint(ctx, lits, 1));
289 		solver.assume(a);
290 		REQUIRE(solver.propagate());
291 		REQUIRE(solver.isTrue(body));
292 		LitVec reason;
293 		solver.reason(body, reason);
294 		REQUIRE(LitVec::size_type(1) == reason.size());
295 		REQUIRE(std::find(reason.begin(), reason.end(), a) != reason.end());
296 
297 		solver.assume(~b);
298 		REQUIRE(solver.propagate());
299 		REQUIRE(solver.isTrue(body));
300 	}
301 	SECTION("testSimplify") {
302 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
303 		REQUIRE(solver.simplify());
304 		REQUIRE(1u == ctx.numConstraints());
305 		solver.force(a, 0);
306 		solver.simplify();
307 		REQUIRE(1u == ctx.numConstraints());
308 		solver.force(~c, 0);
309 		solver.simplify();
310 		REQUIRE(0u == ctx.numConstraints());
311 	}
312 
313 	SECTION("testSimplifyCardinality") {
314 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
315 		ctx.addUnary(~a);
316 		ctx.addUnary(~d);
317 		ctx.addUnary(~b);
318 		solver.simplify();
319 		solver.assume(~c);
320 		solver.propagate();
321 		REQUIRE(solver.isTrue(body));
322 		LitVec out;
323 		solver.reason(body, out);
324 		// a, d, and ~b were removed from constraint
325 		REQUIRE((out.size() == 1 && out[0] == ~c));
326 	}
327 	SECTION("testSimplifyWatches") {
328 		REQUIRE(newCardinalityConstraint(ctx, lits, 2));
329 		uint32 nw3 = solver.numWatches(lits[3]) + solver.numWatches(~lits[3]);
330 		solver.pushRoot(body);
331 		REQUIRE(nw3 >= solver.numWatches(lits[3]) + solver.numWatches(~lits[3]));
332 		solver.popRootLevel(1);
333 		REQUIRE(nw3 == solver.numWatches(lits[3]) + solver.numWatches(~lits[3]));
334 	}
335 }
336 TEST_CASE("Weight constraints", "[constraint][pb][asp]") {
337 	SharedContext ctx;
338 	Solver& solver = *ctx.master();
339 	Literal body = posLit(ctx.addVar(Var_t::Body));
340 	Literal a = posLit(ctx.addVar(Var_t::Atom));
341 	Literal b = posLit(ctx.addVar(Var_t::Atom));
342 	Literal c = posLit(ctx.addVar(Var_t::Atom));
343 	Literal d = posLit(ctx.addVar(Var_t::Atom));
344 	Literal e = posLit(ctx.addVar(Var_t::Atom));
345 	Literal f = posLit(ctx.addVar(Var_t::Atom));
346 	ctx.startAddConstraints(10);
347 	WeightLitVec wlits;
348 	wlits.push_back(WeightLiteral(a, 4));
349 	wlits.push_back(WeightLiteral(~b, 2));
350 	wlits.push_back(WeightLiteral(~c, 1));
351 	wlits.push_back(WeightLiteral(d, 1));
352 	SECTION("testAssertWeightTriviallySat") {
353 		wlits.assign(1, WeightLiteral(a, 2));
354 		REQUIRE(newWeightConstraint(ctx, body, wlits, 0));
355 		REQUIRE(solver.isTrue(body));
356 	}
357 	SECTION("testAssertWeightTriviallyUnSat") {
358 		wlits.assign(1, WeightLiteral(a, 2));
359 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
360 		REQUIRE(solver.isFalse(body));
361 	}
362 	SECTION("testAssertWeightNotSoTriviallySat") {
363 		solver.force(wlits[1].first, 0);
364 		REQUIRE(newWeightConstraint(ctx, body, wlits, 2));
365 		REQUIRE(solver.isTrue(body));
366 	}
367 	SECTION("testAssertWeightNotSoTriviallyUnSat") {
368 		solver.force(~wlits[0].first, 0);
369 		solver.force(~wlits[2].first, 0);
370 		REQUIRE(newWeightConstraint(ctx, body, wlits, 4));
371 		REQUIRE(solver.isTrue(~body));
372 	}
373 	SECTION("testTrivialBackpropTrue") {
374 		solver.force(body, 0);
375 		REQUIRE(newWeightConstraint(ctx, body, wlits, 7));
376 		REQUIRE(ctx.numConstraints() == 1);
377 		REQUIRE(solver.isTrue(a));
378 		REQUIRE(solver.isTrue(~b));
379 		solver.propagate();
380 		solver.assume(~wlits[0].first) && solver.propagate();
381 		REQUIRE(solver.isTrue(wlits[1].first));
382 	}
383 	SECTION("testTrivialBackpropFalseWeight") {
384 		solver.force(~body, 0);
385 		REQUIRE(newWeightConstraint(ctx, body, wlits, 2));
386 		REQUIRE(ctx.numConstraints() == 1);
387 		REQUIRE(solver.isFalse(a));
388 		REQUIRE(solver.isFalse(~b));
389 	}
390 	SECTION("testWeightReasonAfterBackprop") {
391 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
392 		solver.assume(~body) && solver.propagate();
393 		REQUIRE(solver.isTrue(~a));
394 		solver.assume(d) && solver.propagate();
395 		REQUIRE(solver.isTrue(b));
396 		LitVec r;
397 		solver.reason(~a, r);
398 		REQUIRE((r.size() == 1 && r[0] == ~body));
399 		solver.reason(b, r);
400 		REQUIRE((r.size() == 2 && r[0] == ~body && r[1] == d));
401 		solver.undoUntil(solver.decisionLevel()-1);
402 		solver.reason(~a, r);
403 		REQUIRE((r.size() == 1 && r[0] == ~body));
404 		solver.undoUntil(solver.decisionLevel()-1);
405 	}
406 
407 	SECTION("testOnlyBTB") {
408 		ctx.setConcurrency(2);
409 		wlits.clear();
410 		wlits.push_back(WeightLiteral(a, 1));
411 		wlits.push_back(WeightLiteral(b, 1));
412 		wlits.push_back(WeightLiteral(c, 1));
413 		wlits.push_back(WeightLiteral(d, 1));
414 		WeightConstraint::CPair res = WeightConstraint::create(solver, body, wlits, 2, WeightConstraint::create_only_btb);
415 		REQUIRE(res.first());
416 		ctx.endInit(true);
417 		for (int i = 0; i != 2; ++i) {
418 			INFO("Solver " << i);
419 			Solver* s = ctx.solver(i);
420 			Constraint* con = s->constraints()[0];
421 			CHECK(dynamic_cast<WeightConstraint*>(con));
422 			CHECK(s->hasWatch(body, con));
423 			CHECK_FALSE(s->hasWatch(~body, con));
424 			for (WeightLitVec::const_iterator it = wlits.begin(), end = wlits.end(); it != end; ++it) {
425 				CHECK_FALSE(s->hasWatch(it->first, con));
426 				CHECK(s->hasWatch(~it->first, con));
427 			}
428 
429 			s->assume(a) && s->propagate();
430 			s->assume(b) && s->propagate();
431 			// FTB_BFB not added
432 			CHECK(s->value(body.var()) == value_free);
433 			s->undoUntil(0);
434 			s->assume(~a) && s->propagate();
435 			s->assume(~b) && s->propagate();
436 			uint32 dl = s->decisionLevel();
437 			s->assume(body) && s->propagate();
438 			CHECK((s->isTrue(c) && s->isTrue(d)));
439 			s->undoUntil(dl);
440 			s->assume(~c) && s->propagate();
441 			CHECK(s->isFalse(body));
442 		}
443 	}
444 	SECTION("testOnlyBFB") {
445 		ctx.setConcurrency(2);
446 		wlits.clear();
447 		wlits.push_back(WeightLiteral(a, 1));
448 		wlits.push_back(WeightLiteral(b, 1));
449 		wlits.push_back(WeightLiteral(c, 1));
450 		wlits.push_back(WeightLiteral(d, 1));
451 		WeightConstraint::CPair res = WeightConstraint::create(solver, body, wlits, 2, WeightConstraint::create_only_bfb);
452 		REQUIRE(res.first());
453 		ctx.endInit(true);
454 		for (int i = 0; i != 2; ++i) {
455 			INFO("Solver " << i);
456 			Solver* s = ctx.solver(i);
457 			Constraint* con = s->constraints()[0];
458 			CHECK(dynamic_cast<WeightConstraint*>(con));
459 			CHECK_FALSE(s->hasWatch(body, con));
460 			CHECK(s->hasWatch(~body, con));
461 			for (WeightLitVec::const_iterator it = wlits.begin(), end = wlits.end(); it != end; ++it) {
462 				CHECK(s->hasWatch(it->first, con));
463 				CHECK_FALSE(s->hasWatch(~it->first, con));
464 			}
465 			s->assume(a) && s->propagate();
466 			uint32 dl = s->decisionLevel();
467 			s->assume(b) && s->propagate();
468 			CHECK(s->isTrue(body));
469 			s->undoUntil(dl);
470 			s->assume(~body) && s->propagate();
471 			CHECK((s->isFalse(b) && s->isFalse(c) && s->isFalse(d)));
472 			s->undoUntil(0);
473 			s->assume(~a) && s->propagate();
474 			s->assume(~b) && s->propagate();
475 			s->assume(~b) && s->propagate();
476 			CHECK(s->value(body.var()) == value_free);
477 		}
478 	}
479 
480 	SECTION("testSimplifyWeight") {
481 		wlits[2].second = 2;
482 		wlits.push_back(WeightLiteral(e, 1));
483 		wlits.push_back(WeightLiteral(f, 1));
484 		REQUIRE(newWeightConstraint(ctx, body, wlits, 2));
485 		ctx.addUnary(body);
486 		ctx.addUnary(~a);
487 		ctx.addUnary(~d);
488 		ctx.addUnary(~e);
489 		ctx.addUnary(~f);
490 		solver.simplify();
491 		REQUIRE(solver.value(b.var()) == value_free);
492 		solver.assume(c);
493 		solver.propagate();
494 		REQUIRE(solver.isTrue(~b));
495 		LitVec out;
496 		solver.reason(~b, out);
497 		REQUIRE((out.size() == 1 && out[0] == c));
498 	}
499 
500 	SECTION("test propagate") {
501 		LitVec assume, expect;
502 		SECTION("weight forward true") {
503 			expect.push_back(body);
504 			SECTION("with max weight") {
505 				assume.push_back(a);
506 			}
507 			SECTION("with med weight") {
508 				assume.push_back(~b);
509 				assume.push_back(~c);
510 			}
511 			SECTION("with min weight") {
512 				assume.push_back(~b);
513 				assume.push_back(d);
514 			}
515 		}
516 		SECTION("weight forward false") {
517 			assume.push_back(~a);
518 			assume.push_back(b);
519 			expect.push_back(~body);
520 		}
521 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
522 		REQUIRE(checkPropagate(solver, assume, expect));
523 	}
524 
525 	SECTION("testWeightBackwardTrue") {
526 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
527 		solver.assume(~a);
528 		solver.force(body, 0);
529 		REQUIRE(solver.propagate());
530 		REQUIRE(solver.isTrue(~b));
531 		REQUIRE(value_free == solver.value(c.var()));
532 		LitVec r;
533 		solver.reason(~b, r);
534 		REQUIRE(r.size() == 2);
535 		REQUIRE(std::find(r.begin(), r.end(), ~a) != r.end());
536 		REQUIRE(std::find(r.begin(), r.end(), body) != r.end());
537 
538 		solver.assume(~d);
539 		REQUIRE(solver.propagate());
540 		REQUIRE(solver.isTrue(~c));
541 
542 		solver.reason(~c, r);
543 		REQUIRE(r.size() == 3);
544 		REQUIRE(std::find(r.begin(), r.end(), ~a) != r.end());
545 		REQUIRE(std::find(r.begin(), r.end(), body) != r.end());
546 		REQUIRE(std::find(r.begin(), r.end(), ~d) != r.end());
547 
548 		solver.undoUntil(solver.decisionLevel()-1);
549 		solver.reason(~b, r);
550 		REQUIRE(r.size() == 2);
551 		REQUIRE(std::find(r.begin(), r.end(), ~a) != r.end());
552 		REQUIRE(std::find(r.begin(), r.end(), body) != r.end());
553 	}
554 
555 	SECTION("testWeightBackwardFalse") {
556 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
557 		solver.assume(~body);
558 		REQUIRE(solver.propagate());
559 		REQUIRE(solver.isTrue(~a));
560 		LitVec r;
561 		solver.reason(~a, r);
562 		REQUIRE(r.size() == 1);
563 		REQUIRE(std::find(r.begin(), r.end(), ~body) != r.end());
564 
565 		solver.force(~b, 0);
566 		REQUIRE(solver.propagate());
567 		REQUIRE(solver.isTrue(c));
568 		REQUIRE(solver.isTrue(~d));
569 
570 		LitVec r2;
571 		solver.reason(c, r);
572 		solver.reason(~d, r2);
573 		REQUIRE(r == r2);
574 		REQUIRE(r.size() == 2);
575 		REQUIRE(std::find(r.begin(), r.end(), ~body) != r.end());
576 		REQUIRE(std::find(r.begin(), r.end(), ~b) != r.end());
577 	}
578 
579 	SECTION("testWeightConflict") {
580 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
581 		LitVec assume;
582 		assume.push_back(body);
583 		assume.push_back(~a);
584 		assume.push_back(b);
585 		std::sort(assume.begin(), assume.end());
586 		do {
587 			REQUIRE(solver.assume(assume[0]));
588 			for (uint32 i = 1; i < assume.size(); ++i) {
589 				REQUIRE(solver.force(assume[i],0));
590 			}
591 			REQUIRE_FALSE(solver.propagate());
592 			solver.undoUntil(0);
593 		} while (std::next_permutation(assume.begin(), assume.end()));
594 	}
595 
596 	SECTION("testCloneWeight") {
597 		ctx.setConcurrency(2);
598 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
599 		solver.force(~a, 0);
600 		Solver& solver2 = ctx.pushSolver();
601 		ctx.endInit(true);
602 
603 		REQUIRE(solver2.numConstraints() == 1);
604 
605 		REQUIRE((solver2.numWatches(a) == 0 && solver2.numWatches(~a) == 0));
606 		solver2.assume(body);
607 		solver2.propagate();
608 		solver2.assume(~d);
609 		solver2.propagate();
610 		REQUIRE(solver2.isTrue(~b));
611 		REQUIRE(solver2.isTrue(~c));
612 		LitVec out;
613 		solver2.reason(~b, out);
614 		REQUIRE(std::find(out.begin(), out.end(), body) != out.end());
615 		REQUIRE(std::find(out.begin(), out.end(), ~a) != out.end());
616 		REQUIRE(std::find(out.begin(), out.end(), ~d) == out.end());
617 		out.clear();
618 		solver2.reason(~c, out);
619 		REQUIRE(std::find(out.begin(), out.end(), ~d) != out.end());
620 	}
621 
622 	SECTION("testCloneWeightShared") {
623 		ctx.setConcurrency(2);
624 		ctx.setShareMode(ContextParams::share_problem);
625 		REQUIRE(newWeightConstraint(ctx, body, wlits, 3));
626 		solver.force(~a, 0);
627 		Solver& solver2 = ctx.pushSolver();
628 		ctx.endInit(true);
629 
630 		REQUIRE(solver2.numConstraints() == 1);
631 
632 		REQUIRE((solver2.numWatches(a) == 0 && solver2.numWatches(~a) == 0));
633 		solver2.assume(body);
634 		solver2.propagate();
635 		solver2.assume(~d);
636 		solver2.propagate();
637 		REQUIRE(solver2.isTrue(~b));
638 		REQUIRE(solver2.isTrue(~c));
639 		LitVec out;
640 		solver2.reason(~b, out);
641 		REQUIRE(std::find(out.begin(), out.end(), body) != out.end());
642 		REQUIRE(std::find(out.begin(), out.end(), ~a) != out.end());
643 		REQUIRE(std::find(out.begin(), out.end(), ~d) == out.end());
644 		out.clear();
645 		solver2.reason(~c, out);
646 		REQUIRE(std::find(out.begin(), out.end(), ~d) != out.end());
647 	}
648 
649 	SECTION("testAddOnLevel") {
650 		ctx.endInit(true);
651 		uint32 sz = sizeVec(wlits) + 1;
652 		Solver& s = *ctx.master();
653 		s.pushRoot(f);
654 		WeightConstraint::CPair res = WeightConstraint::create(s, body, wlits, 2, WeightConstraint::create_no_add);
655 		REQUIRE((res.ok() && res.first() != 0));
656 		REQUIRE((res.first()->size() == sz && wlits.size() == sz-1));
657 		s.force(body);
658 		s.force(~wlits[0].first);
659 		s.force(~wlits[1].first,0);
660 		s.propagate();
661 		REQUIRE((s.isTrue(wlits[2].first) && s.isTrue(wlits[3].first)));
662 		res.first()->destroy(&s, true);
663 	}
664 	SECTION("testAddPBOnLevel") {
665 		ctx.endInit(true);
666 		Solver& s = *ctx.master();
667 		s.pushRoot(f);
668 		WeightConstraint* wc = WeightConstraint::create(s, lit_true(), wlits, 2, WeightConstraint::create_no_add).first();
669 		wc->destroy(&s, true);
670 		REQUIRE_FALSE(s.removeUndoWatch(s.decisionLevel(), wc));
671 	}
672 	SECTION("testIntegrateRoot") {
673 		ctx.endInit(true);
674 		Solver& s = *ctx.master();
675 		s.pushRoot(~c);
676 		s.pushRoot(d);
677 		WeightConstraint* wc = WeightConstraint::create(s, body, wlits, 3, WeightConstraint::create_no_add).first();
678 		REQUIRE(s.removeUndoWatch(2, wc));
679 		REQUIRE(s.removeUndoWatch(1, wc));
680 		wc->destroy(&s, true);
681 	}
682 	SECTION("testCreateSat") {
683 		ctx.endInit(true);
684 		Solver& s = *ctx.master();
685 
686 		s.force(wlits[0].first);
687 		s.force(wlits[1].first);
688 		WeightConstraint::CPair res = WeightConstraint::create(s, body, wlits, 2, WeightConstraint::create_no_add|WeightConstraint::create_sat);
689 		REQUIRE((res.ok() && res.first() != 0));
690 		REQUIRE(s.isTrue(body));
691 		s.propagate();
692 		REQUIRE(s.isTrue(body));
693 		while (!wlits.empty()) {
694 			REQUIRE((s.force(~wlits.back().first) && s.propagate()));
695 			wlits.pop_back();
696 		}
697 		res.first()->destroy(&s, true);
698 	}
699 	SECTION("testCreateSatOnRoot") {
700 		ctx.endInit(true);
701 		Solver& s = *ctx.master();
702 		s.pushRoot(f);
703 		REQUIRE(s.rootLevel() == 1);
704 		s.force(a, 0);
705 		s.force(b, 0);
706 		s.propagate();
707 		wlits.clear();
708 		wlits.push_back(WeightLiteral(a, 1));
709 		wlits.push_back(WeightLiteral(b, 1));
710 		wlits.push_back(WeightLiteral(c, 1));
711 		wlits.push_back(WeightLiteral(d, 1));
712 		WeightLitsRep rep           = WeightLitsRep::create(s, wlits, 2);
713 		WeightConstraint::CPair res = WeightConstraint::create(s, body, rep, WeightConstraint::create_no_add|WeightConstraint::create_sat);
714 		REQUIRE((res.ok() && res.first()));
715 		REQUIRE(s.isTrue(body));
716 		REQUIRE(s.reason(body) == res.first());
717 		s.popRootLevel(1);
718 		REQUIRE(s.value(body.var()) == value_free);
719 		res.first()->destroy(&s, true);
720 	}
721 	SECTION("testCreateSatOnRootNoProp") {
722 		ctx.endInit(true);
723 		Solver& s = *ctx.master();
724 		s.pushRoot(f);
725 		REQUIRE(s.rootLevel() == 1);
726 		s.force(a, 0);
727 		s.force(b, 0);
728 		wlits.clear();
729 		wlits.push_back(WeightLiteral(a, 1));
730 		wlits.push_back(WeightLiteral(b, 1));
731 		wlits.push_back(WeightLiteral(c, 1));
732 		wlits.push_back(WeightLiteral(d, 1));
733 		WeightLitsRep rep           = WeightLitsRep::create(s, wlits, 2);
734 		WeightConstraint::CPair res = WeightConstraint::create(s, body, rep, WeightConstraint::create_no_add|WeightConstraint::create_sat);
735 		REQUIRE((res.ok() && res.first()));
736 		REQUIRE(!s.isTrue(body));
737 		REQUIRE(s.propagate());
738 		REQUIRE(s.isTrue(body));
739 		REQUIRE(s.reason(body) == res.first());
740 		s.popRootLevel(1);
741 		REQUIRE(s.value(body.var()) == value_free);
742 		res.first()->destroy(&s, true);
743 	}
744 	SECTION("testMergeNegativeWeight") {
745 		wlits.clear();
746 		wlits.push_back(WeightLiteral(a, -1));
747 		wlits.push_back(WeightLiteral(a, -1));
748 		wlits.push_back(WeightLiteral(b, -2));
749 		WeightLitsRep rep = WeightLitsRep::create(*ctx.master(), wlits, -2);
750 		REQUIRE(rep.size == 2);
751 		REQUIRE(rep.bound == 1);
752 		REQUIRE(rep.reach == 2);
753 		REQUIRE(rep.lits[0].second == 1);
754 		REQUIRE(rep.lits[1].second == 1);
755 	}
756 }
757 } }
758