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.
249 lines
6.4 KiB
249 lines
6.4 KiB
4 years ago
|
(set-option :produce-proofs true)
|
||
|
|
|
||
|
|
(define-fun chr ((x Int)) String
|
||
|
|
(ite (= x 26) "z" (ite (= x 25) "y" (ite (= x 24) "x" (ite (= x 23) "w" (ite (= x 22) "v" (ite (= x 21) "u" (ite (= x 20) "t" (ite (= x 19) "s" (ite (= x 18) "r" (ite (= x 17) "q" (ite (= x 16) "p" (ite (= x 15) "o" (ite (= x 14) "n" (ite (= x 13) "m" (ite (= x 12) "l" (ite (= x 11) "k" (ite (= x 10) "j" (ite (= x 9) "i" (ite (= x 8) "h" (ite (= x 7) "g" (ite (= x 6) "f" (ite (= x 5) "e" (ite (= x 4) "d" (ite (= x 3) "c" (ite (= x 2) "b" (ite (= x 1) "a" "-")))))))))))))))))))))))))))
|
||
|
|
|
||
|
|
(define-fun klinker ((x Int)) Bool
|
||
|
|
(or (= x 1) (= x 5) (= x 9) (= x 15) (= x 21) (= x 25)))
|
||
|
|
|
||
|
|
(define-fun verboden ((x Int)) Bool
|
||
|
|
(or
|
||
|
|
(= x 25)
|
||
|
|
(= x 24)
|
||
|
|
))
|
||
|
|
|
||
|
|
(define-fun ran ((x Int)) Bool
|
||
|
|
(and (<= 0 x) (<= x 44)))
|
||
|
|
|
||
|
|
;
|
||
|
|
;
|
||
|
|
; 3
|
||
|
|
; _4_ 5 _10_
|
||
|
|
; _0_ _1_ 2 6 7 _8_ 9 11 12 _13_
|
||
|
|
;
|
||
|
|
|
||
|
|
(declare-fun letter (Int) Int)
|
||
|
|
(define-fun drie ((x Int) (y Int) (z Int)) Bool
|
||
|
|
(= (letter x) (+ (letter y) (letter z))))
|
||
|
|
|
||
|
|
(assert (forall ((x Int)) (and (>= (letter x) 1) (<= (letter x) 26))))
|
||
|
|
(assert (= (letter 0) 4))
|
||
|
|
(assert (= (letter 1) 5))
|
||
|
|
(assert (drie 3 4 5))
|
||
|
|
(assert (= (letter 4) 13))
|
||
|
|
(assert (drie 4 6 7))
|
||
|
|
(assert (drie 5 7 8))
|
||
|
|
(assert (= (letter 8) 4))
|
||
|
|
(assert (= (letter 10) 23))
|
||
|
|
(assert (drie 10 11 12))
|
||
|
|
(assert (= (letter 13) 4))
|
||
|
|
(assert (= (letter 14) 26))
|
||
|
|
(assert (drie 15 16 17))
|
||
|
|
(assert (= (letter 16) 5))
|
||
|
|
(assert (= (letter 18) 5))
|
||
|
|
(assert (= (letter 19) 14))
|
||
|
|
|
||
|
|
(assert (= (letter 21) 20))
|
||
|
|
(assert (= (letter 24) 14))
|
||
|
|
(assert (drie 21 22 23))
|
||
|
|
(assert (drie 22 24 25))
|
||
|
|
(assert (drie 23 25 26))
|
||
|
|
|
||
|
|
(assert (= (letter 27) 5))
|
||
|
|
(assert (= (letter 28) 5))
|
||
|
|
(assert (= (letter 29) 14))
|
||
|
|
|
||
|
|
(assert (= (letter 38) 4))
|
||
|
|
(assert (drie 30 31 32))
|
||
|
|
(assert (drie 31 33 34))
|
||
|
|
(assert (drie 32 34 35))
|
||
|
|
(assert (drie 33 36 37))
|
||
|
|
(assert (drie 34 37 38))
|
||
|
|
(assert (drie 35 38 39))
|
||
|
|
|
||
|
|
(assert (= (letter 44) 6))
|
||
|
|
(assert (drie 42 43 44))
|
||
|
|
|
||
|
|
(define-fun rk ((x Int)) Bool
|
||
|
|
(and (ran x) (klinker (letter x))))
|
||
|
|
|
||
|
|
(assert (exists ((a1 Int) (a2 Int) (a3 Int) (a4 Int) (a5 Int) (a6 Int) (a7 Int))
|
||
|
|
(and
|
||
|
|
(distinct a1 a2 a3 a4 a5 a6 a7)
|
||
|
|
(rk a1) (rk a2) (rk a3) (rk a4) (rk a5) (rk a6) (rk a7)
|
||
|
|
)))
|
||
|
|
|
||
|
|
; nergens een 'x','y'...
|
||
|
|
(assert (forall ((a Int)) (not (verboden (letter a)))))
|
||
|
|
|
||
|
|
; (a,1),(b,2),(c,3),(d,4),(e,5),(f,6),(g,7),(h,8),(i,9),
|
||
|
|
; (j,10),(k,11),(l,12),(m,13),(n,14),(o,15),(p,16),(q,17),
|
||
|
|
; (r,18),(s,19),(t,20),(u,21),(v,22),(w,23),(x,24),(y,25),(z,26)
|
||
|
|
|
||
|
|
|
||
|
|
; '...mih...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 13)
|
||
|
|
(= (letter (+ a 1)) 9)
|
||
|
|
(= (letter (+ a 2)) 8)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...zmm...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 26)
|
||
|
|
(= (letter (+ a 1)) 13)
|
||
|
|
(= (letter (+ a 2)) 13)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...dzz...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 4)
|
||
|
|
(= (letter (+ a 1)) 26)
|
||
|
|
(= (letter (+ a 2)) 26)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...tpd...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 20)
|
||
|
|
(= (letter (+ a 1)) 16)
|
||
|
|
(= (letter (+ a 2)) 4)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...nzl...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 14)
|
||
|
|
(= (letter (+ a 1)) 26)
|
||
|
|
(= (letter (+ a 2)) 12)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...ggb...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 7)
|
||
|
|
(= (letter (+ a 1)) 7)
|
||
|
|
(= (letter (+ a 2)) 2)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...cff...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 3)
|
||
|
|
(= (letter (+ a 1)) 6)
|
||
|
|
(= (letter (+ a 2)) 6)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...bcd...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 2)
|
||
|
|
(= (letter (+ a 1)) 3)
|
||
|
|
(= (letter (+ a 2)) 4)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; nzn
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 14)
|
||
|
|
(= (letter (+ a 1)) 26)
|
||
|
|
(= (letter (+ a 2)) 14)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; nwh
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 14)
|
||
|
|
(= (letter (+ a 1)) 23)
|
||
|
|
(= (letter (+ a 2)) 8)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; nwm
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 14)
|
||
|
|
(= (letter (+ a 1)) 23)
|
||
|
|
(= (letter (+ a 2)) 13)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; nwk
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 14)
|
||
|
|
(= (letter (+ a 1)) 23)
|
||
|
|
(= (letter (+ a 2)) 11)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; rhj
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 18)
|
||
|
|
(= (letter (+ a 1)) 8)
|
||
|
|
(= (letter (+ a 2)) 10)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; zpj
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 26)
|
||
|
|
(= (letter (+ a 1)) 16)
|
||
|
|
(= (letter (+ a 2)) 10)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; qgj
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 17)
|
||
|
|
(= (letter (+ a 1)) 7)
|
||
|
|
(= (letter (+ a 2)) 10)
|
||
|
|
))))
|
||
|
|
|
||
|
|
; '...umhi...' kan niet
|
||
|
|
(assert (forall ((a Int))
|
||
|
|
(not (and (= (letter (+ a 0)) 21)
|
||
|
|
(= (letter (+ a 1)) 13)
|
||
|
|
(= (letter (+ a 2)) 8)
|
||
|
|
(= (letter (+ a 3)) 9)
|
||
|
|
))))
|
||
|
|
|
||
|
|
(assert (= (letter 11) 9)) ; w_i_nd
|
||
|
|
|
||
|
|
(assert (<= (letter 37) 2)) ; a of b.
|
||
|
|
|
||
|
|
(assert (= (letter 43) 1)) ; g_a_f.
|
||
|
|
|
||
|
|
(check-sat)
|
||
|
|
(get-value ((chr (letter 0))))
|
||
|
|
(get-value ((chr (letter 1))))
|
||
|
|
(get-value ((chr (letter 2))))
|
||
|
|
(get-value ((chr (letter 3))))
|
||
|
|
(get-value ((chr (letter 4))))
|
||
|
|
(get-value ((chr (letter 5))))
|
||
|
|
(get-value ((chr (letter 6))))
|
||
|
|
(get-value ((chr (letter 7))))
|
||
|
|
(get-value ((chr (letter 8))))
|
||
|
|
(get-value ((chr (letter 9))))
|
||
|
|
(get-value ((chr (letter 10))))
|
||
|
|
(get-value ((chr (letter 11))))
|
||
|
|
(get-value ((chr (letter 12))))
|
||
|
|
(get-value ((chr (letter 13))))
|
||
|
|
(get-value ((chr (letter 14))))
|
||
|
|
(get-value ((chr (letter 15))))
|
||
|
|
(get-value ((chr (letter 16))))
|
||
|
|
(get-value ((chr (letter 17))))
|
||
|
|
(get-value ((chr (letter 18))))
|
||
|
|
(get-value ((chr (letter 19))))
|
||
|
|
(get-value ((chr (letter 20))))
|
||
|
|
(get-value ((chr (letter 21))))
|
||
|
|
(get-value ((chr (letter 22))))
|
||
|
|
(get-value ((chr (letter 23))))
|
||
|
|
(get-value ((chr (letter 24))))
|
||
|
|
(get-value ((chr (letter 25))))
|
||
|
|
(get-value ((chr (letter 26))))
|
||
|
|
(get-value ((chr (letter 27))))
|
||
|
|
(get-value ((chr (letter 28))))
|
||
|
|
(get-value ((chr (letter 29))))
|
||
|
|
(get-value ((chr (letter 30))))
|
||
|
|
(get-value ((chr (letter 31))))
|
||
|
|
(get-value ((chr (letter 32))))
|
||
|
|
(get-value ((chr (letter 33))))
|
||
|
|
(get-value ((chr (letter 34))))
|
||
|
|
(get-value ((chr (letter 35))))
|
||
|
|
(get-value ((chr (letter 36))))
|
||
|
|
(get-value ((chr (letter 37))))
|
||
|
|
(get-value ((chr (letter 38))))
|
||
|
|
(get-value ((chr (letter 39))))
|
||
|
|
(get-value ((chr (letter 40))))
|
||
|
|
(get-value ((chr (letter 41))))
|
||
|
|
(get-value ((chr (letter 42))))
|
||
|
|
(get-value ((chr (letter 43))))
|
||
|
|
(get-value ((chr (letter 44))))
|