Check in some scripts

3 files changed, 43 insertions, 3 deletions

diff --git a/benchmark.sh b/benchmark.sh
new file mode 100755
index 000000000..1b54e3cd2
--- /dev/null
+++ b/benchmark.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+set -e
+i=0
+for file in $(head -n $1 $HOME/sorted_smt_lib.list)
+do
+  i=$(($i+1))
+  if [ $((i % 10)) == 0 ] ; then
+    echo "$i / $1"
+  fi
+  $PWD/bin/cvc5 --arith-idl-ext $file > /dev/null
+done
diff --git a/matthew_test.sh b/matthew_test.sh
new file mode 100755
index 000000000..9f9eb3460
--- /dev/null
+++ b/matthew_test.sh
@@ -0,0 +1,29 @@
+#!/bin/bash
+
+set -e
+
+RUN_SIMPLE=false
+GET_STATS=true
+RUN_SMTLIB=500
+TIMEOUT_SMTLIB=5m
+
+if [ $GET_STATS = true ] ; then
+  OPTS="$OPTS --stats-expert"
+fi
+
+OPTS="$OPTS --arith-idl-ext"
+
+if [ $RUN_SIMPLE = true ] ; then
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/example-rewritten.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/example.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/example-rewritten-sat.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/matthew-many-syntax.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/matthew-backtrack-needed.smt2
+fi
+# ./bin/cvc5 --stats-expert --arith-idl-ext ../test/regress/regress0/idl/matthew-adapted-smtlib.smt2
+
+for test_file in $(cat $HOME/sorted_smt_lib.list | head -n $RUN_SMTLIB)
+do
+  echo "./bin/cvc5 $OPTS $test_file"
+  timeout $TIMEOUT_SMTLIB ./bin/cvc5 $OPTS $test_file
+done
diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index b3b435fa3..74d512901 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -427,9 +427,9 @@ std::vector<std::vector<TNode>> IdlExtension::negativeCycles()
     }
     Assert(weight < zero);
     cycles.emplace_back(std::move(assertion_cycle));
-    // TODO: Breaking early here seems to be a toss-up on whether it helps or
-    // hurts. Should do some more systematic benchmarking.
-    // break;
+    // TODO: Breaking early here seems to help by a few seconds on the shortest
+    // 50 benchmarks. Should re-run on a larger set.
+    break;
   }
   Assert(!cycles.empty());
   return cycles;