[SMT-LIB] A few general SMTLIB questions

[Kelly Heller]

Hi Dan,

My reply to you comes with a big warning:  the idea of *me* trying to
help out in this case is rather an instance of "the blind leading the
blind."

I seem to be in a similar spot as you.  I am a software programmer
with a (i hope) decent understanding of propositional logic and
predicate logic, but I am having trouble introducing myself properly
to notions of "first order *theories*" and automated proofs.

I will try to answer your question #1 with help from a book on my desk. :)

First, "in my own words": an uninterpreted function seems to mean that
you know what types of inputs the function takes, and you know what
the output type is, but you cannot "see" the body of the function, so
you do not know whether the function computes the cosine, or returns
the square root, or performs the 'ceiling' function, or even whether
it has a hard-coded function body that just always returns the number
1.5 !!  You do not know!  You only know the 'function signature' (in
my own programmer jargon.
http://en.wikipedia.org/wiki/Type_signature).  You know the
'signature' but you know nothing about what the function DOES inside.

>From the book "Decision Procedures" by Kroening and Strichman:

[QUOTE]
Replacing functions with uninterpreted functions in a given formula is
a common technique for making it easier to reason about (e.g. to prove
its validity).  At the same time, this process makes the formula
_weaker_, which means that it can make a valid formula invalid.

...

Uninterpreted functions ... in the context of reasoning and
verification... are mainly used for simplifying proofs.  Under certain
conditions, uninterpreted functions let us reason about systems while
ignoring the semantics of some or all functions, assuming they are not
necessary for the proof.
[/QUOTE]

(quoted from this book: ISBN 3642093442, http://amzn.com/3642093442 )

Currently I cannot answer your other questions, but I can mention
things that have helped me so far.

The above listed book is helpful.  So is "Rigorous Software
Development" (http://amzn.com/0857290177).  Even if software
development is not the main field that you are interested in, I still
recommend the first four chapters of "Rigorous Software Development"
(which is almost half of the book) as a good introduction to first
order theories, such as 'the theory of bitvectors and bitvector
arrays' (QF_ABV).

You might also try posting your questions here:
http://math.stackexchange.com and tagging the questions with one or
more of the tags:

logic
proof-writing
formal-systems

(examples:  http://math.stackexchange.com/questions/tagged/formal-systems )

I wish you luck and success!  (i wish that for me, too!)

All the best,
Kelly


2012/7/25 Delcypher <delcypher at gmail.com>:
> 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.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib