<commit_before># MSAT

MSAT is an OCaml library that features a modular SAT-solver and some
extensions (including SMT). This is *work in progress*.


It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).


## COPYRIGHT

This program is distributed under the Apache Software License version
2.0. See the enclosed file `LICENSE`.


## USAGE

A ready-to-use SAT solver is available in the Sat module. It can be used
as shown in the following code :

    (* Module initialization *)
    module F = Msat.Sat.Tseitin
    module Sat = Msat.Sat.Make(Msat.Log)

    (* We create here two distinct atoms *)
    let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *)
    let b = Sat.make 1      (* Atoms can be creted from integers *)

    (* Let's create some formulas *)
    let p = F.make_and [a; b]
    let q = F.make_or [F.make_not a; F.make_not b]

    (* We can try and check the satisfiability of the given formulas *)
    Sat.assume (F.make_cnf p)
    let _ = Sat.solve ()        (* Should return Sat.Sat *)

    (* The Sat solver has an incremental mutable state, so we still have
     * the formula 'p' in our assumptions *)
    Sat.assume (F.make_cnf q)
    let _ = Sat.solve ()        (* Should return Sat.Unsat *)

## INSTALLATION

### Via opam

Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
For the development version, use:

    opam pin add msat https://github.com/Gbury/mSAT.git

### Manual installation You will need ocamlfind. The command is:

    make install



<commit_msg>Fixed typo + added ocaml annotation in markdown<commit_after># MSAT

MSAT is an OCaml library that features a modular SAT-solver and some
extensions (including SMT). This is *work in progress*.


It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).


## COPYRIGHT

This program is distributed under the Apache Software License version
2.0. See the enclosed file `LICENSE`.


## USAGE

### Sat Solver

A ready-to-use SAT solver is available in the Sat module. It can be used
as shown in the following code :

```ocaml
    (* Module initialization *)
    module F = Msat.Sat.Tseitin
    module Sat = Msat.Sat.Make(Msat.Log)

    (* We create here two distinct atoms *)
    let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *)
    let b = Sat.make 1      (* Atoms can be created from integers *)

    (* Let's create some formulas *)
    let p = F.make_and [a; b]
    let q = F.make_or [F.make_not a; F.make_not b]

    (* We can try and check the satisfiability of the given formulas *)
    Sat.assume (F.make_cnf p)
    let _ = Sat.solve ()        (* Should return Sat.Sat *)

    (* The Sat solver has an incremental mutable state, so we still have
     * the formula 'p' in our assumptions *)
    Sat.assume (F.make_cnf q)
    let _ = Sat.solve ()        (* Should return Sat.Unsat *)
```

### Generic SAT/SMT Solver

A modular implementation of the SMT algorithm can be found in the `Msat.`

## INSTALLATION

### Via opam

Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
For the development version, use:

    opam pin add msat https://github.com/Gbury/mSAT.git

### Manual installation You will need ocamlfind. The command is:

    make install




{'fraction_non_alphanumeric': 0.10118505013673655, 'fraction_numerical': 0.0018231540565177757, 'mean_word_length': 2.9614921780986765, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 2, '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': '155865', 'n_tokens_mistral': 1092, 'n_tokens_neox': 1025, 'n_words': 417}