Analysieren und Speichern von Ausdruck mit Array

Question

Ich habe zwei arithmetische Ganzzahlausdrücke mit Array in einer Datei. Was ist der beste Weg, um jeden Ausdruck im Speicher zu speichern? so dass die äquivalente Formel syntaktisch äquivalent wird. Vergleichen wir die Struktur, können wir die Äquivalenz finden. Um die Äquivalenz zu prüfen, vergleichen Sie zuerst ihre Struktur, wenn sie gleich sind, dann sind sie äquivalent, ansonsten verwenden Sie den SMT-Löser.

Ex. a [i + 2] +5 und a [i + 3-1] + 4 + 1 sind äquivalent.

Zur Zeit stelle ich a [i] = b [i] + z wie wr (a, i, rd (b, i) + z) dar. Wo Write (wr) und Read (rd) Funktionen sind.

Answer 1

Es ist ein bisschen schwer zu verstehen, was Sie fragen. Aber die Theorie von Arrays unterstützt bereits Lese-/Schreiboperationen. Die Gleichheit Sie als Beispiel hinstellen kann wie folgt codiert werden:

(set-logic AUFLIA) 

(declare-const i Int) 
(declare-const a (Array Int Int)) 

(define-fun eq() Bool (= (+ (select a (+ i 2))  5) 
          (+ (select a (+ i (- 3 1))) (+ 4 1)))) 

; To prove equivalence, assert the negation and make sure the result is unsat: 
(assert (not eq)) 

(check-sat) 

Dies unsat führen, die beweist, dass die Gleichheit für alle Arrays a wahr ist. (Beachten Sie, dass wir die Negation der Gleichheit bestätigen.)

Sind Sie das?