diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
tree | dc4b56e27701abd61ebd69675f86a9366d90998f /test | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'test')
8 files changed, 98 insertions, 0 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 08462d51b..8e992c03e 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -38,6 +38,12 @@ TESTS = \ typed_v2l30079.cvc \ typed_v3l20092.cvc \ typed_v5l30069.cvc \ + boolean-terms-datatype.cvc \ + boolean-terms-parametric-datatype-1.cvc \ + boolean-terms-parametric-datatype-2.cvc \ + boolean-terms-tuple.cvc \ + boolean-terms-record.cvc \ + some-boolean-tests.cvc \ v10l40099.cvc \ v2l40025.cvc \ v3l60006.cvc \ @@ -48,6 +54,7 @@ TESTS = \ wrong-sel-simp.cvc FAILING_TESTS = \ + pair-real-bool.smt2 \ datatype-dump.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/datatypes/boolean-terms-datatype.cvc b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc new file mode 100644 index 000000000..490574b35 --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +% EXIT: 10 + +DATATYPE List = + cons(car:BOOLEAN, cdr:List) | nil +END; + +x : List; + +ASSERT x /= nil; + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc new file mode 100644 index 000000000..b667d0bbc --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc @@ -0,0 +1,13 @@ +% EXPECT: sat +% EXIT: 10 + +DATATYPE RightistTree[T] = + node(left:BOOLEAN, right:RightistTree[T]) | + leaf(data:T) +END; + +x : RightistTree[INT]; + +ASSERT x /= leaf(0); + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc new file mode 100644 index 000000000..b667d0bbc --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc @@ -0,0 +1,13 @@ +% EXPECT: sat +% EXIT: 10 + +DATATYPE RightistTree[T] = + node(left:BOOLEAN, right:RightistTree[T]) | + leaf(data:T) +END; + +x : RightistTree[INT]; + +ASSERT x /= leaf(0); + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/boolean-terms-record.cvc b/test/regress/regress0/datatypes/boolean-terms-record.cvc new file mode 100644 index 000000000..ec757d042 --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-record.cvc @@ -0,0 +1,8 @@ +% EXPECT: sat +% EXIT: 10 + +x : [# i:INT, b:BOOLEAN #]; + +ASSERT x /= (# i := 0, b := FALSE #); + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc new file mode 100644 index 000000000..c2d95ce8f --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc @@ -0,0 +1,8 @@ +% EXPECT: sat +% EXIT: 10 + +x : [ INT, BOOLEAN ]; + +ASSERT x /= ( 0, FALSE ); + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2 new file mode 100644 index 000000000..5d028d723 --- /dev/null +++ b/test/regress/regress0/datatypes/pair-real-bool.smt2 @@ -0,0 +1,25 @@ +;(set-option :produce-models true) +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ( + ( RealTree + ( Node + (left RealTree) + (elem Real) + (right RealTree)) + (Leaf) + ) +)) + +(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) + +( declare-fun SumeAndPositiveTree ( RealTree ) (Pair Real Bool) ) + +(declare-fun l1 () RealTree) +(declare-fun l2 () RealTree) +(declare-const result (Pair Real Bool)) +(assert (= l1 (Node l2 5.0 l2))) +(assert (= result (SumeAndPositiveTree l1))) +(assert (= (first result) 5)) +(assert (= (second result) true)) +(check-sat) diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc b/test/regress/regress0/datatypes/some-boolean-tests.cvc new file mode 100644 index 000000000..ac6ef1137 --- /dev/null +++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +% EXIT: 10 +DATATYPE list[T] = cons(car:T, care:BOOLEAN, cdr:list[T]) | nil END; +x : list[REAL]; + +y : [INT,BOOLEAN,INT]; +ASSERT y = (5,TRUE,4); + +ASSERT y.1; + +ASSERT x = cons(1.1,TRUE,nil::list[REAL])::list[REAL]; +CHECKSAT; |