def testOr_2(self):
     var1 = Variable(0, 2)
     dur1 = 1
     
     var2 = Variable(0, 4)
     dur2 = 2
     
     var3 = Variable(0, 6)
     dur3 = 3
     
     model = NativeModel()
     
     #model.add( NoOverlap( (var1, var2), (dur1, dur2) ) )
     #model.add( NoOverlap( (var1, var3), (dur1, dur3) ) )
     #model.add( NoOverlap( (var2, var3), (dur2, dur3) ) )
     
     ur = UnaryResource ( [ NoOverlap( (var1, var2), (dur1, dur2) ),
                                  NoOverlap( (var1, var3), (dur1, dur3) ),
                                  NoOverlap( (var2, var3), (dur2, dur3) ) ] )
     
     model.add( ur )
     
     solver = Solver(model)
     
     assert(solver.solve())
     
     assert ( (var1.get_value() + dur1 < var2.get_value ) or
         ( var2.get_value() + dur2 < var1.get_value  ) )

 def testSumConstant(self):
      obj1 = Variable(list(range(0,6)))
      obj2 = Variable(list(range(0,8)))
      obj3 = Variable(list(range(0,11)))
 
      capacity = Variable(list(range(34,35)))
      volumes = [7, 5, 3]
 
      model = NativeModel()
 
      vol_sum = Sum(((obj1, obj2, obj3), volumes))
 
      model.add_variable((obj1, obj2, obj3, vol_sum, capacity))
 
      model.add_constraint(Leq((vol_sum, capacity)))
      
      solver = Solver(model)
     
      '''
      obj1.print_domain()
      obj2.print_domain()
      obj3.print_domain()
      vol_sum.print_domain()
      capacity.print_domain()
      '''
      
      assert( solver.solve() )
      
      '''

 def testMinusOverNativeModelOp(self):
     var1, var2 = (Variable(range(0,4)), Variable(range(0,4)))
     
     model = NativeModel()
     
     model << (var1 == var2 - 3)
     
     solver = Solver(model)
     assert(solver.solve())

 def testTimesOver(self):
     var1, var2 = (Variable(range(1,4)), Variable(range(0,4)))
     
     model = NativeModel()
     
     model.add_constraint(var1 == var2 * 2)
     
     solver = Solver(model)
     assert(solver.solve())

 def testExactlyUNSAT_2(self):
     model = NativeModel()
     var1, var2 = (Variable(0,5), Variable(0,5))
     
     model << (Exactly(((var1, var2), 2, 3)))
     
     solver = Solver(model)
     
     assert(not solver.solve())

 def testTimesOverNativeModelOp(self):
     var1, var2 = (Variable(list(range(1,4))), Variable(list(range(0,4))))
     
     model = NativeModel()
     
     model << (var1 == var2 * 2)
     
     solver = Solver(model)
     assert(solver.solve())

 def testAtLeastUNSAT_2(self):
     model = NativeModel()
     var1, var2 = (Variable(0,5), Variable(0,5))
     
     model << (AtLeast(([var1, var2], 0, 3)))
     
     solver = Solver(model)
     
     assert(not solver.solve())

 def testOperatorOVerloading(self):
     var1 = Variable(list(range(0,4)))
     var2 = Variable(list(range(0,4)))
     
     model = NativeModel()
     model.add_constraint(var1 != var2)
                          
     solver = Solver(model)
     assert(solver.solve())

 def testAtMostUNSAT_2(self):
     model = NativeModel()
     var1, var2 = (Variable(2,2), Variable(0,1))
     
     model << (AtMost(([var1, var2], 2, 2)))
     
     solver = Solver(model)
     
     assert(solver.solve())

 def testMinusOver(self):
     var1, var2 = (Variable(list(range(0,4))), Variable(list(range(0,4))))
     
     model = NativeModel()
     
     model.add_constraint(var1 == var2 - 3)
     
     solver = Solver(model)
     assert(solver.solve())

 def testGTOver(self):
     var1, var2, var3 = (Variable(list(range(0,3))) for x in range(0,3))
     model = NativeModel()
     
     model.add_constraint(var1 < var2)
     model.add_constraint(var2 < var3)
     model.add_constraint(var1 < var3)
     
     solver = Solver(model)
     assert(solver.solve())

 def testEqualOver(self):
     var1 = Variable([0])
     var2 = Variable(list(range(0,1)))
     
     model = NativeModel()
     
     model.add_constraint(var1 == var2)
     
     solver = Solver(model)
     assert(solver.solve())

 def testEqual(self):
     var1 = Variable([0])
     var2 = Variable(list(range(0,1)))
     
     model = NativeModel()
     
     model.add_variable((var1, var2))
     
     solver = Solver(model)
     assert(solver.solve())

 def testMinus(self):
     var1, var2 = (Variable(list(range(0,4))), Variable(list(range(0,4))))
     
     model = NativeModel()
     model.add_variable((var1, var2))
     
     model.add_constraint(Equal((var1, Minus(var2, 3))))
     
     solver = Solver(model)
     assert(solver.solve())

 def testExactlySAT_2(self):
     model = NativeModel()
     var1, var2 = (Variable(0,5), Variable(0,5))
     
     model << (Exactly(((var1, var2), 2, 1)))
     
     solver = Solver(model)
     
     assert(solver.solve())
     assert((var1.get_value() is 2 or var2.get_value() is 2))

 def testStupid_not_eqOver(self):
     var1 = Variable(list(range(0,3)))
     var2 = Variable(list(range(0,3)))
     
     model = NativeModel()
     model.add_constraint(var1 != var2)
         
     solver = Solver(model)
     
     assert(solver.solve())    
     assert(var1.get_value() != var2.get_value())

 def testAtLeastSAT(self):
     model = NativeModel()
     var1, var2 = (Variable(0,5), Variable(0,5))
     
     model << (AtLeast(([var1, var2], 2, 2)))
     
     solver = Solver(model)
     
     assert(solver.solve())
     assert(var1.get_value() is 2)
     assert(var2.get_value() is 2)

   def testNotUnsat(self):
       var1 = Variable(0, 1)
       var2 = Variable(2, 3)
 
       model = NativeModel()
       
       model << (Not(var1 != var2))
       
       solver = Solver(model)
       
       assert(not solver.solve())

    def testNegDomains(self):
        var1 = Variable(-3, -1)
        var2 = Variable(-2, 0)
        
        model = NativeModel()

        model << (var1*2 <= var2)
        
        solver = Solver(model)
        
        assert(solver.solve())

 def testMaximization(self):
     model = NativeModel()
     
     var1, var2 = (Variable(0,4) for x in range(0,2))
     var3 = Variable(0,10)
     
     model << (var1 + var2 == var3)
     
     solver = Solver(model)
     
     assert( solver.maximise(var3) )