projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ecff741) | patch
- Turns on the excluded middle assertions during the miplibTrick. If it is known...
authorTim King <taking@cs.nyu.edu>
Wed, 16 Mar 2011 22:08:15 +0000 (22:08 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 16 Mar 2011 22:08:15 +0000 (22:08 +0000)
commit84146b42ed0e1c0298b0e2a894c33f357a4483ef
treef315bb9b45f2baed00d6ee8fdd58a8fbd69f3269tree
parentecff741b43b7c5493a7e1ef801cbe7ff68f8ff54commit | diff
- Turns on the excluded middle assertions during the miplibTrick. If it is known that x \in {c_i}, then x is not in the interval (c_{i}, c_{i+1}) (assuming the c_i's are sorted). (Compare jobs 1742 and 1739 for the expected performance change on trunk. Compare jobs 1740 and 1738 for the expected performance change with the rewrite-equality patch.)
src/theory/arith/theory_arith.cpp diff | blob | history