[SMT-LIB] A few general SMTLIB questions

[Delcypher]

Hi,

I've been spending the last few days getting to grips with the SMTLIB
language by using the very useful tutorial and I have a few questions that
I'm hoping someone on this mailing list can answer.
I'd like to apologise in advance because I don't have a strong background
in formal logic I may mix up some technical terms and get things wrong!


1)The tutorial (page 37) describes that the expression (declare-fun ...)
declares a new function symbol that is wholly uninterpreted. What is meant
by a uninterpreted or interpreted symbol? Could you give a simple example
of each?

2) The SMTLIB languages allows be to declare a new function symbol that
takes arguments. For example

;begin
(set-logic QF_UFLIA)
(declare-fun pox (Int) Bool)
(assert (= (pox 7) true))
(assert (= (pox 8) false))
(check-sat)
(get-value (pox))
;end

I'm wondering what the purpose of this is. The only thing I can think of is
that there might be a function whose output you know (what I have asserted)
and you'd like to know what that function is.
In the above example the assertions can be satisfied but the solver will
not show me a possible definition of the function "pox" (which is what I
was expecting). Instead it tells me the value of pox is pox.

3) I'm working on currently I am going to be using either the QF_AUFBV or
the QF_ABV logic. However I do not understand the difference between the
two. The description of QF_AUFBV is

"Closed quantifier-free formulas built over an arbitrary expansion of
the Fixed_Size_BitVectors
and ArraysEx signatures with
free sort and function symbols, but with the restriction that all array
terms have sort of the
form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0. "

The key difference between QF_AUFBV and QF_ABV is the "with free sort and
function symbols". My problem is that I don't understand what that means (I
think the UF stands for uninterpreted function so it may be related to my
earlier questions).
Could anyone explain what this means possibly with a few examples
illustrating the difference?

4) This isn't a question but I noticed a mistakes (at least I think they
are) in the SMTLIB tutorial that should probably be corrected at some point.
- In the table of tokens (table3.1 on page 19) for token types <binary> and
<hex> the example does not match the regular expression .e.g For binary the
regex is #b[01]+ but one of examples is 0b0
- In section 3.9.11 (Options) the following sentence appears

"Setting and retrieving option values is independent of the assertion
stack. The setting of an option is not changed by a pop command."

Surely is retrieving option values is independent of the assertion stack
then the setting of an option is also not changed by the "push" command as
well?

Regards,
Dan Liew.