Module type Mcsolver.S

module type S = Solver_intf.S

The interface exposed by the solver.

Internal modules

These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.

module St: Solver_types.S

WARNING: Very dangerous module that expose the internal representation used by the solver.

module Proof: Res.S  with module St = St

A module to manipulate proofs.

Types

type atom = St.formula

The type of atoms given by the module argument for formulas

type res =

`\|`	`Sat of (St.term, St.formula) Solver_intf.sat_state`	`(*`	Returned when the solver reaches SAT	`*)`
`\|`	`Unsat of (St.clause, Proof.proof) Solver_intf.unsat_state`	`(*`	Returned when the solver reaches UNSAT	`*)`

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : ?tag:int -> atom list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val solve : ?assumptions:atom list -> unit -> res

Try and solves the current set of assumptions.

val new_lit : St.term -> unit

Add a new litteral (i.e term) to the solver. This term will be decided on at some point during solving, wether it appears in clauses or not.

val new_atom : atom -> unit

Add a new atom (i.e propositional formula) to the solver. This formula will be decided on at some point during solving, wether it appears in clauses or not.

val unsat_core : Proof.proof -> St.clause list

Returns the unsat core of a given proof.

val true_at_level0 : atom -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val get_tag : St.clause -> int option

Recover tag from a clause, if any

val export_dimacs : Format.formatter -> unit -> unit

Prints the entire set of clauses in the input problem (including hypothesis, lemmas and local assumptions), in the dimacs format.

val export_icnf : Format.formatter -> unit -> unit

Export the current problem contents to iCNF format. This function is meant to be used icnrementally, i.e. called for each return value of the solve function.