#### msat

Library

Module

Module type

Parameter

Class

Class type

`type 'a printer = Format.formatter -> 'a -> unit`

`type ('term, 'form, 'value) sat_state = {`

`}`

The type of values returned when the solver reaches a SAT state.

`type ('atom, 'clause, 'proof) unsat_state = {`

`}`

The type of values returned when the solver reaches an UNSAT state.

Export internal state

This type is used during the normalisation of formulas. See `Expr_intf`

.S.norm for more details.

`type 'term eval_res = `

The type of evaluation results for a given formula. For instance, let's suppose we want to evaluate the formula `x * y = 0`

, the following result are correct:

`Unknown`

if neither`x`

nor`y`

are assigned to a value`Valued (true, [x])`

if`x`

is assigned to`0`

`Valued (true, [y])`

if`y`

is assigned to`0`

`Valued (false, [x; y])`

if`x`

and`y`

are assigned to 1 (or any non-zero number)

`type ('term, 'formula, 'value) assumption = `

`| Lit of 'formula` | (* The given formula is asserted true by the solver *) |

`| Assign of 'term * 'value` | (* The term is assigned to the value *) |

Asusmptions made by the core SAT solver.

`type ('term, 'formula, 'proof) reason = `

The type of reasons for propagations of a formula `f`

.

`type ('term, 'formula, 'value, 'proof) acts = {`

```
acts_iter_assumptions : ( ( 'term, 'formula, 'value ) assumption -> unit ) ->
unit;
``` | (* Traverse the new assumptions on the boolean trail. *) |

`acts_eval_lit : 'formula -> lbool;` | (* Obtain current value of the given literal *) |

`acts_mk_lit : 'formula -> unit;` | (* Map the given formula to a literal, which will be decided by the SAT solver. *) |

`acts_mk_term : 'term -> unit;` | (* Map the given term (and its subterms) to decision variables, for the MCSAT solver to decide. *) |

`acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;` | (* Add a clause to the solver. *) |

`acts_raise_conflict : 'b. 'formula list -> 'proof -> 'b;` | (* Raise a conflict, yielding control back to the solver. The list of atoms must be a valid theory lemma that is false in the current trail. *) |

`acts_propagate : 'formula -> ( 'term, 'formula, 'proof ) reason -> unit;` | (* Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of |

`}`

The type for a slice of assertions to assume/propagate in the theory.

`type void = ( unit, bool ) gadt_eq`

A provably empty type

`module type FORMULA = sig ... end`

formulas

`module type EXPR = sig ... end`

Formulas and Terms required for mcSAT

`module type PLUGIN_CDCL_T = sig ... end`

Signature for theories to be given to the CDCL(T) solver

`module type PLUGIN_MCSAT = sig ... end`

Signature for theories to be given to the Model Constructing Solver.

`module type PLUGIN_SAT = sig ... end`

Signature for pure SAT solvers

`module type PROOF = sig ... end`

Signature for a module handling proof by resolution from sat solving traces

`module type S = sig ... end`

The external interface implemented by safe solvers, such as the one created by the `Solver`

.Make and `Mcsolver`

.Make functors.