diff options
Diffstat (limited to 'test/regress/regress0/rewriterules/length.smt2')
-rw-r--r-- | test/regress/regress0/rewriterules/length.smt2 | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2 new file mode 100644 index 000000000..215698ade --- /dev/null +++ b/test/regress/regress0/rewriterules/length.smt2 @@ -0,0 +1,26 @@ +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (forall ((?l list)) (! (=> (= ?l nil) (= (length ?l) 0)) :rewrite-rule))) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) + +;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) + +;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) + + +(assert (not (= (length (cons 1 (cons 2 (cons 3 nil)))) 3))) + +(check-sat) +(exit) |