Different results in Z3 with smt2 file and OCaml

Question

I have this same problem in SMT2 and OCaml. I'm able to get the unsat result in ~3 mins using SMT2 file. However the same problem in OCaml gets stuck. Please advise.

SMT2 of the problem:

(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun y0 () (_ BitVec 32))
(declare-fun y1 () (_ BitVec 32))
(declare-fun y2 () (_ BitVec 32))

(assert (not (=> 
(and (= (bvadd x2 x1 x0) (bvadd y2 y1 y0))
     (= (bvadd x2 (bvmul #x00000002 x1) (bvmul #x00000003 x0)) 
        (bvadd y2 (bvmul #x00000002 y1) (bvmul #x00000003 y0)))
     (= (bvadd x2 (bvmul #x00000003 x1) (bvmul #x00000006 x0))
        (bvadd y2 (bvmul #x00000003 y1) (bvmul #x00000006 y0))))
     (= (bvadd x2 (bvmul #x00000004 x1) (bvmul #x0000000a x0))
        (bvadd y2 (bvmul #x00000004 y1) (bvmul #x0000000a y0))))))
(check-sat)

Same problem in OCaml:

let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (mk_context cfg) in
let bv_sort = BitVector.mk_sort ctx 32 in
let c2 = Expr.mk_numeral_int ctx 2 bv_sort in
let c3 = Expr.mk_numeral_int ctx 3 bv_sort in
let c4 = Expr.mk_numeral_int ctx 4 bv_sort in
let c10 = Expr.mk_numeral_int ctx 10 bv_sort in
let c6 = Expr.mk_numeral_int ctx 6 bv_sort in
let x0 = Expr.mk_const ctx (Symbol.mk_string ctx "x0") bv_sort in
let x1 = Expr.mk_const ctx (Symbol.mk_string ctx "x1") bv_sort in
let x2 = Expr.mk_const ctx (Symbol.mk_string ctx "x2") bv_sort in
let y0 = Expr.mk_const ctx (Symbol.mk_string ctx "y0") bv_sort in
let y1 = Expr.mk_const ctx (Symbol.mk_string ctx "y1") bv_sort in
let y2 = Expr.mk_const ctx (Symbol.mk_string ctx "y2") bv_sort in
let ex1 = mk_add ctx (mk_add ctx x0 x1) x2 in
let ey1 = mk_add ctx (mk_add ctx y0 y1) y2 in
let ex2 = mk_add ctx (mk_add ctx (mk_mul ctx c3 x0) (mk_mul ctx x1 c2)) x2 in
let ey2 = mk_add ctx (mk_add ctx (mk_mul ctx c3 y0) (mk_mul ctx y1 c2)) y2 in
let ex3 = mk_add ctx (mk_add ctx (mk_mul ctx c6 x0) (mk_mul ctx x1 c3)) x2 in
let ey3 = mk_add ctx (mk_add ctx (mk_mul ctx c6 y0) (mk_mul ctx y1 c3)) y2 in
let ex4 = mk_add ctx (mk_add ctx (mk_mul ctx c10 x0) (mk_mul ctx x1 c4)) x2 in
let ey4 = mk_add ctx (mk_add ctx (mk_mul ctx c10 y0) (mk_mul ctx y1 c4)) y2 in
let left = Boolean.mk_and ctx [(mk_eq ctx ex1 ey1);(mk_eq ctx ex2 ey2);(mk_eq ctx ex3 ey3)] in
let right = mk_eq ctx ex4 ey4 in
let valid = Boolean.mk_implies ctx left right in
let sat = Boolean.mk_not ctx valid in

print_endline (Z3.Expr.to_string sat);
let solver = (mk_solver ctx None) in
Solver.add solver [sat];
let q = (check solver []) in
match q with
| SATISFIABLE -> print_endline "sat"
| UNSATISFIABLE -> print_endline "unsat"
| UNKNOWN -> print_endline "unknow";

Could you try to create a bit-vector solver instead of the default solver? Z3 in SMT-LIB2 mode will detect that your problem uses just the QF_BV logic (the logic of pure bit-vector). Depending on which version of ocaml API you use, it is called: 'mk_solver_for_logic ctx "QF_BV"' — Nikolaj Bjorner, Jun 10 '14 at 12:17
The equivalent in new OCaml binding is mk_solver_s ctx "QF_BV". I tried it but no help. — Manjeet Dahiya, Jun 11 '14 at 01:34

score 1 · Answer 1 · edited May 23 '17 at 12:20

Those two inputs are not exactly the same as one of them has the arguments of all adders in reverse order, and this has an impact on the performance because the heuristics in the SAT solver go into a different trajectory. We can convince the OCaml API to exhibit the same performance as the SMT2 version by changing the order of the arguments and then using the qfbv tactic, as such:

let _ =
  let cfg = [("model", "true"); ("proof", "false")] in
  let ctx = (mk_context cfg) in
  let bv_sort = BitVector.mk_sort ctx 32 in
  let c2 = Expr.mk_numeral_int ctx 2 bv_sort in
  let c3 = Expr.mk_numeral_int ctx 3 bv_sort in
  let c4 = Expr.mk_numeral_int ctx 4 bv_sort in
  let c10 = Expr.mk_numeral_int ctx 10 bv_sort in
  let c6 = Expr.mk_numeral_int ctx 6 bv_sort in
  let x0 = Expr.mk_const ctx (Symbol.mk_string ctx "x0") bv_sort in
  let x1 = Expr.mk_const ctx (Symbol.mk_string ctx "x1") bv_sort in
  let x2 = Expr.mk_const ctx (Symbol.mk_string ctx "x2") bv_sort in
  let y0 = Expr.mk_const ctx (Symbol.mk_string ctx "y0") bv_sort in
  let y1 = Expr.mk_const ctx (Symbol.mk_string ctx "y1") bv_sort in
  let y2 = Expr.mk_const ctx (Symbol.mk_string ctx "y2") bv_sort in
  let ex1 = mk_add ctx x2 (mk_add ctx x1 x0) in
  let ey1 = mk_add ctx y2 (mk_add ctx y1 y0) in
  let ex2 = mk_add ctx x2 (mk_add ctx (mk_mul ctx x1 c2) (mk_mul ctx c3 x0)) in
  let ey2 = mk_add ctx y2 (mk_add ctx (mk_mul ctx y1 c2) (mk_mul ctx c3 y0) ) in
  let ex3 = mk_add ctx x2 (mk_add ctx (mk_mul ctx x1 c3) (mk_mul ctx c6 x0)) in
  let ey3 = mk_add ctx y2 (mk_add ctx (mk_mul ctx y1 c3) (mk_mul ctx c6 y0)) in
  let ex4 = mk_add ctx x2 (mk_add ctx (mk_mul ctx x1 c4) (mk_mul ctx c10 x0)) in
  let ey4 = mk_add ctx y2 (mk_add ctx (mk_mul ctx y1 c4) (mk_mul ctx c10 y0)) in
  let left = Boolean.mk_and ctx [(mk_eq ctx ex1 ey1);
                                 (mk_eq ctx ex2 ey2);
                                 (mk_eq ctx ex3 ey3)] in
  let right = mk_eq ctx ex4 ey4 in
  let valid = Boolean.mk_implies ctx left right in
  let sat = Boolean.mk_not ctx valid in  
  print_endline (Z3.Expr.to_string sat);
  let solver = (mk_solver_s ctx "QF_BV") in 
  (add solver [sat]) ;
  let q = (check solver []) in
  match q with
    | SATISFIABLE -> print_endline "sat"
    | UNSATISFIABLE -> print_endline "unsat"
    | UNKNOWN -> print_endline "unknown";

As an aside for others: Note that for solving SMT2 problems for the logic called "QF_BV", Z3 will apply the tactic called "qfbv". In this particular case we are constructing a solver for the logic "QF_BV" but if we wanted to explicitly construct a tactic, then

(mk_tactic ctx "QF_BV")

will fail with an `invalid argument' exception.

These following posts may be of interest regarding the performance discrepancies:

What is the importance of the order of the assertions in Z3?

Z3 timing variation

Different results in Z3 with smt2 file and OCaml

1 Answers1