From a1601e7de20bc2347923fd98e23f5f6561ecef2e Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 14 Jun 2010 13:20:54 +0000 Subject: [PATCH] Add some unit tests (which run when regressall is run) to check that simplifications are turning problems into TRUE or FALSE. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@846 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.in | 6 +++++ tests/generated_tests/ArrayGenerator.java | 17 ++++++++----- unit_test/bvand.smt2 | 21 +++++++++++++++ unit_test/bvand2.smt2 | 31 +++++++++++++++++++++++ unit_test/bvnor.smt2 | 13 ++++++++++ unit_test/bvor.smt2 | 11 ++++++++ unit_test/bvsge.smt2 | 8 ++++++ unit_test/bvsgt.smt2 | 8 ++++++ unit_test/bvshift.smt2 | 11 ++++++++ unit_test/bvxor.smt2 | 13 ++++++++++ unit_test/output_0.cnf | 3 +++ unit_test/unit_test.sh | 17 +++++++++++++ 12 files changed, 152 insertions(+), 7 deletions(-) create mode 100644 unit_test/bvand.smt2 create mode 100644 unit_test/bvand2.smt2 create mode 100644 unit_test/bvnor.smt2 create mode 100644 unit_test/bvor.smt2 create mode 100644 unit_test/bvsge.smt2 create mode 100644 unit_test/bvsgt.smt2 create mode 100644 unit_test/bvshift.smt2 create mode 100644 unit_test/bvxor.smt2 create mode 100644 unit_test/output_0.cnf create mode 100755 unit_test/unit_test.sh diff --git a/scripts/Makefile.in b/scripts/Makefile.in index f658a9c..71241b1 100644 --- 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 9b68330..42c4427 100644 --- a/tests/generated_tests/ArrayGenerator.java +++ b/tests/generated_tests/ArrayGenerator.java @@ -14,9 +14,8 @@ public class ArrayGenerator public static List arrays = new ArrayList(); static Random r = new Random(); - // When we get to a nesting of 5, start to return leaf nodes (like symbols). - static int MAX_DEPTH = 8; - + static int MAX_DEPTH; + public static void main(String[] args) { bits.add("b1"); @@ -27,6 +26,9 @@ public class ArrayGenerator arrays.add("a2"); arrays.add("a3"); + // When we get to the nesting depth, start to return leaf nodes (like symbols). + MAX_DEPTH = r.nextInt(15) +1; + randomGenerate(); } @@ -41,15 +43,16 @@ public class ArrayGenerator for (String s : bits) { - output.append(":extrafuns (( " + s + " BitVec[10]))\n"); + output.append(":extrafuns (( " + s + " BitVec[4]))\n"); } for (String s : arrays) { - output.append(":extrafuns (( " + s + " Array[10:10]))\n"); + output.append(":extrafuns (( " + s + " Array[4:4]))\n"); } - for (int i = 0; i < 10; i++) + int top = r.nextInt(10); + for (int i = 0; i < top+1; i++) output.append(":assumption " + generateProp(0) + "\n"); output.append(":formula true \n )\n"); @@ -127,7 +130,7 @@ public class ArrayGenerator case 1: return "(= " + generateBit(depth) + " " + generateBit(depth) + " )"; case 2: - return "(and " + generateProp(depth) + " " + generateProp(depth) + " )"; + return "(or " + generateProp(depth) + " " + generateProp(depth) + " )"; case 3: return "(bvslt " + generateBit(depth) + " " + generateBit(depth) + " )"; case 4: diff --git a/unit_test/bvand.smt2 b/unit_test/bvand.smt2 new file mode 100644 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 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 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 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 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 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 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 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 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 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 + -- 2.47.3