Some cleanup of miplib regressions and options

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 73e2b84c4b06b2eac354975dd3cff0f059c9e836..4104c09161ba5d5aa3411d957c1feb0404d4a51e 100644 (file)
--- 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 2a745a608dbe12a8408a506e06dff289f87723a8..e12120f33810d174fdc38fbc3f472fdcbf9e9010 100644 (file)
--- 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 1510b15ad1388831766b354b5a995866ce7773f6..b0cdc5b918c281e55f49ac296c4f879f7207ca2e 100644 (file)
--- 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 04a3504d7a6dcebc42f072bdca2602503629a036..f6ae1d85b66c648f727f647b63bc08a31501ca97 100644 (file)
--- 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 49d652d800e7db92b7ea26f8a45086a57585e70e..e6ac8e69e2cffd73ab1d4f5647ce3c47de9e5a35 100644 (file)
--- 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 04a3504d7a6dcebc42f072bdca2602503629a036..f6ae1d85b66c648f727f647b63bc08a31501ca97 100644 (file)
--- 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 5bbf0a7583b379654e309f01c1f0d397244c5250..e94506a235f9ba619adc5208ef37aa79a9b5e843 100644 (file)
--- 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 4cd4b25b5c07ab5ed7f3def5de86dea5ee31d833..db2aa2ac55ea35d538b903fef1e70b9a67e0846c 100644 (file)
--- 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 6fbfcab0f530b263ff3faf1ccb28c4fc2478ab1e..84f17e84816e3b447079249edbc9db7b10b2d5fe 100644 (file)
--- 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