## Reals_Ints

```(theory Reals_Ints

:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written_by "Cesare Tinelli"
:date "2010-04-17"
:last-updated "2017-11-24"
:update-history
"Note: history only accounts for content changes, not release changes.
2017-11-24 Added abstract values for irrational numbers to set of Real values,
consistently with the Reals theory (the omission of such values
was an oversight).
2015-04-25 Updated to Version 2.5.
"

:sorts ((Int 0) (Real 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)
(DECIMAL Real)
(- Real Real)                  ; negation
(- Real Real Real :left-assoc) ; subtraction
(+ Real Real Real :left-assoc)
(* Real Real Real :left-assoc)
(/ Real Real Real :left-assoc)
(<= Real Real Bool :chainable)
(<  Real Real Bool :chainable)
(>= Real Real Bool :chainable)
(>  Real Real Bool :chainable)
(to_real Int Real)
(to_int Real Int)
(is_int Real Bool)
)

: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.

The set of values for the sort Real consists of
- an abstract value for each irrational algebraic number
- all terms of the form (/ (to_real m) (to_real n)) or
(/ (- (to_real m)) (to_real n)) where
- m is a numeral,
- n is a numeral other than 0,
- as integers, m and n have no common factors besides 1.
"

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

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

- the sort Real as the set of all real numbers,

- each numeral as the corresponding natural number,

- to_real as the standard injection of the integers into the reals,

- the other function symbols with Int arguments as in the theory
declaration Ints,

- each decimal as the corresponding real number,

- to_int as the function that maps each real number r to its integer part,
that is, to the largest integer n that satisfies (<= (to_real n) r)

- is_int as the function that maps to true all and only the reals in the
image of to_real,

- the other function symbols with Real arguments as in the theory
declaration Reals.
"

:notes
"By definition of to_int, (to_int (- 1.3)) is equivalent to (- 2), not
(- 1).
"

:notes
"For each instance T of Reals_Ints, all models of T satisfy the sentence:

(forall ((x Real))
(= (is_int x) (= x (to_real (to_int x)))))
"
)
```
(raw file)