[SMT-LIB] Integer division

[Cesare Tinelli]

Hi John,

On Aug 5, 2008, at 6:32 PM, John R Harrison wrote:

>
> Sorry if I missed this somewhere in the documentation. Are division
> and modulus on mathematical integers defined in the SMT-LIB standard?

Not currently. We will be happy to add them if there is a need.
Let me add though that, as always with these matters, the priority of  
such additions to the standard is directly proportional to the  
availability of benchmarks using them.

>
> If so, how are they defined when the two arguments have different
> signs?

Since they are not defined yet, this would be a good time to put  
forward a proposal for their definition, if you have one :)

Cheers,


Cesare



> I saw a message from Clark about the analogous operations on
> bitvectors (bvsdiv, bvsmod) proposing quotients be rounded towards
> zero.
>
> John.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib