[SMT-LIB] The "rem" operator

[Morgan Deters]

Hi Dan,

On Mon, Dec 15, 2014 at 6:49 AM, Delcypher <delcypher at gmail.com> wrote:
>
> 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?
>

I can't speak for SMT-LIB, but I would suspect there is no such plan.  CVC4
has no plan to add such an extension.

Please note that you likely can define the function you want in an
SMT-LIB-standard way, perhaps with something like the following which seems
to match the Z3 definition of rem.

  (define-fun rem ((a Int) (b Int)) Int (ite (< b 0) (- (mod a b)) (mod a
b)))

Then it should in principle work in any compliant solver.

Do note that CVC4 is heavily limited in its handling of nonlinear
arithmetic so it's not likely to get you very far.  However, if you only
need integer division (and/or mod/remainder) with constant values as
divisors, then the encoding can be linearized automatically by CVC4 if you
run with the --rewrite-divk option.

Morgan
-- 
Morgan Deters
Senior Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/