[SMT-LIB] SMT doubt

[Paulo J. Matos]

2009/1/6 Daniela da Cruz <danieladacruz at gmail.com>:
> Sorry, was the wrong attachement.
> Now the correct.
> daniela
>

Ola Daniela,

Several issues.

1. Why would you need to negate formulas? The SMT Solver work is to
find a solution to the formula you give it. That's all. Thinking about
negation might me wonder if you are mixing satisfiability solving with
model checking.
2. It depends on what the theory says (can't remember correctly right
now) but I would think you cannot have variable length arrays!!!

Now, by looking at your file, you have several logic definitions. Why?
There should be only one. Same question regarding formulas!

Cheers and good luck,

Paulo Matos

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



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm