CODEWITHSUNDEEP
z3z3-fixedpoint
Qiongwen Xu
Qiongwen Xu

Reputation: 11

why z3 horn solver result is unknown and why this is the unknown reason

I am using z3 to do equivalence check. I try to use z3 horn solver to accelerate z3 solving time, and I met the following problem:

I would like to check whether two programs are the same or not. The logic of two programs is P1: a2 = a1 + 2, where a1 is the input, a2 is the output P2: b2 = b1 + 2, where b1 is the input, b2 is the output Type of a1, a2, b1, b2 is bit-vector 64. The formula is that forall (a1, b1), (a1 == b1) && (a2 == a1 + 2) && (b2 == b1 + 2) => (a2 == b2)

If I use a bv solver, the result is sat. However if I use a horn solver, the solve result is unknown, and the reason is

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

why these two solvers have different results? And why the result of the horn solver is unknown?

Here is the source code:

#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;
}

Upvotes: 1

Views: 166

Answers (0)

Related Questions