[SMT-LIB] A few general SMTLIB questions

[cok at frontiernet.net]

Some others have already contributed answers, but since I wrote the tutorial I'll chime in.

----- "Delcypher" <delcypher at gmail.com> 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?
> 

Martin Brain had a good answer here (and for #2). In addition, one may also assert some axioms about uninterpreted functions that limit their behavior.


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

I was told by another source that QF_ABV was a renaming of QF_AUFBV, but was confusing and was dropped.
Just use 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

You are right. They should start with # - the leading 0 is old syntax.

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

The second sentence was just meant as an example of the first, but I'll adjust to clarify.

Thanks for the feedback - any other feedback is welcome as well.

- David Cok

> 
> Regards,
> Dan Liew.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib