Add some unit tests (which run when regressall is run) to check that simplifications...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@846 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index f658a9cfd6121f7be3412c11538b24a25804254a..71241b1d8064ae20ffc99487e1c4d4b942fc9bc4 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -119,8 +119,14 @@ regressall: all
        $(MAKE) regresseric
        $(MAKE) regresshistar
        $(MAKE) regresscrypto
+       $(MAKE) unit_test
        $(MAKE) regresscapi
+       
 
+# Checks that simplifications are working.
+.PHONY: unit_test
+unit_test:
+       cd unit_test ; ./unit_test.sh
 
 # Runs the basic tests in tests/
 .PHONY: check

diff --git a/tests/generated_tests/ArrayGenerator.java b/tests/generated_tests/ArrayGenerator.java
index 9b683300515425cc59d9ad3221e035a03f6f327c..42c442737c5faca419b5bdad6f48af613d189ac7 100644 (file)
--- a/tests/generated_tests/ArrayGenerator.java
+++ b/tests/generated_tests/ArrayGenerator.java
@@ -14,9 +14,8 @@ public class ArrayGenerator
     public static List<String> arrays = new ArrayList<String>();\r
     static Random r = new Random();\r
 \r
-    // When we get to a nesting of 5, start to return leaf nodes (like symbols).\r
-    static int MAX_DEPTH = 8;\r
-    \r
+    static int MAX_DEPTH;\r
+\r
     public static void main(String[] args)\r
     {\r
        bits.add("b1");\r
@@ -27,6 +26,9 @@ public class ArrayGenerator
        arrays.add("a2");\r
        arrays.add("a3");\r
 \r
+       // When we get to the nesting depth, start to return leaf nodes (like symbols).\r
+       MAX_DEPTH = r.nextInt(15) +1;\r
+\r
        randomGenerate();\r
     }\r
 \r
@@ -41,15 +43,16 @@ public class ArrayGenerator
 \r
        for (String s : bits)\r
        {\r
-           output.append(":extrafuns (( " + s + " BitVec[10]))\n");\r
+           output.append(":extrafuns (( " + s + " BitVec[4]))\n");\r
        }\r
 \r
        for (String s : arrays)\r
        {\r
-           output.append(":extrafuns (( " + s + " Array[10:10]))\n");\r
+           output.append(":extrafuns (( " + s + " Array[4:4]))\n");\r
        }\r
 \r
-       for (int i = 0; i < 10; i++)\r
+       int top = r.nextInt(10);\r
+       for (int i = 0; i < top+1; i++)\r
            output.append(":assumption " + generateProp(0) + "\n");\r
 \r
        output.append(":formula true \n )\n");\r
@@ -127,7 +130,7 @@ public class ArrayGenerator
        case 1:\r
            return "(= " + generateBit(depth) + " " + generateBit(depth) + " )";\r
        case 2: \r
-           return "(and " + generateProp(depth) + " " + generateProp(depth) + " )";\r
+           return "(or " + generateProp(depth) + " " + generateProp(depth) + " )";\r
        case 3: \r
            return "(bvslt " + generateBit(depth) + " " + generateBit(depth) + " )";\r
        case 4: \r

diff --git a/unit_test/bvand.smt2 b/unit_test/bvand.smt2
new file mode 100644 (file)
index 0000000..db86cd4
--- /dev/null
+++ b/unit_test/bvand.smt2
@@ -0,0 +1,21 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 1))
+
+(assert (= (concat (_ bv0 1) v0) (_ bv2 2)))
+
+
+
+
+(check-sat)
+(exit)
+
+
+;1126:(EQ 
+;  24:0b01010
+; 1124:(BVCONCAT 
+;    114:0b000
+;    1108:array_a2_1))

