Sort representing arrays.
Extractor recognising the const
function of
any array theory.
Extractor recognising the const
function of
any array theory.
Constructor and extractor of lambda expressions, encoded using epsilon terms and quantifiers.
Constructor and extractor of lambda expressions, encoded using
epsilon terms and quantifiers. The body of the expression is
expected to contain free variables _0, _1, ...
corresponding to the variables bound by the lambda.
Extractor recognising the select
function of
any array theory.
Extractor recognising the select
function of
any array theory.
Extractor recognising the store
function of
any array theory.
Extractor recognising the store
function of
any array theory.
Get a unique instance of the array theory with the given index and element sorts.
(Since version ) see corresponding Javadoc for more information.