search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.4k stars 1.47k forks source link

[Consolidated] Performance regressions of arith.solver=6 vs. arith.solver=2 #4934

Open muchang opened 3 years ago

muchang commented 3 years ago

QF_S

[627] % time z3release smt.arith.solver=2 small.smt2
unsat

real    0m0.160s
user    0m0.012s
sys 0m0.004s
[628] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[629] % 
[629] % cat small.smt2
(declare-fun a () String)
(assert (< (* (str.len a) (+ (str.indexof a "A" 0) 2)) 0))
(check-sat)
[630] %

Commit: 4db41c0

muchang commented 3 years ago

QF_S

[634] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.125s
user    0m0.031s
sys 0m0.004s
[635] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[636] % cat small.smt2
(declare-fun x () String)
(assert (distinct (str.suffixof "AA" x) (str.prefixof "A" (str.replace x "A" ""))))
(check-sat)
[637] %

Commit: 4db41c0

muchang commented 3 years ago

NRA

[645] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.103s
user    0m0.009s
sys 0m0.006s
[646] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[647] % cat small.smt2
(assert (forall ((a Real)) (exists ((b Real) (c Real)) (or (= (* (/ a 2 b) 2 c) 0) (< a 0)))))
(check-sat)
[648] %

Commit: 4db41c0

muchang commented 3 years ago

UFLIA

[657] % time z3release smt.arith.solver=2 small.smt2
unsat

real    0m0.111s
user    0m0.015s
sys 0m0.004s
[658] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[659] % cat small.smt2
(declare-fun c (Int) Int)
(define-fun ab ((d Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
(define-fun ac ((d Int) (a Int) (b Int)) Int (ab d b (c d)))
(define-fun ad ((d Int) (e Int)) Int e)
(define-fun ae ((d Int) (a Int) (b Int)) Bool (< 0 (ad d b)))
(define-fun af ((d Int)) Bool (forall ((b Int)) (= 0 (/ 0 0))))
(define-fun g ((d Int)) Bool (forall ((a Int)) (distinct a d)))
(define-fun h ((d Int)) Bool (g d))
(define-fun ah ((d Int)) Bool (h d))
(define-fun ai ((d Int)) Bool (af d))
(define-fun aj ((d Int)) Bool (and (ah d) (ai d)))
(assert (forall ((i Int)) (= 0 (c (- i)))))
(assert (exists ((j Int) (l Int) (d Int)) (= (aj d) (= (ae d j (ac d 0 l)) (ae d j l)))))
(check-sat)
[660] %

Commit: 4db41c0

muchang commented 3 years ago

QF_SLIA

[696] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.141s
user    0m0.020s
sys 0m0.000s
[697] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[698] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () String)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () String)
(declare-fun k () String)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () String)
(assert (ite h (= e d 0) (and (distinct f "") (str.in_re k (re.++ (str.to_re "_") (re.union (str.to_re "_") (str.to_re "t")))))))
(assert (distinct a (>= 0 e)))
(assert (distinct a (= b g)))
(assert (distinct b g))
(assert (distinct c (str.++ i)))
(check-sat)
[699] %

Commit: 4db41c0

muchang commented 3 years ago

NRA

[721] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.076s
user    0m0.016s
sys 0m0.000s
[722] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[723] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun t3532uscore0 () Real)
(assert (forall ((e Real)) (and (> b c 0) (= (and (<= e t3532uscore0) (>= (- (/ b e) d) 0)) (= a 2)))))
(check-sat)
[724] %

Commit: 4db41c0

muchang commented 3 years ago

LRA

[729] % time z3release smt.arith.solver=2 small.smt2
unknown

real    0m0.128s
user    0m0.017s
sys 0m0.000s
[730] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[731] % cat small.smt2
(assert (forall ((a Real)) (exists ((b Real)) (and (distinct (/ 1 b) 0) (< (+ a b) 0)))))
(check-sat)
[732] %

Commit: 4db41c0

muchang commented 3 years ago

UFLIA

[736] % time z3release smt.arith.solver=2 small.smt2
unsat

