解析和存储表达式涉及数组

我有两个整数算术表达式涉及文件中的数组。将每个表达式存储到内存中的最佳方式是什么？因此等价公式在语法上等价。比较那里的结构我们可以找到等价。要检查等价性，首先比较那里的结构，如果它们相同，那么它们是等价的，否则使用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

解析和存储表达式涉及数组

回答

相关问题