[SMT-LIB] Array Usage Example

[Morgan Deters]

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