Collections of smt problems
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

(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))))