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
