[SMT-LIB] SMT-LIB semantics

[Viktor Kuncak]

I have a few questions about SMT semantics.
I've been looking at

http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf

which I suppose to be the latest version.  My motivation is building
an HOL like notation and ensuring that I have a reasonable translation
into SMT-LIB format.

>From the document I do not get much about specific theories and their
semantics.  Is there a document explaining them?

For example, at some point I was wondering about the uses of modulo
operator %.  Is it general modulo for integers and what is its
semantics?

Right now I am searching for any information on inductively defined
data types.  It seems that none of the SMT-LIB logics use them?  At
one point though I got quite puzzled because I read at

http://combination.cs.uiowa.edu/smtlib/

that AUFLIA stands for "Closed linear formulas over the theory of
integer arrays with FREE sort, function and predicate symbols."  Why
are the function symbols FREE?  Was this supposed to mean
UNINTERPRETED?  To me, FREE would mean that function symbols come from
term algebra, that is, inductively definited data types.  There is a
clear difference between free datatype constructors and uninterpreted
predicates even in quantifier-free case, e.g. f(x)=f(y) would imply
x=y, so if you claim the symbols are free then solvers would be
allowed to make such deduction and that would be unsound wrt.
expectations of someone who things they are uninterpreted.  Is my
terminology wrong (it seems to be the one used in model theory,
though)?

A more specific question is whether CVC3 is expected to have a stable
support for its inductively defined data types through SMT-LIB format.

(P.S. In my version of SMT-LIB write-up several latex citations are unresolved.)

Thanks!

-- 
Viktor Kuncak
http://lara.epfl.ch/~kuncak