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)