diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 15:37:04 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 15:55:10 -0500 |
| commit | ce7c485182902ae43871057185095f71f74a8a58 (patch) | |
| tree | 0504dff660c6a0b048a5f372ebee25b6336604e7 /src | |
| parent | abadf2e3c081530ed7000d01f759e3b7bec09b4a (diff) | |
new option for doing top-level miplib substitutions (or not)
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
| -rw-r--r-- | src/theory/arith/options | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5c55adc7a..73e2b84c4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2252,7 +2252,7 @@ void SmtEnginePrivate::doMiplibTrick() { //Warning() << "REPLACE " << newAssertion[1] << endl; //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl; Assert(d_topLevelSubstitutions.getSubstitution(newAssertion[0]) == newAssertion[1]); - } else { + } else if(arithMLTrickSubstitutions) { d_topLevelSubstitutions.addSubstitution(newAssertion[0], newAssertion[1]); } Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl; diff --git a/src/theory/arith/options b/src/theory/arith/options index d21ccc0ee..2a745a608 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -55,6 +55,9 @@ 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 :default true + does top-level substitution for miplib 'tmp' 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 / turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds |