From ce7c485182902ae43871057185095f71f74a8a58 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 3 Feb 2013 15:37:04 -0500 Subject: [PATCH] new option for doing top-level miplib substitutions (or not) --- src/smt/smt_engine.cpp | 2 +- src/theory/arith/options | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) 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 -- 2.30.2