[SMT-LIB] SMT-LIB semantics

[Cesare Tinelli]

Hi Viktor,

On Feb 6, 2008, at 8:02 AM, Viktor Kuncak wrote:

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

Yes.

> 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?
>
No theories are defined there. That document is meant to define only  
the general semantics and the syntax of the SMT-LIB format. The  
theories currently supported by SMT-LIB are defined individually in  
the Theories section of the SMT-LIB web site.

For the next version of the format (Version 2.0) we intend to add  
these definitions as an appendix to the format document, for our  
users' convenience.

Incidentally, we are currently discussing Version 2.0 in small work  
group. I hope to be able to present a proposal for it to this list  
for further feedback at the end of the month.


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

Function symbols and operators are defined internally by a theory,  
there are no global SMT-LIB definitions of them. Only logical symbols  
are defined globally.
As far as I remember, none of the currently supported theories uses %  
as an operator, even if it is allowed in the syntax.

If there is a need to have an modulus operator, we will be happy to  
add it to the proper theory, and create a new sublogic as needed. As  
usual, the likelihood that this happens soon is directly proportional  
to the number of benchmarks we receive that use that operator :)


> Right now I am searching for any information on inductively defined
> data types.  It seems that none of the SMT-LIB logics use them?

That is correct. Currently, it is impossible to define inductive data  
types as a theory in SMT-LIB. The problem is simply that IDT's are  
not a theory but an infinite family of ones, parametrized by the  
actual signature of constructor and destructor symbols, and so, as  
things are now, we would need a new theory for each benchmark that  
use a new IDT.

There are plans to extend the format to allow the definition of IDT's  
but that will be after Version 2.0.

Of course, a couple of popular and well established IDTs, such as ML  
style lists for instance, could be added right now. The only reason a  
theory of lists is not in SMT-LIB at the moment is that we do not  
have benchmarks for it.



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

Yes. "Free symbol" is in fact the common terminoly in logic and  
automated reasoning for what formal methods people traditionally have  
called "unintepreted symbols".


> To me, FREE would mean that function symbols come from
> term algebra, that is, inductively definited data types.

That is not quite how "free" is used in the literature, at least the  
literature *I* am familiar with :)

When people want to say what you mean they refer to those symbols as  
"free constructors" not "free symbols".
In truth, I have seen some authors use "free symbol" in your sense,  
but, as far as I can tell, it is not the norm (and is of course  
confusing).


> There is a
> clear difference between free datatype constructors and uninterpreted
> predicates even in quantifier-free case,

Sure.


> 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)?
>
I find this surprising. Which model theory references do you have in  
mind?


> A more specific question is whether CVC3 is expected to have a stable
> support for its inductively defined data types through SMT-LIB format.
>
I guess this is a question for the CVC3 mailing list (cvc- 
users at cs.nyu.edu), not this one :)

At any rate, what do you mean by stable support? CVC3 currently  
allows you to define IDTs using its own input language (or the API).  
I'm sure that if SMT-LIB is extended to allow IDTs, CVC3 will comply.


> (P.S. In my version of SMT-LIB write-up several latex citations are  
> unresolved.)
>
Yes. As embarrassing as it is, Silvio and I never managed to fill in  
all the holes in the document.

The new year's resolution is to write one without holes for Version  
2.0, as well as a tutorial, as a gentler introduction to the SMT-LIB  
format.

Best,


Cesare


> Thanks!
>
> -- 
> Viktor Kuncak
> http://lara.epfl.ch/~kuncak
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib