(theory Ints :written_by {Cesare Tinelli} :date {08/04/05} :updated {30/01/09} :history { 30/01/09 removed erroneous :assoc attribute for binary minus 28/10/09 Slight changes to the ':notes' attribute } :sorts (Int) :notes "The (unsupported) annotations of the function/predicate symbols have the following meaning: attribute | possible value | meaning ------------------------------------------------------- :assoc // the symbol is associative :comm // the symbol is commutative :unit a constant c c is the symbol's left and right unit :trans // the symbol is transitive :refl // the symbol is reflexive :irref // the symbol is irreflexive :antisym // the symbol is antisymmetric " :funs ((0 Int) (1 Int) (~ Int Int) ; unary minus (- Int Int Int) ; binary minus (+ Int Int Int :assoc :comm :unit {0}) (* Int Int Int :assoc :comm :unit {1}) ) :preds ((<= Int Int :refl :trans :antisym) (< Int Int :trans :irref) (>= Int Int :refl :trans :antisym) (> Int Int :trans :irref) ) :definition "This is the first-order theory of the integers, that is, the set of all the first-order sentences over the given signature that are true in the structure of the integer numbers interpreting the signature's symbols in the obvious way (with ~ denoting the negation and - the subtraction functions). " :notes "Note that this theory is not (recursively) axiomatizable in a first-order logic such as SMT-LIB's underlying logic. That is why the theory is defined semantically. " )