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.

59 lines 1.5 KiB Raw Permalink Blame History

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