diff --git a/unit_test/bvand2.smt2 b/unit_test/bvand2.smt2
new file mode 100644 (file)
index 0000000..98ca802
--- /dev/null
+++ b/unit_test/bvand2.smt2
@@ -0,0 +1,31 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+
+(assert (bvsgt (_ bv0 2) (bvnot (bvand (_ bv1 2) v0)) ))
+
+
+
+
+(check-sat)
+(exit)
+
+; Something like this..
+;1498:(BVSGT 
+;  1496:(BVCONCAT 
+;    538:0b00000000000000
+;    1494:(ITE 
+;      1486:(BVGE 
+;        1482:(BVSX 
+;          1480:array_a7_0
+;          62:0x00000008)
+;        12:v0)
+;      54:0b1
+;      56:0b0))
+;  286:(BVNEG 
+;    284:(BVAND 
+;      274:0b000000001001110
+;      20:v4)))

diff --git a/unit_test/bvnor.smt2 b/unit_test/bvnor.smt2
new file mode 100644 (file)
index 0000000..d543fab
--- /dev/null
+++ b/unit_test/bvnor.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(declare-fun v2 () (_ BitVec 2))
+
+(assert (= (bvor v0 v0) (_ bv0 2)))
+(assert (= (bvxor v1 v1) (_ bv0 2)))
+
+(check-sat)
+(exit)

diff --git a/unit_test/bvor.smt2 b/unit_test/bvor.smt2
new file mode 100644 (file)
index 0000000..7dbd9aa
--- /dev/null
+++ b/unit_test/bvor.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(assert (= (bvor v0 v0) (_ bv0 2)))
+(assert (= (bvor v1 (bvnot v1)) (_ bv3 2)))
+
+(check-sat)
+(exit)

diff --git a/unit_test/bvsge.smt2 b/unit_test/bvsge.smt2
new file mode 100644 (file)
index 0000000..c459bac
--- /dev/null
+++ b/unit_test/bvsge.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(assert (bvsge v0 v0))
+(check-sat)
+(exit)

diff --git a/unit_test/bvsgt.smt2 b/unit_test/bvsgt.smt2
new file mode 100644 (file)
index 0000000..46991de
--- /dev/null
+++ b/unit_test/bvsgt.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(declare-fun p () Bool)
+(assert (bvsgt (_ bv4 3) (ite p (_ bv7 3)(_ bv0 3) ) ) )
+(check-sat)
+(exit)

diff --git a/unit_test/bvshift.smt2 b/unit_test/bvshift.smt2
new file mode 100644 (file)
index 0000000..4140aea
--- /dev/null
+++ b/unit_test/bvshift.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(declare-fun v2 () (_ BitVec 2))
+
+(assert (= (bvshl (_ bv0 2) v0) (_ bv0 2)))
+(check-sat)
+(exit)

diff --git a/unit_test/bvxor.smt2 b/unit_test/bvxor.smt2
new file mode 100644 (file)
index 0000000..cab46b3
--- /dev/null
+++ b/unit_test/bvxor.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+
+(assert (bvule (bvxor v0 (_ bv0 2)) v0))
+
+
+
+(check-sat)
+(exit)
+

diff --git a/unit_test/output_0.cnf b/unit_test/output_0.cnf
new file mode 100644 (file)
index 0000000..b5a3851
--- /dev/null
+++ b/unit_test/output_0.cnf
@@ -0,0 +1,3 @@
+p cnf 1 2
+1 0
+1 0

diff --git a/unit_test/unit_test.sh b/unit_test/unit_test.sh
new file mode 100755 (executable)
index 0000000..8369910
--- /dev/null
+++ b/unit_test/unit_test.sh
@@ -0,0 +1,17 @@
+#!/bin/bash     
+
+#Each file should be simplified down to either true or false, so the CNF generated should
+#be very small if simplifications are working as they should.
+
+rm output_*.cnf
+
+files=`ls -1 -S *.smt2`
+for f in $files; do
+       stp --output-CNF $f
+       cnf=`cat output_*.cnf  | wc -l`
+       if [ $cnf -gt 3 ] ; then
+               exit 10
+       fi
+
+done
+