(theory Ints

 :smt-lib-version 2.6
 :smt-lib-release "2017-11-24"
 :written-by "Cesare Tinelli"
 :date "2010-04-17"
 :last-updated "2015-04-25"
 :update-history
 "Note: history only accounts for content changes, not release changes.
  2015-04-25 Updated to Version 2.5.
 "
 
 :sorts ((Int 0))

 :funs ((NUMERAL Int) 
        (- Int Int)                 ; negation
        (- Int Int Int :left-assoc) ; subtraction
        (+ Int Int Int :left-assoc) 
        (* Int Int Int :left-assoc)
        (div Int Int Int :left-assoc)
        (mod Int Int Int)
        (abs Int Int)
        (<= Int Int Bool :chainable)
        (<  Int Int Bool :chainable)
        (>= Int Int Bool :chainable)
        (>  Int Int Bool :chainable)
       )

 :funs_description
 "All ranked function symbols of the form
    ((_ divisible n) Int Bool)
  where n is a positive numeral.
 "

 :values
 "The set of values for the sort Int consists of 
  - all numerals,
  - all terms of the form (- n) where n is a numeral other than 0.
 "

 :definition 
 "For every expanded signature, the instance of Ints with that 
  signature is the theory consisting of all Sigma-models that interpret:

  - the sort Int as the set of all integer numbers, 

  - each numeral as the corresponding natural number,

  - (_ divisible n) as the function mapping to true all and only
    the integers that are divisible by n,

  - abs as the absolute value function,

  - div and mod according to Boute's Euclidean definition [1], that is,
    so as to satify the formula

    (for all ((m Int) (n Int))
      (=> (distinct n 0)
          (let ((q (div m n)) (r (mod m n)))
            (and (= m (+ (* n q) r))
                 (<= 0 r (- (abs n) 1))))))

  - the other function symbols of Ints as expected.

  References:
  [1] Boute, Raymond T. (April 1992). 
      The Euclidean definition of the functions div and mod. 
      ACM Transactions on Programming Languages and Systems (TOPLAS) 
      ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
 "

 :notes
 "Regardless of sign of m, 
  when n is positive, (div m n) is the floor of the rational number m/n;
  when n is negative, (div m n) is the ceiling of m/n.

  This contrasts with alternative but less robust definitions of div and mod
  where (div m n) is 
  - always the integer part of m/n (rounding towards 0), or 
  - always the floor of x/y (rounding towards -infinity).
 "

 :notes
 "See note in the Reals theory declaration about terms of the form (/ t 0).
  The same observation applies here to terms of the form (div t 0) and
  (mod t 0).
 "
)