(theory Int_Arrays
:written_by {Cesare Tinelli}
:date {12/04/05}
:updated {30/01/09}
:history {
30/01/09 removed erroneous :assoc attribute for binary minus
}
:sorts (Int Array)
: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})
(select Array Int Int)
(store Array Int Int Array)
)
:preds ((<= Int Int :refl :trans :antisym)
(< Int Int :trans :irref)
(>= Int Int :refl :trans :antisym)
(> Int Int :trans :irref)
)
:definition
"This is a theory of functional arrays without extensionality with integer
indeces and elements.
It can be formally defined as the union of the SMT-LIB theory Int and
the variant of the SMT-LIB theory Arrays under the signature morphism
that maps both the sorts Index and Element of Arrays to the sort Int,
and leaves every other symbol unchanged.
"
:notes
"If for i=1,2, T_i is an SMT-LIB theory with sorts S_i, function symbols F_i,
predicate symbols P_i, and axioms A_i, by \"union\" of T_1 and T_2
we mean the theory T with sorts S_1 U S_2, function symbols F_1 U F_2,
predicate symbols P_1 U P_2, and axioms A_1 U A_2 (where U stands for set
theoretic union).
The theory T is a well-defined SMT-LIB theory whenever S_1, S_2, F_1, F_2,
P_1, P_2 are all pairwise disjoin, as is the case for the component theories
considered here.
"
)