You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
60 lines
1.5 KiB
60 lines
1.5 KiB
5 years ago
|
;(set-option :produce-proofs true)
|
||
|
|
||
|
(define-fun n () Int 4) ; number of symbols
|
||
|
(define-fun len () Int 33) ; length of string
|
||
|
(define-fun len2 () Int 29)
|
||
|
|
||
|
(define-fun ran ((x Int)) Bool
|
||
|
(and (<= 0 x) (< x len)))
|
||
|
|
||
|
(define-fun ran2 ((x Int)) Bool
|
||
|
(and (<= 0 x) (<= x len2)))
|
||
|
|
||
|
(declare-fun perm (Int) Int)
|
||
|
(assert (forall ((x Int))
|
||
|
(and (>= (perm x) 1) (<= (perm x) n))))
|
||
|
|
||
|
(define-fun subWord ((a0 Int) (a1 Int) (a2 Int) (a3 Int)) Bool
|
||
|
(exists ((x Int))
|
||
|
(and (ran2 x)
|
||
|
(= (perm (+ x 0)) a0)
|
||
|
(= (perm (+ x 1)) a1)
|
||
|
(= (perm (+ x 2)) a2)
|
||
|
(= (perm (+ x 3)) a3) )))
|
||
|
|
||
|
;(assert (forall ((x Int)) (not (= (perm x) (perm (+ x 1)))) ))
|
||
|
;(assert (forall ((x Int)) (not (= (perm x) (perm (+ x 2)))) ))
|
||
|
|
||
|
(assert (= 1 (perm 0)))
|
||
|
(assert (= 2 (perm 1)))
|
||
|
(assert (= 3 (perm 2)))
|
||
|
(assert (= 4 (perm 3)))
|
||
|
|
||
|
;(assert (subWord 1 2 3 4 5))
|
||
|
(assert (subWord 1 2 3 4))
|
||
|
(assert (subWord 2 1 3 4))
|
||
|
(assert (subWord 3 2 1 4))
|
||
|
(assert (subWord 2 3 1 4))
|
||
|
(assert (subWord 3 1 2 4))
|
||
|
(assert (subWord 1 3 2 4))
|
||
|
(assert (subWord 4 3 2 1))
|
||
|
(assert (subWord 3 4 2 1))
|
||
|
(assert (subWord 3 2 4 1))
|
||
|
(assert (subWord 4 2 3 1))
|
||
|
(assert (subWord 2 4 3 1))
|
||
|
(assert (subWord 2 3 4 1))
|
||
|
(assert (subWord 4 1 2 3))
|
||
|
(assert (subWord 1 4 2 3))
|
||
|
(assert (subWord 1 2 4 3))
|
||
|
(assert (subWord 4 2 1 3))
|
||
|
(assert (subWord 2 4 1 3))
|
||
|
(assert (subWord 2 1 4 3))
|
||
|
(assert (subWord 4 1 3 2))
|
||
|
(assert (subWord 1 4 3 2))
|
||
|
(assert (subWord 1 3 4 2))
|
||
|
(assert (subWord 4 3 1 2))
|
||
|
(assert (subWord 3 4 1 2))
|
||
|
(assert (subWord 3 1 4 2))
|
||
|
|
||
|
(check-sat)
|