package msat

  1. Overview
  2. Docs
Library containing a SAT solver that can be parametrized by a theory

Install 

dune-project
 Dependency

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

Authors

  1. S
    Simon Cruanes
  2. G
    Guillaume Bury

Maintainers

  1. G
    guillaume.bury@gmail.com
  2. S
    simon.cruanes.2007@m4x.org

Sources

v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99

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

Module Msat_sat.Int_lit

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
type t

The type of atomic formulas over terms.

val equal : t -> t -> bool

Equality over formulas.

val hash : t -> int

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

Printing function used among other thing for debugging.

val neg : t -> t

Formula negation

val 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.

val make : int -> t

Make a proposition from an integer.

val to_int : t -> int
val fresh : unit -> t

Make a fresh atom

val compare : t -> t -> int

Compare atoms

val sign : t -> bool

Is the given atom positive ?

val apply_sign : bool -> t -> t

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

val set_sign : bool -> t -> t

Return the atom with the sign set.