real    0m0.101s
user    0m0.011s
sys 0m0.007s
[737] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[738] % cat small.smt2
(declare-fun c (Int) Int)
(define-fun d ((k Int) (a Int)) Int (mod a (c (to_int (/ 9 k)))))
(define-fun e ((k Int)) Int (- (c k) 1))
(define-fun f ((k Int) (l Int)) Bool (and (>= l 0) (<= l (e k))))
(define-fun g ((k Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
(define-fun h ((k Int) (a Int) (b Int)) Int (g k a (c k)))
(define-fun i ((k Int) (l Int)) Int (- (d k l)))
(define-fun intsle ((k Int) (a Int) (b Int)) Bool (<= (i k a) (i k b)))
(define-fun m ((k Int) (l Int)) Bool (f k l))
(assert (exists ((j Int) (k Int)) (not (=> true (m k j) (intsle k j (h k j 0))))))
(check-sat)
[739] %

Commit: 4db41c0

muchang commented 3 years ago

QF_NIRA

[753] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.084s
user    0m0.011s
sys 0m0.004s
[754] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[755] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun f () Int)
(declare-fun e () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(assert (xor (and (xor (and (> b 1) (= (* b (- e)) 1)) (> 1 e)) (<= 0 (+ (* e 5536) (* c g))) (> 36 (div c g))) (= (* f g) 0)))
(assert (distinct a (/ d h) c))
(check-sat)
[756] %

Commit: 4db41c0

muchang commented 3 years ago

QF_NIRA

[762] % time z3release smt.arith.solver=2 small.smt2
unsat

real    0m0.155s
user    0m0.010s
sys 0m0.007s
[763] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[764] % 
[764] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (<= (* a (* a (+ 1 (- a (* a (* a (* a (* a (* a (* a (* a (* a (* a (+ 78 (* a (- 174356582400)))))))))))))))) 0))
(assert (not (<= (* a (* a (mod 1 (to_int (- a (* a (* a (* a (/ a (+ 28800 (* a (* a (- 79001600 a))))))))))))) 1)))
(assert (> a b))
(assert (<= 10 b))
(check-sat)
[765] %

Commit: 4db41c0

muchang commented 3 years ago

NIRA

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun k () Real)
(assert
 (exists ((j Real))
  (xor (= (= (< 0 j) (>= (div (mod (to_int d) (to_int j)) (to_int (+ 5 g))) 4)) (> (- b) 8))
   (>= (- c e) (- (* (mod (to_int (* b i)) (to_int (/ b i))) k) (/ 0 (+ c e)))))))
(assert (= h (mod (to_int a) (to_int d)) (div (to_int f) (to_int f))))
(check-sat)

Commit: 4db41c0

muchang commented 3 years ago

QF_S

[835] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m0.129s
user    0m0.023s
sys 0m0.003s
[836] % timeout -s 9 30 z3release smt.arith.solver=6 small.smt2
Killed
[837] % 
[837] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun jnLrE_new () String)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun f () String)
(declare-fun e () String)
(declare-fun g () String)
(declare-fun i () String)
(assert (= "YY8CBEMy6Q" f))
(assert (= c (= "" (str.substr jnLrE_new 0 0))))
(assert (xor (= a b) (= (str.substr jnLrE_new (+ 115 19) (str.len f)) "YY8CBEMy6Q")))
(assert (= d (= a (= b d))))
(assert (distinct g i))
(assert (distinct (str.substr jnLrE_new (str.len f) (str.len e)) ""))
(check-sat)
[838] %

Commit: 4db41c0

rainoftime commented 3 years ago

QF_NRA

(declare-fun v1 () Bool)
(declare-fun v5 () Bool)
(declare-fun v9 () Bool)
(declare-fun r0 () Real)
(declare-fun r1 () Real)
(declare-fun r2 () Real)
(declare-fun r3 () Real)
(declare-fun r18 () Real)
(push)
(assert (or v9 v5 v1 (= 424362.0 (- r18 73811183.0 73811183.0 424362.0) (* (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r0 r2 r3))) (= r3 (* (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r0 r2 r3)) (* (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r0 r2 r3)) r3 r3) (<= 73811183.0 (* (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r0 r2 r3)) 73811183.0 73811183.0 (* (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r3 r1 r3 73811183.0 (- r3 (* r0 r2 r3))) (* r0 r2 r3)))))
(check-sat)
 time z3 smt.arith.solver=2 delta.out.smt2 timeout=10000
sat

real    0m0.026s
user    0m0.024s
sys     0m0.014s

 time z3 smt.arith.solver=6 delta.out.smt2 timeout=10000
unknown

real    0m10.017s
user    0m11.522s
sys     0m5.002s
rainoftime commented 3 years ago

QF_UFNRA

(declare-fun v3 () Bool)
(declare-fun r0 () Real)
(declare-fun r1 () Real)
(push)
(pop)
(declare-fun r4 () Real)
(declare-fun v69 () Bool)
(assert (or false v69 v3 false))
(assert (or (> 87386 (- 0.082 482 (* r4 (* r0 9647.0 r4 r0 (+ r1 r0 r1 r0))) r0) r4 (* r0 9647.0 (+ r1 r0 r1 r0) r0 (+ 1.0 r0 r1 r0)) 480.0) false))
(check-sat)

time z3 smt.arith.solver=2 delta.out.smt2 timeout=10000
sat

real    0m0.230s
user    0m0.224s
sys     0m0.004s
time z3 smt.arith.solver=6 delta.out.smt2 timeout=10000                                                                                                                               
unknown

real    0m10.013s
user    0m10.008s
sys     0m0.004s
rainoftime commented 3 years ago

QF_S

(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v14 () Bool)
(declare-fun str0 () String)
(declare-fun str1 () String)
(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str5 () String)
(assert (or v14 v3 v2))
(assert (str.prefixof (str.++ str5 str3) (str.++ (str.++ str0 str2) str5 (str.++ str3 str1) "1SX")))
(push)
(check-sat)
(check-sat)
$ time z3 smt.arith.solver=2 delta.out.smt2 timeout=10000
sat
sat

real    0m0.021s
user    0m0.012s
sys     0m0.008s
$ time z3 smt.arith.solver=6 delta.out.smt2 timeout=10000                                                                                                                               
sat
unknown

real    0m10.026s
user    0m10.020s