1

我正在使用 z3 进行等价检查。我尝试使用 z3 horn solver 来加速 z3 求解时间，我遇到了以下问题：

我想检查两个程序是否相同。两个程序的逻辑是 P1：a2 = a1 + 2，其中 a1 是输入，a2 是输出 P2：b2 = b1 + 2，其中 b1 是输入，b2 是输出 a1、a2、b1 的类型， b2 是位向量 64。公式是 forall (a1, b1), (a1 == b1) && (a2 == a1 + 2) && (b2 == b1 + 2) => (a2 == b2)

如果我使用 bv 求解器，结果是sat. 但是，如果我使用喇叭求解器，求解结果是unknown，原因是

unknown
Uninterpreted 'a2' in <null>:
query!0(#1,#0) :- 
 (= a2 (bvadd (:var 1) #x0000000000000002)),
 (not (= a2 b2)),
 (= b2 (bvadd (:var 0) #x0000000000000002)),
 (= (:var 1) (:var 0)).

为什么这两个求解器有不同的结果？以及为什么喇叭求解器的结果是未知的？

这是源代码：

#include "z3++.h"
using namespace std;

int main() {
  z3::context ctx;
  z3::expr a1 = ctx.bv_const("a1", 64);
  z3::expr a2 = ctx.bv_const("a2", 64);
  z3::expr b1 = ctx.bv_const("b1", 64);
  z3::expr b2 = ctx.bv_const("b2", 64);

  z3::expr p1 = (a2 == a1 + 2);
  z3::expr p2 = (b2 == b1 + 2);
  z3::expr p_same_input = (a1 == b1);
  z3::expr p_post = (a2 == b2);
  z3::expr f = z3::implies(p_same_input && p1 && p2, p_post);

  z3::expr smt = z3::forall(a1, b1, f);
  z3::solver s(ctx, "HORN");  // set the solver as a horn solver
  s.add(smt);
  cout << s.check() << endl;
  cout << s.reason_unknown() << endl;
}
4

0 回答 0