<commit_before># LogTK

Logic toolkit, designed primarily for first-order automated reasoning. It aims
at providing basic types and algorithms (terms, unification, orderings,
indexing, etc.) that can be factored out of several applications.

## License

This project is licensed under the BSD2 license. See the `LICENSE` file.

## Regular build

You will need OCaml >= 4.00.1 or higher with ocamlbuild,
[zarith](https://forge.ocamlcore.org/projects/zarith/),
[ocaml-containers](https://github.com/c-cube/ocaml-containers/),
[sequence](https://github.com/c-cube/sequence/)
and the standard library.

Additional sub-libraries can be built if their respective dependencies
are met, and the appropriate `./configure --enable-foobar` flag was set.
For instance, to build the *meta-prover* library (used to detect axiomatic
theories), you should run

    $ ./configure --enable-meta

If [menhir](http://cristal.inria.fr/~fpottier/menhir/) is installed, the
parsers library `Logtk_parsers` can be built with

    $ ./configure --enable-parsers

If you have installed [qcheck](https://github.com/c-cube/qcheck/), for instance
via `opam install qcheck`, you can enable the property-based testing and
random term generators with

    $ ./configure --enable-qcheck --enable-tests<commit_msg>updated readme to favor opam<commit_after># LogTK

Logic toolkit, designed primarily for first-order automated reasoning. It aims
at providing basic types and algorithms (terms, unification, orderings,
indexing, etc.) that can be factored out of several applications.

## License

This project is licensed under the BSD2 license. See the `LICENSE` file.

## Build

### Via opam

We recommand using [opam](http://opam.ocaml.org). Once you installed it,
type

    $ opam repository add deducteam https://gforge.inria.fr/git/opam-deducteam/opam-deducteam.git
    $ opam install logtk

### From sources

You will need OCaml >= 4.00.1 or higher with ocamlbuild,
[zarith](https://forge.ocamlcore.org/projects/zarith/),
[ocaml-containers](https://github.com/c-cube/ocaml-containers/),
[sequence](https://github.com/c-cube/sequence/)
and the standard library.

Additional sub-libraries can be built if their respective dependencies
are met, and the appropriate `./configure --enable-foobar` flag was set.
For instance, to build the *meta-prover* library (used to detect axiomatic
theories), you should run

    $ ./configure --enable-meta

If [menhir](http://cristal.inria.fr/~fpottier/menhir/) is installed, the
parsers library `Logtk_parsers` can be built with

    $ ./configure --enable-parsers

If you have installed [qcheck](https://github.com/c-cube/qcheck/), for instance
via `opam install qcheck`, you can enable the property-based testing and
random term generators with

    $ ./configure --enable-qcheck --enable-tests
{'fraction_non_alphanumeric': 0.11063526052819414, 'fraction_numerical': 0.0035688793718772305, 'mean_word_length': 4.268796992481203, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 9, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4342962', 'n_tokens_mistral': 861, 'n_tokens_neox': 828, 'n_words': 297}