[SMT-LIB] user defined records

[Tim King]

Hello Amir,

1) Is it possible to make user defined records in SMT-LIB?

Yes in the proposal for v2.6, but not 2.5 (without difficulty+quantifiers).
See the proposal
http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-draft-1.pdf page
61 for an example with a pair datatype.

2) Suppose we have the following SMT-LIB code:
> (declare-sort Pair 2)
> (define-sort PInt () (Pair Int Int))

As far as I know, this creates a sort from the sort "constructor function"
Pair applied to Int and Int to generate a sort term (Pair Int Int). The
Pair function has no semantic attachment via a theory. The result is a sort
[for the sort term] that is uninterpreted. There would then be no way to
distinguish between (Pair Int Int) and say the sort (declare-sort foo 0). This
example is a common point of confusion. See these stackoverflow/cvc4
mailing questions posts for comfort that you are not the first to be
confused and further explanations of what to do:
http://stackoverflow.com/questions/13490937/acessing-elements-of-a-sort-w-multiple-fields
http://stackoverflow.com/questions/12923770/parameterized-sorts
http://cs.nyu.edu/pipermail/cvc-users/2014/000627.html

Best,
Tim

On Tue, Jul 14, 2015 at 11:42 PM, Amirhossein Vakili <avakili at outlook.com>
wrote:

> Hi
>
> I have two questions:
>
> 1) Is it possible to make user defined records in SMT-LIB?
>
> 2) Suppose we have the following SMT-LIB code:
>
> (declare-sort Pair 2)
> (define-sort PInt () (Pair Int Int))
>
> If I am correct, this definition implies that each element of type PInt is
> a pair of integers. How can one access each element of this pair?
>
> Thanks,
> Amir
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>