From d1311fd2f1e629b1d554cad8f6d1c37e8bb52d51 Mon Sep 17 00:00:00 2001 From: katelman Date: Tue, 18 Nov 2008 18:36:25 +0000 Subject: [PATCH] actually pushing this copy out for realase... git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@42 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile.in | 5 +- bin/run_tests | 2 +- sample-tests/egt-1899.cvc | 217 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 220 insertions(+), 4 deletions(-) create mode 100644 sample-tests/egt-1899.cvc diff --git a/Makefile.in b/Makefile.in index 169adbc..1438bce 100644 --- a/Makefile.in +++ b/Makefile.in @@ -51,8 +51,8 @@ clean: rm -rf bin/*~ rm -rf bin/stp rm -rf *.log - @#rm -rf Makefile - @#rm -rf config.info + #rm -rf Makefile + #rm -rf config.info rm -f TAGS $(MAKE) clean -C AST $(MAKE) clean -C sat/core @@ -117,7 +117,6 @@ regressbigarray: .PHONY: regressall regressall: - $(MAKE) install $(MAKE) regress GRIND_LOG = `date +%Y-%m-%d`"-grind.log" diff --git a/bin/run_tests b/bin/run_tests index 40490af..5571e65 100755 --- a/bin/run_tests +++ b/bin/run_tests @@ -84,7 +84,7 @@ my %optionsDefault = ("level" => 4, my %options = (); # The list of testcases to run # -my @testcases = "bigarray-test"; +my @testcases = "sample-tests"; # Temporary array for STP options my @stpOptions = (); # State is either "own" or "stp", meaning that we're reading either diff --git a/sample-tests/egt-1899.cvc b/sample-tests/egt-1899.cvc new file mode 100644 index 0000000..2cb952a --- /dev/null +++ b/sample-tests/egt-1899.cvc @@ -0,0 +1,217 @@ +%% Regression level = 2 +%% Result = Valid +%% Language = presentation +%START---------------------------------- +packet: ARRAY BITVECTOR(32) OF BITVECTOR(8); +%---------------------------------------------------- +ASSERT ((0bin000000000000000000000000 @ packet[0bin00000000000000000000000011110000]) + = 0bin00000000000000000000000000110101); +ASSERT NOT NOT ((0bin000000000000000000000000 @ + 0bin00000000) = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000000011100])); +ASSERT NOT ((0bin000000000000000000000000 @ + 0bin00000000) = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000000011101])); +ASSERT ((0bin000000000000000000000000 @ packet[0bin00000000000000000000000011110010]) + = 0bin00000000000000000000000000000001); +ASSERT NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110010, + (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]))]) + = 0bin00000000000000000000000000110010); +ASSERT NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110010, + (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]))]) + = 0bin00000000000000000000000000000000); +ASSERT NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110010, + (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]))]) + = 0bin00000000000000000000000000110100); +ASSERT NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110010, + (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]))]) + = 0bin00000000000000000000000011111111); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT SBVLE(0bin00000000000000000000000100110100 + ,BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, + BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), + BVPLUS(32, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]), + 0bin00000000000000000000000000000010)))); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110100, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]))]) + = 0bin00000000000000000000000000110010)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110100, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]))]) + = 0bin00000000000000000000000000000000)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT SBVLE(0bin00000000000000000000000100110100 + ,BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, + BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), + BVPLUS(32, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]), + 0bin00000000000000000000000000000010)), + 0bin00000000000000000000000000000001))); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110101, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]))]) + = 0bin00000000000000000000000000110010)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110101, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]))]) + = 0bin00000000000000000000000000000000)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110101, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]))]) + = 0bin00000000000000000000000000110100)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110101, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]))]) + = 0bin00000000000000000000000011111111)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)])) + IN (BVLE(0bin00000000000000000000000000000000 + ,cvcl_1) AND BVLE(cvcl_1,0bin00000000000000000000001000100011))); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN NOT SBVLE(0bin00000000000000000000000100110100 + ,BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, + BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), + BVPLUS(32, cvcl_1, 0bin00000000000000000000000000000010)), + 0bin00000000000000000000000000000001), + BVPLUS(32, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]), + 0bin00000000000000000000000000000010)))); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110111, + cvcl_0, cvcl_1, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]))]) + = 0bin00000000000000000000000000110010)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011110111, + cvcl_0, cvcl_1, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]))]) + = 0bin00000000000000000000000000000000)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN NOT SBVLE(0bin00000000000000000000000100110100 + ,BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, + BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), + BVPLUS(32, cvcl_1, 0bin00000000000000000000000000000010)), + 0bin00000000000000000000000000000001), + BVPLUS(32, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]), + 0bin00000000000000000000000000000010)), + 0bin00000000000000000000000000000001))); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011111000, + cvcl_0, cvcl_1, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]))]) + = 0bin00000000000000000000000000110010)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN NOT ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011111000, + cvcl_0, cvcl_1, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]))]) + = 0bin00000000000000000000000000000000)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN ((0bin000000000000000000000000 @ + packet[BVPLUS(32, 0bin00000000000000000000000011111000, + cvcl_0, cvcl_1, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]))]) + = 0bin00000000000000000000000000110100)); +ASSERT (LET cvcl_0 = (0bin000000000000000000000000 + @ packet[0bin00000000000000000000000011110001]), + cvcl_1 = (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110011, + cvcl_0)]) + IN SBVLE(0bin00000000000000000000000100110100 + ,BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, BVPLUS(32, 0bin00000000000000000000000000000000, + BVPLUS(32, cvcl_0, 0bin00000000000000000000000000000010)), + BVPLUS(32, cvcl_1, 0bin00000000000000000000000000000010)), + 0bin00000000000000000000000000000001), + BVPLUS(32, (0bin000000000000000000000000 + @ packet[BVPLUS(32, 0bin00000000000000000000000011110110, + cvcl_0, cvcl_1)]), + 0bin00000000000000000000000000000010)), + 0bin00000000000000000000000000000001), + 0bin00000000000000000000000000000001), + (0bin000000000000000000000000 + @ 0bin00000000)))); +QUERY NOT ((0bin000000000000000000000000 @ + packet[0bin00000000000000000000000011110000]) + = 0bin00000000000000000000000000110100); +%END------------------------------------ -- 2.47.3