(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.
 "
 )