[SMT-LIB] SMT doubt
aaron.stump at gmail.com
Fri Jan 16 13:29:04 EST 2009
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
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.
SMT-LIB initiative co-organizer with Clark Barrett, Silvio Ranise, and
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.
> On Tue, Jan 6, 2009 at 5:44 PM, Daniela da Cruz <danieladacruz at gmail.com>wrote:
>> 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?
>> best regards
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
More information about the SMT-LIB