Functor Mcsolver.Make

module Make: functor (E : Expr_intf.S) -> functor (Th : Plugin_intf.S  with type term = E.Term.t
                         and type formula = E.Formula.t
                         and type proof = E.proof) -> functor (Dummy : sig

end) -> S  with type St.term = E.Term.t
     and type St.formula = E.Formula.t
     and type St.proof = E.proof

Functor to create a solver parametrised by the atomic formulas and a theory.

Parameters:

`E`	:	`Expr_intf.S`
`Th`	:	`Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof`
`Dummy`	:	`sig end`

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.