From 72cae59d28aa43b734148090feb3b8cf4ecd2074 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 3 Feb 2013 16:05:37 -0500 Subject: [PATCH] Some cleanup of miplib regressions and options --- src/smt/smt_engine.cpp | 3 +-- src/theory/arith/options | 4 ++-- test/regress/regress0/arith/Makefile.am | 12 +++++++----- .../regress0/arith/miplib-opt1217--27.smt.expect | 2 +- test/regress/regress0/arith/miplib-opt1217--27.smt2 | 2 +- .../regress0/arith/miplib-pp08a-3000.smt.expect | 2 +- test/regress/regress0/arith/miplib-pp08a-3000.smt2 | 2 +- test/regress/regress0/arith/miplib.cvc | 1 + test/regress/regress0/arith/miplib2.cvc | 1 + 9 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 73e2b84c4..4104c0916 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2202,7 +2202,6 @@ void SmtEnginePrivate::doMiplibTrick() { Debug("miplib") << " -- INELIGIBLE " << (*j).first << " -- (insufficiently marked, got " << (*j).second << " for " << numVars << " vars, expected " << expected << endl; } else { if(false) { //checks[(*j).first] != coef[(*j).first][0] + coef[(*j).first][1]) { -#warning fixme Debug("miplib") << " -- INELIGIBLE " << (*j).first << " -- (not linear combination)" << endl; } else { Debug("miplib") << " -- ELIGIBLE " << *i << " , " << (*j).first << " --" << endl; @@ -2252,7 +2251,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 if(arithMLTrickSubstitutions) { + } else if(options::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 2a745a608..e12120f33 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -51,11 +51,11 @@ option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite- turns on the preprocessing rewrite turning equalities into a conjunction of inequalities /turns off the preprocessing rewrite turning equalities into a conjunction of inequalities -option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default true +option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false 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 +option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs bool :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 diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 1510b15ad..b0cdc5b91 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -41,14 +41,16 @@ TESTS = \ bug443.delta01.smt \ miplib.cvc \ miplib2.cvc \ - miplibtrick.smt \ + miplibtrick.smt +# problem__003.smt2 + +EXTRA_DIST = $(TESTS) \ miplib-opt1217--27.smt \ miplib-opt1217--27.smt2 \ miplib-pp08a-3000.smt \ - miplib-pp08a-3000.smt2 -# problem__003.smt2 - -EXTRA_DIST = $(TESTS) + miplib-pp08a-3000.smt2 \ + miplib-opt1217--27.smt.expect \ + miplib-pp08a-3000.smt.expect #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect index 04a3504d7..f6ae1d85b 100644 --- a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect +++ b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect @@ -1,3 +1,3 @@ -% COMMAND-LINE: --tlimit 5000 +% COMMAND-LINE: --enable-miplib-trick % EXPECT: unsat % EXIT: 20 diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt2 b/test/regress/regress0/arith/miplib-opt1217--27.smt2 index 49d652d80..e6ac8e69e 100644 --- a/test/regress/regress0/arith/miplib-opt1217--27.smt2 +++ b/test/regress/regress0/arith/miplib-opt1217--27.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --tlimit 5000 +; COMMAND-LINE: --enable-miplib-trick ; EXPECT: unsat ; EXIT: 20 (set-logic QF_LRA) diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect index 04a3504d7..f6ae1d85b 100644 --- a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect +++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect @@ -1,3 +1,3 @@ -% COMMAND-LINE: --tlimit 5000 +% COMMAND-LINE: --enable-miplib-trick % EXPECT: unsat % EXIT: 20 diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt2 b/test/regress/regress0/arith/miplib-pp08a-3000.smt2 index 5bbf0a758..e94506a23 100644 --- a/test/regress/regress0/arith/miplib-pp08a-3000.smt2 +++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --tlimit 5000 +; COMMAND-LINE: --enable-miplib-trick ; EXPECT: unsat ; EXIT: 10 (set-logic QF_LRA) diff --git a/test/regress/regress0/arith/miplib.cvc b/test/regress/regress0/arith/miplib.cvc index 4cd4b25b5..db2aa2ac5 100644 --- a/test/regress/regress0/arith/miplib.cvc +++ b/test/regress/regress0/arith/miplib.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: --enable-miplib-trick % EXPECT: sat % EXIT: 10 diff --git a/test/regress/regress0/arith/miplib2.cvc b/test/regress/regress0/arith/miplib2.cvc index 6fbfcab0f..84f17e848 100644 --- a/test/regress/regress0/arith/miplib2.cvc +++ b/test/regress/regress0/arith/miplib2.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: --enable-miplib-trick % EXPECT: sat % EXIT: 10 -- 2.30.2