Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
improve quantifier elimination for arithmetic
This update changes the handling of mod and adds support for nested div terms. Simple use cases that are handled using small results are given below. ``` (declare-const x Int) (declare-const y Int) (declare-const z Int) (assert (exists ((x Int)) (and (<= y (* 10 x)) (<= (* 10 x) z)))) (apply qe2) (reset) (declare-const y Int) (assert (exists ((x Int)) (and (> x 0) (= (div x 41) y)))) (apply qe2) (reset) (declare-const y Int) (assert (exists ((x Int)) (= (mod x 41) y))) (apply qe2) (reset) ``` The main idea is to introduce definition rows for mod/div terms. Elimination of variables under mod/div is defined by rewriting the variable to multiples of the mod/divisior and remainder. The functionality is disabled in this push.
- Loading branch information