(theory Ints :smt-lib-version 2.0 :written_by "Cesare Tinelli" :date "2010-04-17" :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 / 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). " )