Z3'te toUpperCase işlevi nasıl eklenir?

Question

Aşağıdaki kodu Z3'te denedim. Ama Z3 modelin mevcut olmadığını söyledi.

(declare-const s String) 
(declare-fun toUppercase (String) (String)) 

(assert (= (str.len s) (str.len (toUppercase s)))) 
(assert (forall ((i Int) (x String)) 
    (let ((a!1 (and (not (= (str.at x i) "a")) 
        (not (= (str.at x i) "b")) 
        (not (= (str.at x i) "c")) 
        (not (= (str.at x i) "d")) 
        (not (= (str.at x i) "e")) 
        (not (= (str.at x i) "f")) 
        (not (= (str.at x i) "g")) 
        (not (= (str.at x i) "h")) 
        (not (= (str.at x i) "i")) 
        (not (= (str.at x i) "j")) 
        (not (= (str.at x i) "k")) 
        (not (= (str.at x i) "l")) 
        (not (= (str.at x i) "m")) 
        (not (= (str.at x i) "n")) 
        (not (= (str.at x i) "o")) 
        (not (= (str.at x i) "p")) 
        (not (= (str.at x i) "q")) 
        (not (= (str.at x i) "r")) 
        (not (= (str.at x i) "s")) 
        (not (= (str.at x i) "t")) 
        (not (= (str.at x i) "u")) 
        (not (= (str.at x i) "v")) 
        (not (= (str.at x i) "w")) 
        (not (= (str.at x i) "x")) 
        (not (= (str.at x i) "y")) 
        (not (= (str.at x i) "z")) 
        (= (str.at x i) (str.at (toUppercase x) i))))) 
    (let ((a!2 (or (and (= (str.at x i) "a") (= (str.at (toUppercase x) i) "A")) 
       (and (= (str.at x i) "b") (= (str.at (toUppercase x) i) "B")) 
       (and (= (str.at x i) "c") (= (str.at (toUppercase x) i) "C")) 
       (and (= (str.at x i) "d") (= (str.at (toUppercase x) i) "D")) 
       (and (= (str.at x i) "e") (= (str.at (toUppercase x) i) "E")) 
       (and (= (str.at x i) "f") (= (str.at (toUppercase x) i) "F")) 
       (and (= (str.at x i) "g") (= (str.at (toUppercase x) i) "G")) 
       (and (= (str.at x i) "h") (= (str.at (toUppercase x) i) "H")) 
       (and (= (str.at x i) "i") (= (str.at (toUppercase x) i) "I")) 
       (and (= (str.at x i) "j") (= (str.at (toUppercase x) i) "J")) 
       (and (= (str.at x i) "k") (= (str.at (toUppercase x) i) "K")) 
       (and (= (str.at x i) "l") (= (str.at (toUppercase x) i) "L")) 
       (and (= (str.at x i) "m") (= (str.at (toUppercase x) i) "M")) 
       (and (= (str.at x i) "n") (= (str.at (toUppercase x) i) "N")) 
       (and (= (str.at x i) "o") (= (str.at (toUppercase x) i) "O")) 
       (and (= (str.at x i) "p") (= (str.at (toUppercase x) i) "P")) 
       (and (= (str.at x i) "q") (= (str.at (toUppercase x) i) "Q")) 
       (and (= (str.at x i) "r") (= (str.at (toUppercase x) i) "R")) 
       (and (= (str.at x i) "s") (= (str.at (toUppercase x) i) "S")) 
       (and (= (str.at x i) "t") (= (str.at (toUppercase x) i) "T")) 
       (and (= (str.at x i) "u") (= (str.at (toUppercase x) i) "U")) 
       (and (= (str.at x i) "v") (= (str.at (toUppercase x) i) "V")) 
       (and (= (str.at x i) "w") (= (str.at (toUppercase x) i) "W")) 
       (and (= (str.at x i) "x") (= (str.at (toUppercase x) i) "X")) 
       (and (= (str.at x i) "y") (= (str.at (toUppercase x) i) "Y")) 
       (and (= (str.at x i) "z") (= (str.at (toUppercase x) i) "Z")) 
       a!1))) 
    (=> (and (>= i 0) (< i (str.len x))) a!2))))) 
(assert (str.prefixof "hE" s)) 

(check-sat) 
(get-model) 

Belki büyük harfli tüm küçük harf karakterlerini değiştirmek için replaceAll işlevini uygulayabileceğimi düşünüyordum. Ama replaceAll işlevini de kullanamıyorum.

Bu tanımlar-fun-rec kullanarak benim ilk denemede:

(set-option :smt.mbqi true) 
(define-fun-rec replaceAll ((x!1 String) (x!2 String) (x!3 String)) (String) 
    (let ((I (str.indexof x!1 x!2))) 
    (if (= I -1) x!1 
     (replaceAll (str.replace x!1 x!2 x!3) x!2 x!3) 
    ) 
) 
) 
(declare-const a String) 
(simplify (replaceAll "aba" "a" "A")) 
(assert (= (replaceAll a "a" "A") "Ab")) 

(check-sat) 
(get-model) 
(exit) 

Bu koşullu makro kullanarak 2 denemede:

(declare-fun replaceAll (String String String String) Bool) 

(assert (forall ((x!1 String) (x!2 String) (x!3 String) (x!4 String)) 
       (=> (= -1 (str.indexof x!1 x!2)) (replaceAll x!1 x!2 x!3 x!4)))) 
(assert (forall ((S String) (r String) (T String) (R String)) 
       (=> 
        (>= (str.indexof S r) 0) 
        (exists ((U String) (M String) (S1 String) (R1 String)) 
        (and (= S (str.++ U M S1)) 
         (= R (str.++ U T R1)) 
         (= M r) 
         (= (str.len U) (str.indexof S r)) 
         (replaceAll S1 r T R1)) 
        ) 
       ))) 

(declare-const a String) 
(assert (= a "ab")) 
(assert (replaceAll a "a" "A" "Ab")) 

(check-sat) 
(get-model) 

Sana göstereceğiniz her türlü rehberlik takdir ediyorum. Teşekkür ederim.

Answer 1

Bu, String yordamının kısıtlamaları nasıl doyurduğuyla başa çıkabileceği konuların kapsamı dışında olacaktır. Temel olarak bir dönüştürücü açıklıyorsunuz. Şu anda, transdüserler hakkında, onlar hakkında ortaya çıkan aksiyomlar dışında mantık yürütme konusunda bir destek bulunmamaktadır. Transdüserleri yerel olarak ele alan ve etrafında çözmeyi kısıtlayan araçlar vardır. Örneğin Bek/Bex araçları (http://rise4fun.com/bex, http://rise4fun.com/bek) ve automata araç takımı (http://research.microsoft.com/~margus, https://github.com/AutomataDotNet/Automata).