Wie zu TopperCase Funktion in Z3 hinzufügen?

Question

Ich habe den folgenden Code in Z3 versucht. Aber Z3 besagten Modells ist nicht verfügbar.

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

Ich dachte, vielleicht könnte ich eine replaceAll-Funktion implementieren, um alle Kleinbuchstaben durch Großbuchstaben zu ersetzen. Aber ich kann nicht die Funktion replaceAll funktionieren.

Dies ist mein erster Versuch mit define-fun-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) 

Dies ist mein zweiter Versuch mit bedingten Makros:

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

Ich würde jede Führung schätzt Sie bieten können. Vielen Dank.

Answer 1

Dies wird außerhalb des Geltungsbereichs dessen liegen, was die String-Prozedur in Bezug auf die Sättigung von Constraints handhaben kann. Sie beschreiben im Grunde einen Wandler. Es gibt derzeit keine Unterstützung für Überlegungen zu Wandlern, außer dass sie Axiome über sie instanziieren. Es gibt Werkzeuge, die nativ mit Wandlern umgehen und die Umgebung um sie herum regeln. Zum Beispiel die Bek/Bex-Werkzeuge (http://rise4fun.com/bex, http://rise4fun.com/bek) und das Automaten-Toolkit (http://research.microsoft.com/~margus, https://github.com/AutomataDotNet/Automata).