package msat

You can search for identifiers within the package.

in-package search v0.2.0

Library containing a SAT solver that can be parametrized by a theory

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (16)

Authors

Maintainers

Sources

v0.8.2.tar.gz

md5=c02d63bf45357aa1d1b85846da373f48

sha512=e6f0d7f6e4fe69938ec2cc3233b0cb72dd577bfb4cc4824afe8247f5db0b6ffea2d38d73a65e7ede500d21ff8db27ed12f2c4f3245df4451d02864260ae2ddaf

doc/msat.sat/Msat_sat/Int_lit/index.html

Module `Msat_sat.Int_lit`Source

The module defining formulas

SAT Formulas

This modules implements formuals adequate for use in a pure SAT Solver. Atomic formuals are represented using integers, that should allow near optimal efficiency (both in terms of space and time).

This modules implements the requirements for implementing an SAT Solver.

include Msat.Solver_intf.FORMULA

Sourcetype t

The type of atomic formulas over terms.

Sourceval equal : t -> t -> bool

Equality over formulas.

Sourceval hash : t -> int

Hashing function for formulas. Should be such that two formulas equal according to Expr_intf.S.equal have the same hash.

Sourceval pp : t Msat.Solver_intf.printer

Printing function used among other thing for debugging.

Sourceval neg : t -> t

Formula negation

Sourceval norm : t -> t * Msat.Solver_intf.negated

Returns a 'normalized' form of the formula, possibly negated (in which case return Negated). norm must be so that a and neg a normalise to the same formula, but one returns Negated and the other Same_sign.

Sourceval make : int -> t

Make a proposition from an integer.

Sourceval to_int : t -> int

Sourceval fresh : unit -> t

Make a fresh atom

Sourceval compare : t -> t -> int

Compare atoms

Sourceval sign : t -> bool

Is the given atom positive ?

Sourceval apply_sign : bool -> t -> t

apply_sign b is the identity if b is true, and the negation function if b is false.

Sourceval set_sign : bool -> t -> t

Return the atom with the sign set.

On This Page

The module defining formulas