Do not use CVC4's internal SMT-LIB arithmetic functions

On 27 June 2013 16:17, Tim King <taking@cs.nyu.edu> wrote:
> The quick answer is that you likely want to use the kind "INTS_DIVISION".
> This is the smtlib "div" function.  The function "INTS_DIVISION_TOTAL"
> corresponds to the internal integer division function not the smtlib "div"
> function. These are not quite the same functions so INTS_DIVISION_TOTAL and
> INTS_DIVISION should not both be printed as "div".
>
> When y != 0, (INTS_DIVISION_TOTAL x y) and (div x y) are the same function.
> They have different semantics; however, when y = 0. The smtlib standard
> states that div is a function, but it does not interpret (div x 0).
> (Effectively div, mod, /, ... each implicitly define uninterpreted functions
> (div_by_0 x) for all of the terms (div x 0).  So x = 5, y = 6 and (div x 0)
> = 6 imply that (div (div x 0) 0) equals (div y 0).)  INTS_DIVISION_TOTAL
> additionally defines what happens when dividing by 0. What it does right now
> is to evaluate (INTS_DIVISION_TOTAL x 0) to 0 for all x. (Another reasonable
> choice is to always evaluate this to x, which I believe bitvector division
> does.)  What it defines it as is currently at the discretion of the solver.
> One of the reasons we did this is that there is an internal invariant that
> constant theory terms are rewritten (by the internal rewriter) to constants.
> So (div 5 0) doesn't have a value until (div 5 0) is assigned a value and
> does not rewrite to a constant term while (INTS_DIVISION_TOTAL 5 0) can
> rewrite to 0. Internally, CVC4 handles div by expanding (div x y) to
> something like:
>   (ite (= y 0) (div_by_0 x) (INTS_DIVISION_TOTAL x y) )
> where div_by_0 is an uninterpreted int to int function.  Sharing + UF +
> Arith then enforce the correct semantics.
>
> The documentation for this one is actually not that bad. :) From
> build/src/expr/kind.h:
>   INTS_DIVISION, /**< ints division (user symbol) */
>   INTS_DIVISION_TOTAL, /**< ints division with interpreted division by 0
> (internal symbol) */