diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 05:52:21 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 05:52:21 +0000 |
commit | 41fc06dc6352a847f047970e63e46455eb4dd050 (patch) | |
tree | 92f08943a4782f24f0cb44935d612b400a612592 /test | |
parent | b122cec27ca27d0b48e786191448e0053be78ed0 (diff) |
First chunk of boolean-terms support.
Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.
This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 7 | ||||
-rw-r--r-- | test/regress/regress0/bug217.smt2 (renamed from test/regress/regress0/uf/bug217.smt2) | 6 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output1.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output2.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output1.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output2.smt2 | 14 | ||||
-rwxr-xr-x | test/regress/run_regression | 4 |
7 files changed, 100 insertions, 5 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 4789b0a55..6af6fbf70 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -49,7 +49,11 @@ SMT2_TESTS = \ simple-uf.smt2 \ simplification_bug4.smt2 \ parallel-let.smt2 \ - get-value-incremental.smt2 + get-value-incremental.smt2 \ + hung13sdk_output1.smt2 \ + hung10_itesdk_output2.smt2 \ + hung10_itesdk_output1.smt2 \ + hung13sdk_output2.smt2 # Regression tests for PL inputs CVC_TESTS = \ @@ -116,6 +120,7 @@ BUG_TESTS = \ bug168.smt \ bug187.smt2 \ bug216.smt2 \ + bug217.smt2 \ bug220.smt2 \ bug239.smt \ bug274.cvc \ diff --git a/test/regress/regress0/uf/bug217.smt2 b/test/regress/regress0/bug217.smt2 index 45f0f3c0c..92b72c87d 100644 --- a/test/regress/regress0/uf/bug217.smt2 +++ b/test/regress/regress0/bug217.smt2 @@ -1,10 +1,12 @@ +; EXPECT: unsat +; EXIT: 20 (set-logic QF_UF) -(set-info :status unsat) +(set-info :status sat) +(set-option :produce-models true) (declare-fun f (Bool) Bool) (declare-fun x () Bool) (declare-fun y () Bool) (declare-fun z () Bool) -;(assert (and x (or (f x) (f y)))) (assert (or (f x) (f y) (f z))) (assert (not (f false))) (assert (not (f true))) diff --git a/test/regress/regress0/hung10_itesdk_output1.smt2 b/test/regress/regress0/hung10_itesdk_output1.smt2 new file mode 100644 index 000000000..8bcdfdfbc --- /dev/null +++ b/test/regress/regress0/hung10_itesdk_output1.smt2 @@ -0,0 +1,30 @@ +( set-logic QF_ALL_SUPPORTED) +( set-info :source | SMT-COMP'06 organizers |) +( set-info :smt-lib-version 2.0) +( set-info :category "check") +( set-info :status sat) +( declare-fun x1 () Bool) +( declare-fun x2 () Real) +( declare-fun x3 () Real) +( declare-fun x4 () Bool) +( declare-fun x5 () Real) +( declare-fun x6 () Real) +( declare-fun x7 () Real) +( declare-fun x8 () Real) +( declare-fun bo1 () Bool) +( declare-fun bo2 () Bool) +( declare-fun bo3 () Bool) +( declare-fun r1 () Real) +( declare-fun r2 () Real) +( declare-fun r3 () Real) +( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool + ( ite ( > a 0.0) b c)) +( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real + ( ite a1 b1 c1)) +( declare-fun f ( Real Bool) Real) +( declare-fun fRealRealReal ( Real Real) Real) +( declare-fun fRealReal ( Real) Real) +( declare-fun fReal () Real) +( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/hung10_itesdk_output2.smt2 b/test/regress/regress0/hung10_itesdk_output2.smt2 new file mode 100644 index 000000000..8bcdfdfbc --- /dev/null +++ b/test/regress/regress0/hung10_itesdk_output2.smt2 @@ -0,0 +1,30 @@ +( set-logic QF_ALL_SUPPORTED) +( set-info :source | SMT-COMP'06 organizers |) +( set-info :smt-lib-version 2.0) +( set-info :category "check") +( set-info :status sat) +( declare-fun x1 () Bool) +( declare-fun x2 () Real) +( declare-fun x3 () Real) +( declare-fun x4 () Bool) +( declare-fun x5 () Real) +( declare-fun x6 () Real) +( declare-fun x7 () Real) +( declare-fun x8 () Real) +( declare-fun bo1 () Bool) +( declare-fun bo2 () Bool) +( declare-fun bo3 () Bool) +( declare-fun r1 () Real) +( declare-fun r2 () Real) +( declare-fun r3 () Real) +( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool + ( ite ( > a 0.0) b c)) +( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real + ( ite a1 b1 c1)) +( declare-fun f ( Real Bool) Real) +( declare-fun fRealRealReal ( Real Real) Real) +( declare-fun fRealReal ( Real) Real) +( declare-fun fReal () Real) +( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/hung13sdk_output1.smt2 b/test/regress/regress0/hung13sdk_output1.smt2 new file mode 100644 index 000000000..bf3ab9a26 --- /dev/null +++ b/test/regress/regress0/hung13sdk_output1.smt2 @@ -0,0 +1,14 @@ +( set-logic QF_ALL_SUPPORTED) +( set-info :source | SMT-COMP'06 organizers |) +( set-info :smt-lib-version 2.0) +( set-info :category "check") +( set-info :status sat) +( declare-fun x1 () Bool) +( declare-fun x2 () Real) +( declare-fun x3 () Real) +( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real + ( ite a1 b1 c1)) +( declare-fun fReal () Real) +( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/hung13sdk_output2.smt2 b/test/regress/regress0/hung13sdk_output2.smt2 new file mode 100644 index 000000000..bf3ab9a26 --- /dev/null +++ b/test/regress/regress0/hung13sdk_output2.smt2 @@ -0,0 +1,14 @@ +( set-logic QF_ALL_SUPPORTED) +( set-info :source | SMT-COMP'06 organizers |) +( set-info :smt-lib-version 2.0) +( set-info :category "check") +( set-info :status sat) +( declare-fun x1 () Bool) +( declare-fun x2 () Real) +( declare-fun x3 () Real) +( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real + ( ite a1 b1 c1)) +( declare-fun fReal () Real) +( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3)))) +(check-sat) +(exit) diff --git a/test/regress/run_regression b/test/regress/run_regression index 9333cdb8c..68c1e0677 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -121,12 +121,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi benchmark=$tmpbenchmark - elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev/null; then + elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then expected_proof= expected_output=sat expected_exit_status=10 command_line= - elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev/null; then + elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then expected_proof= expected_output=unsat expected_exit_status=20 |