[SMT-LIB] SMT doubt

[Aaron Stump]

Hi, Daniela.

Sorry for the slow reply!  Looking at the file you sent along, I
notice a few things that might be contributing
to your problem:

1. If you take a look at Definition 5 on page 23 of the SMT-LIB
specification -- available at

   http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf

   you will see that a benchmark can only have one ":formula"
attribute.  If you want to check satisfiability
   of a formula F with respect to some assumptions A1 ... An, then you
use one ":assumption" attribute
   for each Ai, and the ":formula" attribute for F.  As explained in
Section 5 (starting page 22) of the specification,
   the semantics of a benchmark like this is to check satisfiability
of (and A1 ... An F).  So if you want to test
   validity of an implication like (implies (and A1 ... An) F), then
it suffices to test (un)satisfiability of (and A1 ... An (not F)).

2. To define a variable, you include in your formula a "let" or
"flet".  See page 13 of the specification.

I hope that helps.

Sincerely,
Aaron Stump
SMT-LIB initiative co-organizer with Clark Barrett, Silvio Ranise, and
Cesare Tinelli.

On Tue, Jan 6, 2009 at 11:45 AM, Daniela da Cruz
<danieladacruz at gmail.com> wrote:
> Sorry, was the wrong attachement.
> Now the correct.
> daniela
>
> On Tue, Jan 6, 2009 at 5:44 PM, Daniela da Cruz <danieladacruz at gmail.com>wrote:
>
>> Hi.
>> I'm new in the SMT language and I'm facing some problems with respect to
>> the understanding
>> of notation.
>> I send in attachement a file that I write to prove a set of formulas.
>> I've two questions:
>> 1. There is necessary to negate each formula?
>> 2. When we are reasoning over arrays, there it makes sense to define the
>> size of the array as a variable
>> (for example, the variable "length" with value 100). If so, how I do it?
>>
>> Thanks
>> best regards
>> daniela
>>
>>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>