analyse et stockage d'expression impliquant un tableau

Question

J'ai deux expressions arithmétiques entières impliquant un tableau dans un fichier. Quelle est la meilleure façon de stocker chaque expression en mémoire. de sorte que la formule équivalente devienne syntaxiquement équivalente. En comparant la structure, nous pouvons trouver l'équivalence. Pour vérifier l'équivalence, comparez d'abord la structure si elle est la même que si elle est équivalente, sinon utilisez le solveur SMT.

Ex. a [i + 2] +5 et a [i + 3-1] + 4 + 1 sont équivalents. Actuellement, je représente a [i] = b [i] + z est comme wr (a, i, rd (b, i) + z). Où Write (wr) et Read (rd) sont des fonctions.

Answer 1

Il est un peu difficile de comprendre ce que vous demandez. Mais la théorie des tableaux supporte déjà les opérations de lecture/écriture. L'égalité que vous mettez comme exemple peut être codé comme celui-ci:

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

Cela se traduira par unsat ce qui prouve que l'égalité est vrai pour tous les tableaux a. (Notez que nous affirmons la négation de l'égalité.)

Est-ce ce que vous cherchez?