Setting up datatype inference manager, add mkfinalrulecount script.

1 files changed, 14 insertions, 0 deletions

diff --git a/contrib/mkfinalrulecount b/contrib/mkfinalrulecount
new file mode 100644
index 000000000..7f6b38eca
--- /dev/null
+++ b/contrib/mkfinalrulecount
@@ -0,0 +1,14 @@
+#!/bin/bash
+echo "mkfinalcount: Make regress with stats..."
+make regress -j8 CVC4_REGRESSION_ARGS="--stats --check-proofs-new $@" >& temp.txt
+echo "Do grep for final rule counts..."
+cat temp.txt | grep ruleCount > temp-rc.txt
+#rm temp.txt
+echo "Clean..."
+sed -i $'s/[^[:print:]\t]//g' temp-rc.txt
+sed -i 's/\[92m+finalProof::ruleCount, "\[//g; s/)/\n/g; s/,//g; s/ (//g; s/(//g; s/]"\[0m//g; s/ : /,/g' temp-rc.txt
+sed -i '/^$/d' temp-rc.txt
+echo "Aggregate..."
+awk -F, '{a[$1]+=$2;}END{for(i in a)print i", "a[i];}' temp-rc.txt
+#rm temp-rc.txt
+