135 lines
4.5 KiB
Text
135 lines
4.5 KiB
Text
(set-option :produce-proofs true)
|
|
|
|
; Some string
|
|
(declare-const perm String)
|
|
|
|
; of this length
|
|
(assert (= (str.len perm) 152))
|
|
|
|
; with these substrings...
|
|
(assert (str.prefixof "12345" perm))
|
|
(assert (str.contains perm "21345"))
|
|
(assert (str.contains perm "32145"))
|
|
(assert (str.contains perm "23145"))
|
|
(assert (str.contains perm "31245"))
|
|
(assert (str.contains perm "13245"))
|
|
(assert (str.contains perm "43215"))
|
|
(assert (str.contains perm "34215"))
|
|
(assert (str.contains perm "32415"))
|
|
(assert (str.contains perm "42315"))
|
|
(assert (str.contains perm "24315"))
|
|
(assert (str.contains perm "23415"))
|
|
(assert (str.contains perm "41235"))
|
|
(assert (str.contains perm "14235"))
|
|
(assert (str.contains perm "12435"))
|
|
(assert (str.contains perm "42135"))
|
|
(assert (str.contains perm "24135"))
|
|
(assert (str.contains perm "21435"))
|
|
(assert (str.contains perm "41325"))
|
|
(assert (str.contains perm "14325"))
|
|
(assert (str.contains perm "13425"))
|
|
(assert (str.contains perm "43125"))
|
|
(assert (str.contains perm "34125"))
|
|
(assert (str.contains perm "31425"))
|
|
(assert (str.contains perm "54321"))
|
|
(assert (str.contains perm "45321"))
|
|
(assert (str.contains perm "43521"))
|
|
(assert (str.contains perm "43251"))
|
|
(assert (str.contains perm "53421"))
|
|
(assert (str.contains perm "35421"))
|
|
(assert (str.contains perm "34521"))
|
|
(assert (str.contains perm "34251"))
|
|
(assert (str.contains perm "52341"))
|
|
(assert (str.contains perm "25341"))
|
|
(assert (str.contains perm "23541"))
|
|
(assert (str.contains perm "23451"))
|
|
(assert (str.contains perm "53241"))
|
|
(assert (str.contains perm "35241"))
|
|
(assert (str.contains perm "32541"))
|
|
(assert (str.contains perm "32451"))
|
|
(assert (str.contains perm "52431"))
|
|
(assert (str.contains perm "25431"))
|
|
(assert (str.contains perm "24531"))
|
|
(assert (str.contains perm "24351"))
|
|
(assert (str.contains perm "54231"))
|
|
(assert (str.contains perm "45231"))
|
|
(assert (str.contains perm "42531"))
|
|
(assert (str.contains perm "42351"))
|
|
(assert (str.contains perm "51234"))
|
|
(assert (str.contains perm "15234"))
|
|
(assert (str.contains perm "12534"))
|
|
(assert (str.contains perm "12354"))
|
|
(assert (str.contains perm "52134"))
|
|
(assert (str.contains perm "25134"))
|
|
(assert (str.contains perm "21534"))
|
|
(assert (str.contains perm "21354"))
|
|
(assert (str.contains perm "52314"))
|
|
(assert (str.contains perm "25314"))
|
|
(assert (str.contains perm "23514"))
|
|
(assert (str.contains perm "23154"))
|
|
(assert (str.contains perm "51324"))
|
|
(assert (str.contains perm "15324"))
|
|
(assert (str.contains perm "13524"))
|
|
(assert (str.contains perm "13254"))
|
|
(assert (str.contains perm "53124"))
|
|
(assert (str.contains perm "35124"))
|
|
(assert (str.contains perm "31524"))
|
|
(assert (str.contains perm "31254"))
|
|
(assert (str.contains perm "53214"))
|
|
(assert (str.contains perm "35214"))
|
|
(assert (str.contains perm "32514"))
|
|
(assert (str.contains perm "32154"))
|
|
(assert (str.contains perm "51432"))
|
|
(assert (str.contains perm "15432"))
|
|
(assert (str.contains perm "14532"))
|
|
(assert (str.contains perm "14352"))
|
|
(assert (str.contains perm "54132"))
|
|
(assert (str.contains perm "45132"))
|
|
(assert (str.contains perm "41532"))
|
|
(assert (str.contains perm "41352"))
|
|
(assert (str.contains perm "54312"))
|
|
(assert (str.contains perm "45312"))
|
|
(assert (str.contains perm "43512"))
|
|
(assert (str.contains perm "43152"))
|
|
(assert (str.contains perm "51342"))
|
|
(assert (str.contains perm "15342"))
|
|
(assert (str.contains perm "13542"))
|
|
(assert (str.contains perm "13452"))
|
|
(assert (str.contains perm "53142"))
|
|
(assert (str.contains perm "35142"))
|
|
(assert (str.contains perm "31542"))
|
|
(assert (str.contains perm "31452"))
|
|
(assert (str.contains perm "53412"))
|
|
(assert (str.contains perm "35412"))
|
|
(assert (str.contains perm "34512"))
|
|
(assert (str.contains perm "34152"))
|
|
(assert (str.contains perm "51423"))
|
|
(assert (str.contains perm "15423"))
|
|
(assert (str.contains perm "14523"))
|
|
(assert (str.contains perm "14253"))
|
|
(assert (str.contains perm "54123"))
|
|
(assert (str.contains perm "45123"))
|
|
(assert (str.contains perm "41523"))
|
|
(assert (str.contains perm "41253"))
|
|
(assert (str.contains perm "54213"))
|
|
(assert (str.contains perm "45213"))
|
|
(assert (str.contains perm "42513"))
|
|
(assert (str.contains perm "42153"))
|
|
(assert (str.contains perm "51243"))
|
|
(assert (str.contains perm "15243"))
|
|
(assert (str.contains perm "12543"))
|
|
(assert (str.contains perm "12453"))
|
|
(assert (str.contains perm "52143"))
|
|
(assert (str.contains perm "25143"))
|
|
(assert (str.contains perm "21543"))
|
|
(assert (str.contains perm "21453"))
|
|
(assert (str.contains perm "52413"))
|
|
(assert (str.contains perm "25413"))
|
|
(assert (str.contains perm "24513"))
|
|
(assert (str.contains perm "24153"))
|
|
|
|
; Does it exist?
|
|
(check-sat)
|
|
|
|
;(get-model)
|
|
(get-proof)
|