diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 16:01:17 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 16:37:04 -0500 |
| commit | 9c0b2f6abd82564df0686cca826015f4eb9095fa (patch) | |
| tree | 8fba8acbecdd08ee82d943bd3ded7148f29f035f /src/theory/arith | |
| parent | 2c460aacc9b3d52e4c6423fa54a8437b5be5c04b (diff) | |
Some fixes for the miplib preprocessing pass.
* TNode violation bug fix (thanks to Tim King for discovery & fix)
* change Boolean miplib-trick substitution option into a threshold
* ppAssert() the generated miplib constraints to arithmetic
Diffstat (limited to 'src/theory/arith')
| -rw-r--r-- | src/theory/arith/options | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/options b/src/theory/arith/options index e12120f33..9e758a0ef 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -55,8 +55,8 @@ option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bo turns on the preprocessing step of attempting to infer bounds on miplib problems /turns off the preprocessing step of attempting to infer bounds on miplib problems -option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs bool :default true - does top-level substitution for miplib 'tmp' vars +option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned :default 1 + do substitution for miplib 'tmp' vars if defined in <= N eliminated vars option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds |