[SMT-LIB] The "rem" operator

Delcypher delcypher at gmail.com
Mon Dec 15 06:49:39 EST 2014


Hi,

I've been playing around with Z3 recently and I noticed that supports
the "rem" operator which doesn't seem to be part of SMTLIB.

Example:

```
(set-option :produce-models true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun rem_result () Int)
(declare-fun div_result () Int)
(declare-fun mod_result () Int)
(assert (= a 12))
(assert (= b (- 7)))
(assert (= rem_result (rem a b)))
(assert (= mod_result (mod a b)))
(assert (= div_result (div a b)))
(check-sat)
(get-model)
sat
(model
  (define-fun div_result () Int
    (- 1))
  (define-fun mod_result () Int
    5)
  (define-fun rem_result () Int
    (- 5))
  (define-fun b () Int
    (- 7))
  (define-fun a () Int
    12)
)
```

I've noted that CVC4 doesn't support "rem" so I'm guessing it's a Z3
extension. Are there any plans to make it an official part of SMTLIB?

It seems strange that QF_BV has both "bvsmod" and "bvsdiv" but the
logics that use Integers only have "mod". However I'm quite ignorant
of the distinction between "mod" and "rem" but clearly there is a
difference.

I noticed that "div" and "mod" uses the "Euclidean" definition of
division but how about "rem", "bvsmod" and "bvsdiv"? Is there name
given to definition that's used these?

Thanks,
Dan Liew.


More information about the SMT-LIB mailing list