解析和存儲表達式涉及數組

我有兩個整數算術表達式涉及文件中的數組。將每個表達式存儲到內存中的最佳方式是什麼？因此等價公式在語法上等價。比較那裏的結構我們可以找到等價。要檢查等價性，首先比較那裏的結構，如果它們相同，那麼它們是等價的，否則使用SMT解算器。解析和存儲表達式涉及數組

Ex。 a [i + 2] +5和a [i + 3-1] + 4 + 1是等價的。現在我代表一個[i] = b [i] + z就如同wr（a，i，rd（b，i）+ z）。寫（wr）和讀（rd）是函數。

來源

2017-10-06 user2468460

我還沒看過這篇文章，因爲它太貴了。 –

這很難理解你在問什麼。但是陣列理論已經支持讀/寫操作。你放下爲例平等可以被編碼如下：

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

這將導致unsat這證明了平等是所有陣列a如此。（請注意，我們主張否定平等。）

這是你在追求什麼？

來源

2017-10-08 19:04:07

我們可以將這些方程存儲在內存中，使得等效公式在語法上等價。比較那裏的結構我們可以找到等價。 – user2468460

不，一般。沒有明顯的正常形式可以將這些表達式簡化爲可以在結構上相等的情況下進行比較。至少不在SMT解決方案的背景下。 –

是的一般情況下這是不可能的。但是對於其可能的表達式的子集，那麼就不需要每次調用SMT解算器，我也可以節省一些時間。我可以知道如何將數組表達式存儲到內存中嗎？ – user2468460

解析和存儲表達式涉及數組

回答

相關問題