[SMT-LIB] Array Usage Example

[haihao shen]

Thank you for your info, Morgan. I will try it :)

Best,
Haihao

On Tue, Dec 20, 2011 at 8:00 AM, Morgan Deters <mdeters at gmail.com> wrote:

> Hi Haihao,
>
> Certainly.  There are lots of array benchmarks in the SMT-LIB library.
>  Here's a short one:
>
>
> http://smtexec.org/exec/smtlib-portal-benchmarks.php?download&inline&b=QF_AX%2Fcvc%2Fread5.smt2
>
> Others can be browsed at
>
>   http://smtexec.org/exec/smtlib-portal-benchmarks.php
>
> ..I suggest you look at the QF_AX logic.  The array theory is defined here:
>
>   http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2
>
> Best,
> Morgan
>
>
> On Sun, Dec 18, 2011 at 9:31 AM, haihao shen <haihaoshen at gmail.com> wrote:
>
>> Hello,
>>
>> As mentioned in tutorial, smt syntax could support Array theory. However,
>> I
>> cannot find a example from tutorial. Could anyone please share an example
>> of its usage?
>>
>> Thanks in advance!
>>
>> Best,
>> Haihao
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
>>
>
>
> --
> Morgan Deters
> mdeters at gmail.com
>