如何在Z3中添加toUpperCase功能？

Question

我在Z3中試過下面的代碼。但Z3說模型不可用。

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

我在想也許我可以實現一個replaceAll函數來將所有小寫字母替換爲大寫字母。但我無法使replaceAll函數也能正常工作。

這是我第一次嘗試使用定義樂趣-REC：

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

這是我第二次嘗試使用條件的宏：

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

我希望你可以提供任何指導。謝謝。

Answer 1

這將超出String過程可以處理的約束飽和的範圍。 你基本上是描述一個傳感器。目前還不支持推斷換能器，除了實例化它們的公理。 有一些工具可以本地處理換能器，並在其周圍解決約束問題。例如，Bek/Bex工具（http://rise4fun.com/bex,http://rise4fun.com/bek）和自動機工具包（http://research.microsoft.com/~margus,https://github.com/AutomataDotNet/Automata）。