- Turns on the miplibTrick. This detects during the static learning phase a set...
authorTim King <taking@cs.nyu.edu>
Wed, 16 Mar 2011 15:36:45 +0000 (15:36 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 16 Mar 2011 15:36:45 +0000 (15:36 +0000)
commitecff741b43b7c5493a7e1ef801cbe7ff68f8ff54
tree002caa8263ff2b9ccb4873db1e0b0e1d55aedf7e
parent4ee5a74967c9cd273ca3449b948ac8a12834991c
- Turns on the miplibTrick.  This detects during the static learning phase a set of nodes that are asserted to the theory of the form (=> p_i (= x c_i)). If (or p_1 p_2 ...) is a tautology, then x \in {c_1, c_2, ...}. (This tautology check currently requires CUDD to be installed.)  Right now all this does is assert x \leq max{c_i} and x \geq min{c_i}. (Compare jobs 1728 to 1626 for how this affects the miplib examples.)
src/theory/arith/theory_arith.cpp