Différents résultats dans Z3 avec le fichier smt2 et OCaml

Question

J'ai ce même problème dans SMT2 et OCaml. Je suis en mesure d'obtenir le résultat unsat en ~ 3 minutes en utilisant le fichier SMT2. Cependant, le même problème dans OCaml est bloqué. S'il vous plaît donnez votre avis.

SMT2 du problème:

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

Même problème dans 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"; 

Answer 1

Ces deux entrées ne sont pas exactement les mêmes que l'un d'eux a les arguments de tous sommateurs dans l'ordre inverse, et ceci a un impact sur la performance car les heuristiques dans le solveur SAT vont dans une trajectoire différente. Nous pouvons convaincre l'API OCaml à présenter les mêmes performances que la version SMT2 en changeant l'ordre des arguments, puis en utilisant la tactique de qfbv, en tant que telle:

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"; 

En aparté pour les autres: Notez que pour résoudre SMT2 problèmes pour la logique appelée "QF_BV", Z3 appliquera la tactique appelée "qfbv". Dans ce cas particulier, nous construisons un solveur pour la logique « QF_BV » mais si nous voulions construire explicitement une tactique, puis

(mk_tactic ctx "QF_BV") 

échouera avec un `argument invalide » exception.

Ces postes suivants peuvent intéresser sur les écarts de performance:

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

Z3 timing variation