形式化9：EUF理论

理论"/>

形式化9：EUF理论

EUF理论

EUF理论是Theory of Equality and Uninterpreted Functions的简写，即等式理论及未解释函数

等式理论

定义

E : : = x ∣ c ( x 是变量集合， c 是常量集合 ) R : : = E = E ∣ E ! = E ( 关系仅包含等和不等 ) P : : = R ∣ P ∧ P \begin{align} E::=&x|c\ (x是变量集合，c是常量集合) \\ R::=&E=E | E!=E \ (关系仅包含等和不等) \\ P::=&R \\ |& P \land P \end{align} E::=R::=P::=∣​x∣c (x是变量集合，c是常量集合)E=E∣E!=E (关系仅包含等和不等)RP∧P​​

示例

例如：a=b /\ b=c /\ d=e /\ b=s /\ d=t /\ a!=e /\ a!=s，用z3来描述就是

S = DeclareSort('S')
a, b, c, d, e, s, t = Consts('a b c d e s t', S)
solve(a == b, b == c, d == e, b == s, d == t, a != e, a != s)

• 解决等式理论

由于等式理论仅有等域不等，因此根据命题对变量进行归类，步骤如下

1. a=b: 将a,b添加到同一个集合 【ab】
2. b=c: 将c添加到b的集合中【abc】
3. …
   
4. a!=e: a与e不在一个集合中
5. a!=s: a与s在一个集合中，产生冲突，因此得到UNSAT

decideEquality(){ for(each "x=y"){ setx = find(x); sety = find(y); union(setx, sety);}for(each "x!=y"){ setx = find(x); sety = find(y); if(setx == sety) return UNSAT;} return SAT;
}

上述算法在数据量较大时会非常低效，因此可使用并查集进行优化：

带有未解释函数的等式理论

定义

E : : = x ∣ c ∣ f ( E , . . . , E ) ( 可判断函数与常 / 变量的相等关系 ) R : : = E = E ∣ E ! = E P : : = R ∣ P ∧ P \begin{align} E::=&x|c|f(E,...,E)\ (可判断函数与常/变量的相等关系)\\ R::=&E=E | E!=E \\ P::=&R \\ |& P \land P \end{align} E::=R::=P::=∣​x∣c∣f(E,...,E) (可判断函数与常/变量的相等关系)E=E∣E!=ERP∧P​​

一致性规则（Congruence rule）

e 1 = e 1 ′ e 2 = e 2 ′ . . . e n = e n ′ f ( e 1 , . . . , e n ) = f ( e 1 ′ , . . . , e n ′ ) ( C o n g r u e n c e ) \cfrac{e1=e1'\quad e2=e2'\quad ... \quad en=en' }{f(e1,...,en)=f(e1',...,en')}(Congruence) f(e1,...,en)=f(e1′,...,en′)e1=e1′e2=e2′...en=en′​(Congruence)

也就是说参数相等，函数的结果也相等

示例

例如：a=b /\ b=c /\ d=e /\ b=s /\ d=t /\ f(a,g(d))!=f(b,g(e))，用z3来描述就是

S = DeclareSort('S')
f = Function('f', S, S, S) # (S,S)->S
g = Function('g', S, S)    # (S)->S
a, b, c, d, e, s, t = Consts('a b c d e s t', S)
solve(a == b, b == c, d == e, b == s, d == t,f(a, g(d)) != f(b, g(e)))

• 解决带有未解释函数的等式理论

1. 列出所有的元素，包含未解释函数中的子项【a,b,...,t,g(d),g(e),f(a,g(d)),f(b,g(e))】
2. 执行同上
3. 由一致性规则可知：由于d=e，因此g(d)=d(e)
   
4. 由于a=b，g(d)=g(e)，因此f(a,g(d))=f(b,g(e))
   
5. 但是前提中指出f(a,g(d))!=f(b,g(e))，因此无解（UNSAT）

应用

• 下面的两段代码是等价的，请进行证明

int power3(int in) {int out_a = in;for (int i = 0; i < 2; ++i)out_a *= in;return out_a;
}int power3_new(int in) {int out_b = (in * in) * in;return out_b;
}

首先对第一段代码进行循环展开：

out_a0 = in;
out_a1 = out_a0 * in;
out_a2 = out_a1 * in;
return out_a2;

这样我们就有了如下的命题(将乘法替换为未解释函数)

P1 ≜ out_a0 = in /\out_a1 = f(out_a0, in) /\out_a2 = f(out_a1, in)
P2 ≜ out_b = f(f(in, in), in)

如果在P1和P2命题的前提下可以推出他们的结果相同就可以证明程序等价：

P1 /\ P2 -> out_a2 = out_b

• 证明下面z1和z2的计算是否等价

z1 = (x1+y1)*(x2+y2);t1 = x1 + y1; 
t2 = x2 + y2;
z2 = t1 * t2;

P1 ≜ z1 = g(f(x1,y1),f(x2,y2))
P2 ≜ t1 = f(x1,y1) /\t2 = f(x2,y2) /\z2 = g(t1,t2)
P1 /\ P2 -> z1 = z2