Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

QF_LIA performance issue with mod/div #410

Open
unosalt opened this issue Sep 21, 2022 · 0 comments
Open

QF_LIA performance issue with mod/div #410

unosalt opened this issue Sep 21, 2022 · 0 comments

Comments

@unosalt
Copy link

unosalt commented Sep 21, 2022

Hi, the following input in Yices 2.6.4 seems to take a while compared to Z3 and CVC5. Also, Yices 2.5.0 terminates instantly with sat.

(set-logic QF_LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (not (and (<= (mod b (- 968)) (mod b 53)) (= (mod a 533) (- a b)))))
(assert (not (and (<= (div b 432) (div a 492)) (< (- b b) (mod b (- 554))))))
(check-sat)
(exit)

I tested this on both Windows 10 and Ubuntu 18.04.6.
Are there any options that could possibly improve performance?

Here are some stats from Yices 2.6.4 with the provided input:
(
:num-terms 31
:num-types 4
:total-run-time 812.179
:boolean-variables 62380
:atoms 62379
:clauses 14080
:restarts 23
:clause-db-reduce 61
:clause-db-simplify 0
:decisions 549085
:conflicts 2545836
:theory-conflicts 71951
:boolean-propagations 40119973
:theory-propagations 37910214
:simplex-init-vars 22
:simplex-init-rows 13
:simplex-init-atoms 5
:simplex-vars 260
:simplex-rows 249
:simplex-atoms 62379
:simplex-pivots 61612
:simplex-conflicts 66552
:simplex-interface-lemmas 0
:simplex-integer-vars 40
:simplex-branch-and-bound 61847
:simplex-gomory-cuts 481
:simplex-bound-conflicts 36342
:simplex-bound-recheck-conflicts 6080
:simplex-itest-conflicts 5399
:simplex-itest-bound-conflicts 30943
:simplex-itest-recheck-conflicts 30943
:simplex-gcd-conflicts 0
:simplex-dioph-checks 0
:simplex-dioph-conflicts 0
:simplex-dioph-bound-conflicts 0
:simplex-dioph-recheck-conflicts 0
)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
1 participant