[SMT-LIB] A few general SMTLIB questions

[Martin Brain]

On Wed, 2012-07-25 at 11:00 +0100, Delcypher wrote:
> 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?

An interpreted function is something that one of the theories "knows"
about (i.e. knows how to interpret), for example '+' or '*' in the
theory of reals.  In programming languages these might be referred to as
"operators" and regarded as a different thing to functions but in
SMT-LIB they are regarded as functions.  Uninterpreted function are
user-defined functions, for example 'f', 'g', etc.  The only thing the
solver 'knows' about these is that if you have two uses to the same
function and the arguments are the same then they must have evaluate to
the same value, i.e.

a = b   =>   f(a) = f(b)

Beyond that, the function can take any value in the codomain (the sort
of things it maps to).  If you want it to have particular properties
then you have to explicitly state them.

> 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))
  ^^^^^^^^^^^^^^^^^^^^^^^^^^
This is an example of stating the desired properties of a symbolic
function.

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

That's not quite how the solver would work as check-sat produces a
model, i.e. an assignment of values for each variable.  It won't give
you a symbolic solution for the function; it won't, for example, say
'pox(x) = x < 7'.

The purpose, well, there are a number of uses.  They are useful for
implementing other theories, for examples, array read can be thought of
as an uninterpreted function (so a read could return any value)
restricted by the 'read over write' axioms.  Another use is in
abstracting out details of actual maps and functions.

> 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?

The key thing that QF_AUFBV adds is uninterpreted functions.  As a
general rule, use the most specific / restricted logic you can.  However
in this case it probably doesn't make much difference as many
implementations of array decision procedures use uninterpreted function
decision procedures.  I'd suggest starting out using QF_ABV and then if
you find things that you need uninterpreted functions to represent then
you can always switch to QF_AUFBV.


> 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

I'll leave this for those with suitable access permissions.

> - 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?

Yes, push is fairly straight forward as it is just adding information.
>From an implementation point of view pop is the hard bit as you have to
undo things.

HTH

Cheers,
 - Martin