Hi, and thanks for the reply. Sorry if my questions sound naive. I've now read that part of the manual and I can now load the module Array. But I have some difficulties, for instance: I am trying to build formulas and terms such as a[0]>1 /\ a[1]>2 ==> a[0]+a[1]>3 . I fail though in even understanding how to build a term of type "array". While for "first order" terms like integers or naturals it works ok. I would also eventually like to quantify existentially over a its indices. I m trying to read this http://why3.lri.fr/stdlib-0.81/array.mlw.html but I don't understand how to do things in ocaml.
Cheers, GP On Wed, May 2, 2018 at 5:37 AM, Claude Marché <claude.mar...@inria.fr> wrote: > > Hello, > > I guess you already read the chapter 4 of the manual ( > http://why3.lri.fr/doc/api.html#sec30). The importation of modules and > the manipulation of programs is not documented yet, but you can find some > examples of use in the directory examples/use_api of the distribution: > files mlw.ml and mlw_tree.ml. > > Indeed there is a subtle distinction between modules and theories. Arrays > are in a module and not in a theory. Specifically, the importation of a > module is done using Mlw_module.read_module. see > http://why3.lri.fr/api/Mlw_module.html > > Do not hesitate to request for more help on any specific use of the API > > - Claude > > > > Le 01/05/2018 à 23:55, Gian Pietro Farina a écrit : > >> Hello, >> >> I would like to use the Ocaml api of why3 in my project where I need to >> send to the smt solvers >> queries in the theory of arrays. How do I load a theory in my project? >> >> Best regards, >> Gian Pietro >> >> >> >> _______________________________________________ >> Why3-club mailing list >> Why3-club@lists.gforge.inria.fr >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club >> > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
