test/regress/regress1/rewriterules/datatypes_sat.smt2

   1 ; COMMAND-LINE: --rewrite-rules --quiet
   2 ;; try to solve datatypes with rewriterules
   3 (set-logic AUFLIA)
   4 (set-info :status sat)
   5
   6 ;; lists 2 nil
   7 (declare-sort elt 0) ;; we suppose that elt is infinite
   8 (declare-sort list 0)
   9
  10 (declare-fun nil1 () list)
  11 (declare-fun nil2 () list)
  12 (declare-fun cons (elt list) list)
  13
  14 ;;;;;;;;;;;;;;;;;;;;
  15 ;; injective
  16
  17 (declare-fun inj1 (list) elt)
  18 (assert (forall ((?e elt) (?l list))
  19                 (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
  20
  21 (declare-fun inj2 (list) list)
  22 (assert (forall ((?e elt) (?l list))
  23                 (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
  24
  25 ;;;;;;;;;;;;;;;;;;;;
  26 ;; projection
  27
  28 (declare-fun proj1 (list) elt)
  29 (assert (forall ((?e elt) (?l list))
  30                 (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) ))
  31
  32 (declare-fun proj2 (list) list)
  33 (assert (forall ((?e elt) (?l list))
  34                 (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) ))
  35
  36 ;;;;;;;;;;;;;;;;;;;
  37 ;; test
  38 (declare-fun iscons (list) Bool)
  39 (assert (= (iscons nil1) false))
  40 (assert (= (iscons nil2) false))
  41 (assert (forall ((?e elt) (?l list))
  42                 (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
  43
  44 (assert (forall ((?l list))
  45                 (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
  46 (assert (forall ((?l list))
  47                 (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
  48
  49
  50 (declare-fun isnil1 (list) Bool)
  51 (assert (= (isnil1 nil1) true))
  52 (assert (= (isnil1 nil2) false))
  53 (assert (forall ((?e elt) (?l list))
  54                 (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) ))
  55 (assert (forall ((?l list))
  56                 (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) ))
  57
  58 (declare-fun isnil2 (list) Bool)
  59 (assert (= (isnil2 nil1) false))
  60 (assert (= (isnil2 nil2) true))
  61 (assert (forall ((?e elt) (?l list))
  62                 (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) ))
  63 (assert (forall ((?l list))
  64                 (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) ))
  65
  66 ;; distinct
  67 (assert (forall ((?l list))
  68                 (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
  69
  70 (assert (forall ((?l list))
  71                 (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
  72
  73 (assert (forall ((?l list))
  74                 (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) ))
  75
  76
  77 ;;;;;;;;;;;;;;;;;;;
  78 ;; case-split
  79 (assert (forall ((?l list))
  80                 (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
  81 (assert (forall ((?l list))
  82                 (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
  83
  84 ;;;;;;;;;;;;;;;;;;;
  85 ;; finite case-split
  86 (assert (forall ((?l list))
  87                  (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
  88
  89
  90
  91 ;;;;; goal
  92
  93 (declare-fun e () elt)
  94 (declare-fun l1 () list)
  95 (declare-fun l2 () list)
  96
  97
  98 (assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l2) (proj2 l2)))))))
  99
 100 (check-sat)
 101
 102 (exit)