diff --git a/test/int/arithmetic.cpp b/test/int/arithmetic.cpp index 0105cf41f7..a4d8326c9c 100644 --- a/test/int/arithmetic.cpp +++ b/test/int/arithmetic.cpp @@ -494,6 +494,7 @@ namespace Test { namespace Int { }; /// Known identities at the integer limits, independent of the oracles. + // Observe rewriting after the modulus changes at an initial fixpoint. class NumberTheoryLimits : public ::Test::Base { class TestSpace : public Gecode::Space { public: @@ -505,33 +506,6 @@ namespace Test { namespace Int { virtual bool run(void) { using namespace Gecode; const int hi=Gecode::Int::Limits::max; - const int lo=Gecode::Int::Limits::min; - const int cases[][4] = { - {lo,hi,hi,1}, {hi,lo,hi,1}, {lo,0,hi,1}, - {0,lo,hi,0}, {0,0,0,1}, {lo,1,1,0} - }; - for (const auto& c : cases) { - TestSpace home; - IntVar x(home,c[0],c[0]); - IntVar y(home,c[1],c[1]); - IntVar g(home,0,hi); - BoolVar b(home,0,1); - BoolVar correct(home,0,1); - BoolVar wrong(home,0,1); - gcd(home,x,y,g); - divides(home,x,y,Reify(b)); - IntVar expected(home,c[2],c[2]); - IntVar other(home,c[2] == 0 ? 1 : 0,c[2] == 0 ? 1 : 0); - gcd(home,x,y,expected,Reify(correct)); - gcd(home,x,y,other,Reify(wrong)); - if ((home.status() == SS_FAILED) || !g.assigned() || - (g.val() != c[2]) || !b.assigned() || (b.val() != c[3]) || - !correct.assigned() || (correct.val() != 1) || - !wrong.assigned() || (wrong.val() != 0)) - return arithmetic_failed - ("signed GCD and divisibility: x, y, g, expected, other", - Gecode::IntVarArgs() << x << y << g << expected << other); - } // hi-1 is -1 modulo hi. Its square is 1 and its cube is -1; // negating one factor reverses these residues. The cube exceeds // signed 64-bit range, but its residue remains exactly known. @@ -559,29 +533,58 @@ namespace Test { namespace Int { ("large product residue: x, m, y", Gecode::IntVarArgs() << x << m << y); } - for (ReifyMode rm : {RM_EQV,RM_IMP,RM_PMI}) - for (int truth=0; truth<=1; truth++) - for (int control=0; control<=1; control++) { - TestSpace home; - IntVarArgs x(home,n,hi-1,hi-1); - if (negative) x[0]=IntVar(home,1-hi,1-hi); - IntVar m(home,hi,hi); - IntVar y(home,truth ? expected : 0,truth ? expected : 0); - BoolVar b(home,control,control); - if (variable) product_mod(home,x,m,y,Reify(b,rm)); - else product_mod(home,x,hi,y,Reify(b,rm)); - const bool holds=(rm == RM_EQV) ? (control == truth) : - ((rm == RM_IMP) ? (!control || truth) : (!truth || control)); - if ((home.status() != SS_FAILED) != holds) - return arithmetic_failed - ("large product reification: x, m, y", - Gecode::IntVarArgs() << x << m << y); - } } return true; } }; + /// Known modular residues whose unreduced product exceeds 64 bits. + class ProductModLimits : public Test { + int n; + bool negative; + bool variable; + public: + ProductModLimits(int n0, bool neg, bool var) + : Test("Arithmetic::ProductMod::Limits::"+str(n0)+"::"+ + str(neg)+"::"+str(var),1, + Gecode::IntSet({0,1,Gecode::Int::Limits::max-1}),true), + n(n0), negative(neg), variable(var) { + // Reified modular products do not promise a propagation fixpoint. + testfix = false; + } + virtual bool solution(const Assignment& x) const { + return x[0] == (((n+negative)%2 == 0) ? + 1 : Gecode::Int::Limits::max-1); + } + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) { + using namespace Gecode; + const int hi = Gecode::Int::Limits::max; + IntVarArgs factors(home,n,hi-1,hi-1); + if (negative) + factors[0] = IntVar(home,1-hi,1-hi); + if (variable) { + IntVar modulus(home,hi,hi); + product_mod(home,factors,modulus,x[0]); + } else { + product_mod(home,factors,hi,x[0]); + } + } + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x, + Gecode::Reify r) { + using namespace Gecode; + const int hi = Gecode::Int::Limits::max; + IntVarArgs factors(home,n,hi-1,hi-1); + if (negative) + factors[0] = IntVar(home,1-hi,1-hi); + if (variable) { + IntVar modulus(home,hi,hi); + product_mod(home,factors,modulus,x[0],r); + } else { + product_mod(home,factors,hi,x[0],r); + } + } + }; + /// Evaluate an exact product for testing without overflowing. bool product_value(const Assignment& x, int n, int& product) { for (int i=0; i(n)) - return false; - for (int i=0; istatus() == SS_FAILED; - delete home; - return failed; - } - }; - /// Test the bin-packing propagation levels class PropagationLevels : public Base { protected: @@ -386,59 +355,26 @@ namespace Test { namespace Int { } }; - /// Test DFF arithmetic at the largest supported integer value - class DFFLargeWeights : public Base { - protected: - /// Simple test space class - class TestSpace : public Gecode::Space { - public: - /// Constructor - TestSpace(void) {} - /// Copy function - virtual Gecode::Space* copy(void) { - return nullptr; - } - }; + /// Large weights must preserve every feasible bin assignment. + class DFFLargeWeights : public Test { + int capacity; + int weight; public: - /// Constructor - DFFLargeWeights(void) - : Base("Int::BinPacking::DFFLargeWeights") {} - /// Run the actual test - virtual bool run(void) { - using namespace Gecode; - { - TestSpace* home = new TestSpace; - IntVarArgs l(*home, 2, 0, Gecode::Int::Limits::max); - IntVarArgs b(*home, 1, 0, 1); - IntArgs s({Gecode::Int::Limits::max}); - binpacking(*home, l, b, s); - bool failed = home->status() == SS_FAILED; - delete home; - if (failed) - return false; - } - { - TestSpace* home = new TestSpace; - int c = Gecode::Int::Limits::max / 2; - IntVarArgs l(*home, 2, 0, c); - IntVarArgs b(*home, 1, 0, 1); - IntArgs s({c}); - binpacking(*home, l, b, s); - bool failed = home->status() == SS_FAILED; - delete home; - if (failed) - return false; - } - { - TestSpace* home = new TestSpace; - IntVarArgs l(*home, 2, 0, 1100000000); - IntVarArgs b(*home, 2, 0, 1); - IntArgs s({1000000000,1000000000}); - binpacking(*home, l, b, s); - bool failed = home->status() == SS_FAILED; - delete home; - return !failed; - } + DFFLargeWeights(int n, int c, int w) + : Test("BinPacking::DFFLargeWeights::"+str(n)+"::"+str(w), + n,0,1), capacity(c), weight(w) {} + virtual bool solution(const Assignment& x) const { + long long loads[2] = {0,0}; + for (int i=0; i -#include #include -#include -#include namespace Test { namespace Int { @@ -497,124 +494,46 @@ namespace Test { namespace Int { } }; - /// Focused test for bounded knapsack-augmented overload checking - class KnapsackAugmentedOverload : public Test::Base { - private: - struct Task { - int e; - int l; - int p; - int d; - int est(void) const { return e; } - int lst(void) const { return l; } - int ect(void) const { return e+p; } - int lct(void) const { return l+p; } - int c(void) const { return d; } - }; - - static int scalar_available(const std::vector& demands, - int capacity) { - std::vector reachable(static_cast(capacity+1), - false); - reachable[0] = true; - for (int demand : demands) - for (int value=capacity; value>=demand; value--) - reachable[static_cast(value)] = - reachable[static_cast(value)] || - reachable[static_cast(value-demand)]; - for (int value=capacity; value>=0; value--) - if (reachable[static_cast(value)]) - return value; - return 0; + /// Fixed-end tasks must accept exactly the capacity-feasible schedules + class ManFixECumulative : public Test { + public: + ManFixECumulative(void) + : Test("Cumulative::Man::FixE",4, + Gecode::IntSet({0,9,19,29,39}),false,Gecode::IPL_ADVANCED) { + testfix = false; + contest = CTL_NONE; } - - static bool scalar_conflict(const std::vector& tasks, - int capacity) { - std::vector order(tasks.size()); - std::vector times; - for (std::size_t i=0; i(i); - times.push_back(tasks[i].est()); - times.push_back(tasks[i].ect()); - times.push_back(tasks[i].lst()); - times.push_back(tasks[i].lct()); - } - std::sort(order.begin(),order.end(),[&](int a, int b) { - return std::make_pair(tasks[static_cast(a)].lct(),a) < - std::make_pair(tasks[static_cast(b)].lct(),b); - }); - std::sort(times.begin(),times.end()); - times.erase(std::unique(times.begin(),times.end()),times.end()); - int earliest = tasks[static_cast(order[0])].est(); - std::vector prefix; - for (int index : order) { - prefix.push_back(index); - earliest = (std::min)(earliest, - tasks[static_cast(index)].est()); - const int finish = tasks[static_cast(index)].lct(); - long long overflow = 0; - for (std::size_t point=0; point+1= finish)) - continue; - int fixed = 0; - int required = 0; - std::vector free; - for (const Task& task : tasks) - if ((task.lst() <= left) && (left < task.ect())) - fixed += task.c(); - if (fixed > capacity) - return true; - for (int member : prefix) { - const Task& task = tasks[static_cast(member)]; - const bool compulsory = - (task.lst() <= left) && (left < task.ect()); - if ((task.est() <= left) && (left < task.lct()) && !compulsory) - free.push_back(task.c()); - if ((task.est() <= left) && - (left < (std::min)(task.ect(),task.lst()))) - required += task.c(); - } - const int right = (std::min)(times[point+1],finish); - overflow = (std::max)(0LL,overflow+ - static_cast(right-left) * - (required-scalar_available(free,capacity-fixed))); - } - if (overflow > 0) - return true; + virtual bool solution(const Assignment& x) const { + for (int i=0; i<4; i++) + if (x[i] >= 10*(i+1)) + return false; + for (int t=0; t<40; t++) { + int used = 0; + for (int i=0; i<4; i++) + if ((x[i] <= t) && (t < 10*(i+1))) + used += 2; + if (used > 4) + return false; } - return false; - } - - static bool reference_parity(void) { - std::vector shapes; - for (int est=0; est<=1; est++) - for (int lst=est; lst<=2; lst++) - for (int duration=1; duration<=2; duration++) - for (int demand=1; demand<=3; demand++) - shapes.push_back({est,lst,duration,demand}); - for (std::size_t a=0; a tasks = - {shapes[a],shapes[b],shapes[c],shapes[d]}; - for (int capacity=2; capacity<=3; capacity++) { - bool supported = true; - bool non_unit = false; - for (const Task& task : tasks) { - supported = supported && (task.c() <= capacity); - non_unit = non_unit || (task.c() != 1); - } - if (supported && non_unit && - (Gecode::Int::Cumulative::Kaoc::conflict( - tasks,capacity) != scalar_conflict(tasks,capacity))) - return false; - } - } return true; } + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) { + Gecode::IntArgs ends({10,20,30,40}); + Gecode::TaskTypeArgs types(4); + for (int i=0; i<4; i++) { + Gecode::dom(home,x[i],0,ends[i]-1); + types[i] = Gecode::TT_FIXE; + } + Gecode::cumulative(home,4,types,x,ends, + Gecode::IntArgs({2,2,2,2}),ipl); + } + }; + ManFixECumulative manFixECumulative; + /// Check overload detection before search, including capacity wakeups + // Complete assignments cannot distinguish basic from advanced propagation. + class KnapsackAugmentedOverload : public Test::Base { + private: class Fixture : public Gecode::Space { public: Gecode::IntVarArray starts; @@ -672,78 +591,7 @@ namespace Test { namespace Int { return clone->status() == Gecode::SS_FAILED; } - static bool fixed_end_feasible(void) { - class FixedEndFixture : public Gecode::Space { - public: - Gecode::IntVarArray starts; - FixedEndFixture(void) : starts(*this,4) { - Gecode::IntArgs ends({10,20,30,40}); - Gecode::TaskTypeArgs types(4); - for (int i=0; i<4; i++) { - starts[i] = Gecode::IntVar(*this,0,ends[i]-1); - types[i] = Gecode::TT_FIXE; - } - Gecode::cumulative(*this,4,types,starts,ends, - Gecode::IntArgs({2,2,2,2}),Gecode::IPL_ADVANCED); - } - FixedEndFixture(FixedEndFixture& fixture) : Gecode::Space(fixture) { - starts.update(*this,fixture.starts); - } - virtual Gecode::Space* copy(void) { - return new FixedEndFixture(*this); - } - }; - - FixedEndFixture fixture; - if (fixture.status() == Gecode::SS_FAILED) - return false; - // Each task can run for one unit immediately before its fixed end. - for (int i=0; i<4; i++) - Gecode::rel(fixture,fixture.starts[i],Gecode::IRT_EQ,10*(i+1)-1); - return fixture.status() != Gecode::SS_FAILED; - } - - static bool bit_boundaries(void) { - using Gecode::Int::Cumulative::Kaoc::Bits; - using Gecode::Int::Cumulative::Kaoc::add; - using Gecode::Int::Cumulative::Kaoc::max_reachable; - const int capacities[] = {63,64,65,127}; - for (int capacity : capacities) { - for (int first=1; first<=capacity; first+=7) { - Bits bits = {1ULL,0ULL}; - std::vector demands; - for (int demand=first; demand<=capacity; demand+=13) { - add(bits,demand,capacity); - demands.push_back(demand); - for (int residual=0; residual<=capacity; residual++) - if (max_reachable(bits,residual) != - scalar_available(demands,residual)) - return false; - } - } - } - Bits gap = {1ULL,0ULL}; - add(gap,4,9); - add(gap,6,9); - return max_reachable(gap,9) == 6; - } - - static bool gates_and_optional_subset(void) { - std::vector all_unit(4,Task{0,1,1,1}); - std::vector parity(4,Task{0,5,2,2}); - std::vector too_few(3,Task{0,1,1,2}); - std::vector too_many(65,Task{0,1,1,2}); - std::vector bad_demand(4,Task{0,1,1,1}); - bad_demand[0].d = 4; - if (Gecode::Int::Cumulative::Kaoc::conflict(all_unit,3) || - !Gecode::Int::Cumulative::Kaoc::conflict(parity,3) || - Gecode::Int::Cumulative::Kaoc::conflict(parity,1) || - Gecode::Int::Cumulative::Kaoc::conflict(parity,128) || - Gecode::Int::Cumulative::Kaoc::conflict(too_few,3) || - Gecode::Int::Cumulative::Kaoc::conflict(too_many,3) || - Gecode::Int::Cumulative::Kaoc::conflict(bad_demand,3)) - return false; - + static bool optional_subset(void) { class OptionalSubsetFixture : public Gecode::Space { public: OptionalSubsetFixture(Gecode::IntPropLevel level) { @@ -790,23 +638,9 @@ namespace Test { namespace Int { virtual bool run(void) { Fixture basic(Gecode::IPL_BASIC); Fixture advanced(Gecode::IPL_ADVANCED); - const bool boundaries = bit_boundaries(); - const bool parity = reference_parity(); - const bool variable = variable_capacity_rechecks(); - const bool fixed_end = fixed_end_feasible(); - const bool gates = gates_and_optional_subset(); - const bool basic_ok = basic.status() != Gecode::SS_FAILED; - const bool advanced_ok = advanced.status() == Gecode::SS_FAILED; - if (!(boundaries && parity && variable && fixed_end && gates && - basic_ok && advanced_ok)) - std::cerr << "kaoc boundaries=" << boundaries - << " parity=" << parity << " variable=" << variable - << " fixed_end=" << fixed_end - << " gates=" << gates - << " basic=" << basic_ok - << " advanced=" << advanced_ok << "\n"; - return boundaries && parity && variable && fixed_end && gates && - basic_ok && advanced_ok; + return (basic.status() != Gecode::SS_FAILED) && + (advanced.status() == Gecode::SS_FAILED) && + variable_capacity_rechecks() && optional_subset(); } }; diff --git a/test/int/extensional.cpp b/test/int/extensional.cpp index 5de3aa3d86..be05c3b53b 100755 --- a/test/int/extensional.cpp +++ b/test/int/extensional.cpp @@ -888,8 +888,9 @@ namespace Test { namespace Int { /// Create and register test TupleSetTest(const std::string& s, bool p, Gecode::IntSet d0, Gecode::TupleSet ts0, bool td, - Gecode::ExtensionalPropKind epk0) - : Test(TestTags::sweep(), + Gecode::ExtensionalPropKind epk0, + TestTags tags=TestTags::sweep()) + : Test(tags, "Extensional::TupleSet::" + extensional_kind_name(epk0) + "::" + str(p) + "::" + s, ts0.arity(),d0,true,Gecode::IPL_DOM), @@ -943,383 +944,126 @@ namespace Test { namespace Int { } }; - /// Sparse smoke test for very low-density unary tuple sets - class SparseTupleSetUnary : public ::Test::Base { - public: - SparseTupleSetUnary(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::Unary") {} - - virtual bool run(void) { - using namespace Gecode; - - const int n = 2000; - TupleSet ts(1); - for (int i=0; i e(root); - delete root; - - SparseUnarySpace* sol = e.next(); - if (sol == nullptr) - return false; - const bool ok = sol->x[0].assigned() && (sol->x[0].val() == 0); - delete sol; - return ok; } - }; - - /// Sparse smoke test for low-density ternary tuple sets - class SparseTupleSetTernary : public ::Test::Base { public: - SparseTupleSetTernary(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::Ternary") {} - - virtual bool run(void) { - using namespace Gecode; - - const int n = 1500; - TupleSet ts(3); - for (int i=0; i e(root); - delete root; - - SparseTernarySpace* sol = e.next(); - if (sol == nullptr) - return false; - const int a = sol->x[0].val(); - const int b = sol->x[1].val(); - const int c = sol->x[2].val(); - delete sol; - return (b == ((a*7) % n)) && (c == ((a*11) % n)); + SparseAssignment(const Gecode::TupleSet& t0, const Gecode::IntSet& d, + Gecode::Support::RandomGenerator& rand) + : RandomAssignment(t0.arity(),d,32,rand), t(t0) { + tuple(rand); } - }; - - /// Sparse smoke test for low-density higher-arity tuple sets - class SparseTupleSetHighArity : public ::Test::Base { - public: - SparseTupleSetHighArity(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::HighArity") {} - - virtual bool run(void) { - using namespace Gecode; - - const int n = 1000; - TupleSet ts(6); - for (int i=0; i e(root); - delete root; - - SparseHighAritySpace* sol = e.next(); - if (sol == nullptr) - return false; - const int a = sol->x[0].val(); - const int b = sol->x[1].val(); - const int c = sol->x[2].val(); - const int d = sol->x[3].val(); - const int e0 = sol->x[4].val(); - const int f = sol->x[5].val(); - delete sol; - return (b == ((a*3) % n)) && - (c == ((a*5) % n)) && - (d == ((a*7) % n)) && - (e0 == ((a*11) % n)) && - (f == ((a*13) % n)); + virtual void next(Gecode::Support::RandomGenerator& rand) { + RandomAssignment::next(rand); + tuple(rand); } }; - /// Sparse smoke test for nullary tuple sets - class SparseTupleSetNullary : public ::Test::Base { + /// Sparse tables with the original large support counts and arities. + class SparseTupleSet : public Test { + Gecode::TupleSet t; public: - SparseTupleSetNullary(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::Nullary") {} - - virtual bool run(void) { - using namespace Gecode; - - class SparseNullarySpace : public Space { - public: - IntVarArray x; - SparseNullarySpace(const TupleSet& t) - : x(*this,0,0,0) { - extensional(*this, x, t, true, IPL_DOM); - } - SparseNullarySpace(SparseNullarySpace& s) - : Space(s) { - x.update(*this,s.x); - } - virtual Space* - copy(void) { - return new SparseNullarySpace(*this); - } - }; - - TupleSet sat(0); - sat.add(IntArgs(0)); - sat.finalize(EPK_SPARSE); - if (sat.representation() != EPK_SPARSE) { - std::cerr << "ERROR: Nullary sat table not sparse" << std::endl; - return false; - } - SparseNullarySpace* sat_root = new SparseNullarySpace(sat); - DFS sat_engine(sat_root); - delete sat_root; - SparseNullarySpace* sat_sol = sat_engine.next(); - if (sat_sol == nullptr) { - std::cerr << "ERROR: Nullary sat table produced no solution" - << std::endl; - return false; + SparseTupleSet(const std::string& name, int arity, int size) + : Test("Extensional::TupleSet::Sparse::"+name, + arity,0,size-1,false,Gecode::IPL_DOM), t(arity) { + const int factors[] = {1,arity == 3 ? 7 : 3, + arity == 3 ? 11 : 5,7,11,13}; + for (int i=0; i unsat_engine(unsat_root); - delete unsat_root; - SparseNullarySpace* unsat_sol = unsat_engine.next(); - const bool ok = (unsat_sol == nullptr); - if (!ok) - std::cerr << "ERROR: Nullary empty table unexpectedly satisfiable" - << std::endl; - delete unsat_sol; - return ok; + t.finalize(Gecode::EPK_SPARSE); + testsearch = false; + contest = CTL_NONE; + } + virtual Assignment* assignment(void) const { + return new SparseAssignment(t,dom,_rand); + } + virtual bool solution(const Assignment& x) const { + const int size = dom.max()+1; + const int factors[] = {1,arity == 3 ? 7 : 3, + arity == 3 ? 11 : 5,7,11,13}; + for (int i=1; i e(root); - delete root; - - SparseDeltaSpace* sol = e.next(); - if (sol == nullptr) - return false; - SparseDeltaSpace* extra = e.next(); - const bool ok = sol->x[0].assigned() && sol->x[1].assigned() && - (sol->x[0].val() == 2) && (sol->x[1].val() == 2) && - (extra == nullptr); - delete sol; - delete extra; - return ok; + SparseTupleSetNullary(bool n) + : Test("Extensional::TupleSet::Sparse::Nullary::"+str(n), + 1,0,0), nonempty(n), t(0) { + if (nonempty) + t.add(Gecode::IntArgs(0)); + t.finalize(Gecode::EPK_SPARSE); + } + virtual bool solution(const Assignment&) const { + return nonempty; + } + virtual void post(Gecode::Space& home, Gecode::IntVarArray&) { + Gecode::extensional(home,Gecode::IntVarArgs(),t,true,Gecode::IPL_DOM); } }; - /// Sparse incremental test for assigned-variable advisor updates - class SparseTupleSetIncrementalAssign : public ::Test::Base { + /// Tells issued after posting exercise sparse advisor updates. + class SparseTupleSetIncremental : public Test { + int kind; + Gecode::TupleSet t; public: - SparseTupleSetIncrementalAssign(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::IncrementalAssign") {} - - virtual bool run(void) { + SparseTupleSetIncremental(const std::string& name, int k) + : Test("Extensional::TupleSet::Sparse::Incremental"+name, + 2,0,k == 2 ? 1 : 3,false,Gecode::IPL_DOM), kind(k), t(2) { using namespace Gecode; - - class SparseAssignSpace : public Space { - public: - IntVarArray x; - SparseAssignSpace(const TupleSet& t) - : x(*this,2,0,3) { - extensional(*this, x, t, true, IPL_DOM); - rel(*this, x[0], IRT_EQ, 2); - rel(*this, x[1], IRT_NQ, 1); - branch(*this, x, INT_VAR_NONE(), INT_VAL_MIN()); - } - SparseAssignSpace(SparseAssignSpace& s) - : Space(s) { - x.update(*this,s.x); - } - virtual Space* - copy(void) { - return new SparseAssignSpace(*this); - } - }; - - TupleSet ts(2); - ts.add(IntArgs({0,0})).add(IntArgs({1,1})) - .add(IntArgs({2,1})).add(IntArgs({3,3})); - ts.finalize(EPK_SPARSE); - if (ts.representation() != EPK_SPARSE) + if (kind == 2) + t.add(IntArgs({0,1})).add(IntArgs({1,0})); + else + t.add(IntArgs({0,0})).add(IntArgs({1,1})) + .add(IntArgs({2,kind == 1 ? 1 : 2})).add(IntArgs({3,3})); + t.finalize(EPK_SPARSE); + } + virtual bool solution(const Assignment& x) const { + if (kind == 0) + return (x[0] == 2) && (x[1] == 2); + if (kind == 1) return false; - - SparseAssignSpace* root = new SparseAssignSpace(ts); - DFS e(root); - delete root; - SparseAssignSpace* sol = e.next(); - const bool ok = (sol == nullptr); - delete sol; - return ok; + return (x[0] == 1) && (x[1] == 0); } - }; - - /// Sparse incremental test for BoolView specialization - class SparseTupleSetIncrementalBool : public ::Test::Base { - public: - SparseTupleSetIncrementalBool(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::IncrementalBool") {} - - virtual bool run(void) { + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) { using namespace Gecode; - - class SparseBoolSpace : public Space { - public: - BoolVarArray x; - SparseBoolSpace(const TupleSet& t) - : x(*this,2,0,1) { - extensional(*this, x, t, true, IPL_DOM); - rel(*this, x[0], IRT_NQ, 0); - branch(*this, x, BOOL_VAR_NONE(), BOOL_VAL_MIN()); - } - SparseBoolSpace(SparseBoolSpace& s) - : Space(s) { - x.update(*this,s.x); - } - virtual Space* - copy(void) { - return new SparseBoolSpace(*this); + if (kind == 2) { + BoolVarArgs b(2); + for (int i=0; i<2; i++) + b[i] = channel(home,x[i]); + extensional(home,b,t,true,ipl); + rel(home,b[0],IRT_NQ,0); + } else { + extensional(home,x,t,true,ipl); + if (kind == 0) { + rel(home,x[0],IRT_NQ,0); + rel(home,x[0],IRT_NQ,1); + rel(home,x[1],IRT_NQ,3); + } else { + rel(home,x[0],IRT_EQ,2); + rel(home,x[1],IRT_NQ,1); } - }; - - TupleSet ts(2); - ts.add(IntArgs({0,1})).add(IntArgs({1,0})); - ts.finalize(EPK_SPARSE); - if (ts.representation() != EPK_SPARSE) - return false; - - SparseBoolSpace* root = new SparseBoolSpace(ts); - DFS e(root); - delete root; - - SparseBoolSpace* sol = e.next(); - if (sol == nullptr) - return false; - SparseBoolSpace* extra = e.next(); - const bool ok = sol->x[0].assigned() && sol->x[1].assigned() && - (sol->x[0].val() == 1) && (sol->x[1].val() == 0) && - (extra == nullptr); - delete sol; - delete extra; - return ok; + } } }; @@ -1441,105 +1185,6 @@ namespace Test { namespace Int { } }; - /// Sparse smoke test for negative tuple-set posting - class SparseTupleSetNegative : public ::Test::Base { - public: - SparseTupleSetNegative(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::Negative") {} - - virtual bool run(void) { - using namespace Gecode; - - class SparseNegativeSpace : public Space { - public: - IntVarArray x; - SparseNegativeSpace(const TupleSet& t) - : x(*this,2,0,1) { - extensional(*this, x, t, false, IPL_DOM); - branch(*this, x, INT_VAR_NONE(), INT_VAL_MIN()); - } - SparseNegativeSpace(SparseNegativeSpace& s) - : Space(s) { - x.update(*this,s.x); - } - virtual Space* - copy(void) { - return new SparseNegativeSpace(*this); - } - }; - - TupleSet ts(2); - ts.add(IntArgs({0,0})).add(IntArgs({1,1})); - ts.finalize(EPK_SPARSE); - - SparseNegativeSpace* root = new SparseNegativeSpace(ts); - DFS e(root); - delete root; - - int n = 0; - while (SparseNegativeSpace* sol = e.next()) { - if (sol->x[0].val() == sol->x[1].val()) { - delete sol; - return false; - } - n++; - delete sol; - } - return n == 2; - } - }; - - /// Sparse smoke test for reified tuple-set posting - class SparseTupleSetReified : public ::Test::Base { - public: - SparseTupleSetReified(void) - : ::Test::Base("Int::Extensional::TupleSet::Sparse::Reified") {} - - virtual bool run(void) { - using namespace Gecode; - - class SparseReifiedSpace : public Space { - public: - IntVarArray x; - BoolVar b; - SparseReifiedSpace(const TupleSet& t) - : x(*this,2,0,1), b(*this,0,1) { - extensional(*this, x, t, true, Reify(b,RM_EQV), IPL_DOM); - rel(*this, b, IRT_EQ, 1); - branch(*this, x, INT_VAR_NONE(), INT_VAL_MIN()); - } - SparseReifiedSpace(SparseReifiedSpace& s) - : Space(s) { - x.update(*this,s.x); - b.update(*this,s.b); - } - virtual Space* - copy(void) { - return new SparseReifiedSpace(*this); - } - }; - - TupleSet ts(2); - ts.add(IntArgs({0,0})).add(IntArgs({1,1})); - ts.finalize(EPK_SPARSE); - - SparseReifiedSpace* root = new SparseReifiedSpace(ts); - DFS e(root); - delete root; - - int n = 0; - while (SparseReifiedSpace* sol = e.next()) { - if (sol->x[0].val() != sol->x[1].val()) { - delete sol; - return false; - } - n++; - delete sol; - } - return n == 2; - } - }; - /// Sparse/compressed tuplesets should materialize only requested support class TupleSetSingleRepresentation : public ::Test::Base { public: @@ -2154,76 +1799,6 @@ namespace Test { namespace Int { } }; - /// Sparse reified posting should support all reify modes for positive/negative - class SparseTupleSetReifiedModes : public ::Test::Base { - public: - SparseTupleSetReifiedModes(void) - : ::Test::Base( - "Int::Extensional::TupleSet::Sparse::ReifiedModes") {} - - virtual bool run(void) { - using namespace Gecode; - class ReifModeSpace : public Space { - public: - IntVarArray x; - BoolVar b; - ReifModeSpace(const TupleSet& t, bool pos, ReifyMode rm, int bv) - : x(*this,2,0,1), b(*this,0,1) { - extensional(*this, x, t, pos, Reify(b,rm), IPL_DOM); - rel(*this, b, IRT_EQ, bv); - branch(*this, x, INT_VAR_NONE(), INT_VAL_MIN()); - } - ReifModeSpace(ReifModeSpace& s) - : Space(s) { - x.update(*this,s.x); - b.update(*this,s.b); - } - virtual Space* copy(void) { - return new ReifModeSpace(*this); - } - }; - - TupleSet ts(2); - ts.add(IntArgs({0,0})); - ts.finalize(EPK_SPARSE); - if (ts.representation() != EPK_SPARSE) - return false; - - auto count = [&ts](bool pos, ReifyMode rm, int bv, - bool must_equal) { - ReifModeSpace* root = new ReifModeSpace(ts,pos,rm,bv); - DFS e(root); - delete root; - int n = 0; - while (ReifModeSpace* sol = e.next()) { - const bool eq = (sol->x[0].val() == 0) && (sol->x[1].val() == 0); - if (must_equal != eq) { - delete sol; - return -1; - } - n++; - delete sol; - } - return n; - }; - - if (count(true,RM_EQV,1,true) != 1) - return false; - if (count(true,RM_EQV,0,false) != 3) - return false; - if (count(true,RM_IMP,1,true) != 1) - return false; - if (count(true,RM_PMI,0,false) != 3) - return false; - if (count(false,RM_EQV,0,true) != 1) - return false; - if (count(false,RM_EQV,1,false) != 3) - return false; - - return true; - } - }; - /// %Test with large tuple set class TupleSetLarge : public Test { protected: @@ -2596,17 +2171,33 @@ namespace Test { namespace Int { RegTerminalMerged reg_sparse_terminal_merged; RegTerminalUnmerged reg_sparse_terminal_unmerged; - SparseTupleSetUnary sparse_tuple_set_unary; - SparseTupleSetTernary sparse_tuple_set_ternary; - SparseTupleSetHighArity sparse_tuple_set_high_arity; - SparseTupleSetNullary sparse_tuple_set_nullary; - SparseTupleSetIncrementalDelta sparse_tuple_set_incremental_delta; - SparseTupleSetIncrementalAssign sparse_tuple_set_incremental_assign; - SparseTupleSetIncrementalBool sparse_tuple_set_incremental_bool; + /// Exhaustive positive, negative, and reified sparse-table semantics. + class CreateSparse { + public: + CreateSparse(void) { + using namespace Gecode; + TupleSet equal(2), zero(2); + equal.add(IntArgs({0,0})).add(IntArgs({1,1})).finalize(EPK_SPARSE); + zero.add(IntArgs({0,0})).finalize(EPK_SPARSE); + for (bool positive : {false,true}) { + (void) new TupleSetTest("Equal",positive,IntSet(0,1),equal, + false,EPK_SPARSE,TestTags::standard()); + (void) new TupleSetTest("Zero",positive,IntSet(0,1),zero, + false,EPK_SPARSE,TestTags::standard()); + } + } + } create_sparse; + + SparseTupleSet sparse_tuple_set_unary("Unary",1,2000); + SparseTupleSet sparse_tuple_set_ternary("Ternary",3,1500); + SparseTupleSet sparse_tuple_set_high_arity("HighArity",6,1000); + SparseTupleSetNullary sparse_tuple_set_nullary(true); + SparseTupleSetNullary sparse_tuple_set_empty(false); + SparseTupleSetIncremental sparse_tuple_set_incremental_delta("Delta",0); + SparseTupleSetIncremental sparse_tuple_set_incremental_assign("Assign",1); + SparseTupleSetIncremental sparse_tuple_set_incremental_bool("Bool",2); SparseTupleSetDisabledFailure sparse_tuple_set_disabled_failure; SparseTupleSetWideDelta sparse_tuple_set_wide_delta; - SparseTupleSetNegative sparse_tuple_set_negative; - SparseTupleSetReified sparse_tuple_set_reified; TupleSetSingleRepresentation tuple_set_single_representation; TupleSetSupportOffsetBoundary tuple_set_support_offset_boundary; TupleSetTerminalFinalizationFailure tuple_set_terminal_failure; @@ -2616,7 +2207,6 @@ namespace Test { namespace Int { DenseCompressedTupleSetWideGap dense_compressed_tuple_set_wide_gap; SparseTupleSetNegativeFail sparse_tuple_set_negative_fail; SparseTupleSetNegativePrune sparse_tuple_set_negative_prune; - SparseTupleSetReifiedModes sparse_tuple_set_reified_modes; //@} } diff --git a/test/int/min-distance.cpp b/test/int/min-distance.cpp index d993efc72a..418af52f14 100644 --- a/test/int/min-distance.cpp +++ b/test/int/min-distance.cpp @@ -127,7 +127,8 @@ namespace Test { namespace Int { namespace MinDistance { virtual Gecode::Space* copy(void) { return new Model(*this); } }; - /// Matching certificates, zero witnesses, and callback lifetime + /// Domain filtering, matching strength, and callback lifetime + // Check domain bounds before assignment and ownership across Space clones. class Propagation : public Base { public: Propagation(void) : Base("Int::MinDistance::Propagation", @@ -150,31 +151,6 @@ namespace Test { namespace Int { namespace MinDistance { if ((clone->status() == SS_FAILED) || !clone->z.assigned() || (clone->z.val() != 2) || forward.z.assigned()) return false; - - // With only one pair, zero requires equal selections here. - Model zero(2,4,0,0,kind,level, - [](int a, int b) { return std::abs(a-b); }); - dom(zero,zero.x[0],IntSet({0,1})); - dom(zero,zero.x[1],IntSet({1,2})); - if ((zero.status() == SS_FAILED) || - !zero.x[0].assigned() || (zero.x[0].val() != 1) || - !zero.x[1].assigned() || (zero.x[1].val() != 1)) - return false; - - // Assigned objectives still need exact equality, not just >= z. - Model invalid(2,4,1,1,kind,level, - [](int a, int b) { return std::abs(a-b); }); - rel(invalid,invalid.x[0],IRT_EQ,0); - rel(invalid,invalid.x[1],IRT_EQ,3); - if (invalid.status() != SS_FAILED) - return false; - - // One active site can be repeated at objective zero. - Model repeated(3,1,0,3,kind,level, - [](int, int) { return 0; }); - if ((repeated.status() == SS_FAILED) || !repeated.z.assigned() || - (repeated.z.val() != 0)) - return false; } // A perfect conflict matching rules out selecting three sites at 3. diff --git a/test/int/mm-bool.cpp b/test/int/mm-bool.cpp index fa3b3b75d4..ef0c1415dd 100644 --- a/test/int/mm-bool.cpp +++ b/test/int/mm-bool.cpp @@ -254,7 +254,8 @@ namespace Test { namespace Int { home.fail(); return; } - home.fail(); + throw Exception("Test::BoolExprInvalid", + "Expected MiniModel::TooFewArguments"); } }; diff --git a/test/int/mm-lin.cpp b/test/int/mm-lin.cpp index e1603a1c5e..c1f5d47671 100755 --- a/test/int/mm-lin.cpp +++ b/test/int/mm-lin.cpp @@ -95,40 +95,20 @@ namespace Test { namespace Int { */ //@{ /// %Test public default linear expression behavior - class LinExprDefaultSpace : public Gecode::Space { + class LinExprDefault : public Test { public: - Gecode::IntVar x; - LinExprDefaultSpace(void) : x(*this,-5,5) { + LinExprDefault(void) : Test("MiniModel::LinExpr::Default",1,-5,5) {} + virtual bool solution(const Assignment& x) const { + return x[0] == 1; + } + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) { using namespace Gecode; LinIntExpr e; LinIntExpr c(e); - LinIntExpr a = e + x; + LinIntExpr a = e + x[0]; LinIntExpr b = 2 + c; LinIntExpr m = 3 * e; - rel(*this, a + b + m == 3); - } - LinExprDefaultSpace(LinExprDefaultSpace& s) : Gecode::Space(s) { - x.update(*this,s.x); - } - virtual Gecode::Space* copy(void) { - return new LinExprDefaultSpace(*this); - } - }; - - /// %Test public default linear expression behavior - class LinExprDefault : public Test::Base { - public: - LinExprDefault(void) : Test::Base("MiniModel::LinExpr::Default") {} - virtual bool run(void) { - LinExprDefaultSpace* s = new LinExprDefaultSpace; - Gecode::DFS e(s); - delete s; - LinExprDefaultSpace* sol = e.next(); - if (sol == nullptr) - return false; - bool ok = sol->x.assigned() && (sol->x.val() == 1); - delete sol; - return ok && (e.next() == nullptr); + rel(home, a + b + m == 3); } };