diff --git a/src/backend/backend_intf.ml b/src/backend/backend_intf.ml index 81957d78..9cfff729 100644 --- a/src/backend/backend_intf.ml +++ b/src/backend/backend_intf.ml @@ -1,6 +1,27 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** Backend interface + + This modules defines the interface of the modules providing + export of proofs. +*) module type S = sig + (** Proof exporting + + Currently, exporting a proof means printing it into a file + according to the conventions of a given format. + *) + type t + (** The type of proofs. *) + val print : Format.formatter -> t -> unit + (** A function for printing proofs in the desired format. *) + end diff --git a/src/backend/dot.ml b/src/backend/dot.ml index b629e7a4..f8338a2e 100644 --- a/src/backend/dot.ml +++ b/src/backend/dot.ml @@ -1,3 +1,8 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module type S = Backend_intf.S diff --git a/src/backend/dot.mli b/src/backend/dot.mli index aa86092d..e66665f1 100644 --- a/src/backend/dot.mli +++ b/src/backend/dot.mli @@ -1,14 +1,50 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** Dot backend for proofs + + This modules provides functions to export proofs into the dot graph format. + Graphs in dot format can be used to generates images using the graphviz tool. +*) module type S = Backend_intf.S +(** Interface for exporting proofs. *) module type Arg = sig + (** Term printing for DOT + + This module defines what functions are required in order to export + a proof to the DOT format. + *) + type atom + (** The type of atomic formuals *) + type lemma + (** The type of theory-specifi proofs (also called lemmas). *) val print_atom : Format.formatter -> atom -> unit + (** Print the contents of the given atomic formulas. + WARNING: this function should take care to esapce and/or not output special + reserved characters for the dot format (such as quotes and so on). *) + val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list + (** Generate some information about a theory specific lemmas. This backend does not + support printing of proper proofs in DOT format, so all proofs are printed as leafs + of the resolution tree. This function should return a triplet [(rule, color, l)], + such that: + - [rule] is a name for the proof (arbitrary, does not need to be unique, but + should rather be descriptive) + - [color] is a color name (optional) understood by DOT + - [l] is a list of printers that will be called to print some additional information + *) + end module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) : S with type t := S.proof +(** Functor for making a module to export proofs to the DOT format. *) diff --git a/src/core/expr_intf.ml b/src/core/expr_intf.ml index 84fe946f..172ab472 100644 --- a/src/core/expr_intf.ml +++ b/src/core/expr_intf.ml @@ -4,9 +4,16 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +(** Mcsat expressions + + This modules defines the required implementation of expressions for Mcsat. +*) + type negated = Formula_intf.negated = - | Negated (* changed sign *) - | Same_sign (* kept sign *) + | Negated (** changed sign *) + | Same_sign (** kept sign *) +(** This type is used during the normalisation of formulas. + See {!val:Expr_intf.S.norm} for more details. *) module type S = sig (** Signature of formulas that parametrises the Mcsat Solver Module. *) @@ -15,29 +22,41 @@ module type S = sig (** An abstract type for proofs *) module Term : sig + (** McSat Terms *) type t (** The type of terms *) - val hash : t -> int val equal : t -> t -> bool + (** Equality over terms. *) + + val hash : t -> int + (** Hashing function for terms. Should be such that two terms equal according + to {!val:Expr_intf.S.equal} have the same hash. *) + val print : Format.formatter -> t -> unit - (** Common functions *) + (** Printing function used among other for debugging. *) end module Formula : sig + (** McSat formulas *) type t (** The type of atomic formulas over terms. *) - val hash : t -> int 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 {!val:Expr_intf.S.equal} have the same hash. *) + val print : Format.formatter -> t -> unit - (** Common functions *) + (** Printing function used among other thing for debugging. *) val dummy : t - (** Formula constants. A valid formula should never be physically equal to [dummy] *) + (** Constant formula. A valid formula should never be physically equal to [dummy] *) val neg : t -> t (** Formula negation *) diff --git a/src/core/formula_intf.ml b/src/core/formula_intf.ml index 366b2f46..08dc9646 100644 --- a/src/core/formula_intf.ml +++ b/src/core/formula_intf.ml @@ -4,12 +4,20 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +(** SMT formulas + + This module defines the required implementation of formulas for + an SMT solver. +*) + type negated = - | Negated (* changed sign *) - | Same_sign (* kept sign *) + | Negated (** changed sign *) + | Same_sign (** kept sign *) +(** This type is used during the normalisation of formulas. + See {!val:Expr_intf.S.norm} for more details. *) module type S = sig - (** Signature of formulas that parametrises the SAT/SMT Solver Module. *) + (** SMT formulas *) type t (** The type of atomic formulas. *) @@ -17,13 +25,18 @@ module type S = sig type proof (** An abstract type for proofs *) - val hash : t -> int 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 {!val:Expr_intf.S.equal} have the same hash. *) + val print : Format.formatter -> t -> unit - (** Common functions *) + (** Printing function used among other thing for debugging. *) val dummy : t - (** Formula constants. A valid formula should never be physically equal to [dummy] *) + (** Formula constant. A valid formula should never be physically equal to [dummy] *) val neg : t -> t (** Formula negation *) diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml index 6ed3e8c8..bfba8585 100644 --- a/src/core/plugin_intf.ml +++ b/src/core/plugin_intf.ml @@ -12,38 +12,54 @@ (* *) (**************************************************************************) +(** McSat Theory + + This module defines what a theory must implement in order to + be sued in a McSat solver. +*) + type 'term eval_res = - | Unknown - | Valued of bool * ('term list) -(** The type of evaluation results, either the given formula cannot be - evaluated, or it can thanks to assignment. In that case, the level - of the evaluation is the maximum of levels of assignemnts needed - to evaluate the given formula. *) + | Unknown (** The given formula does not have an evaluation *) + | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool. + The list of terms to give is the list of terms that + were effectively used for the evaluation. + *) +(** 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 ('formula, 'proof) res = | Sat + (** The current set of assumptions is satisfiable. *) | Unsat of 'formula list * 'proof -(** Type returned by the theory, either the current set of assumptions is satisfiable, - or it is not, in which case a tautological clause (hopefully minimal) is returned. - Formulas in the unsat clause must come from the current set of assumptions, i.e - must have been encountered in a slice. *) + (** The current set of assumptions is *NOT* satisfiable, and here is a + theory tautology (with its proof), for which every litteral is false + under the current assumptions. *) +(** Type returned by the theory. Formulas in the unsat clause must come from the + current set of assumptions, i.e must have been encountered in a slice. *) type ('term, 'formula) assumption = - | Lit of 'formula - | Assign of 'term * 'term -(** Asusmptions made by the core SAT solver. Can be either a formula, or an assignment. - Assignemnt are given a level. *) + | Lit of 'formula (** The given formula is asserted true by the solver *) + | Assign of 'term * 'term (** The first term is assigned to the second *) +(** Asusmptions made by the core SAT solver. *) type ('term, 'formula, 'proof) slice = { - start : int; - length : int; - get : int -> ('term, 'formula) assumption; - push : 'formula list -> 'proof -> unit; - propagate : 'formula -> 'term list -> unit; + start : int; (** Start of the slice *) + length : int; (** Length of the slice *) + get : int -> ('term, 'formula) assumption; (** Accessor for the assertions in the slice. + Should only be called on integers [i] s.t. + [start <= i < start + length] *) + push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *) + propagate : 'formula -> 'term list -> unit; (** Propagate a formula, i.e. the theory can + evaluate the formula to be true (see the + definition of {!type:eval_res} *) } -(** The type for a slice of litterals to assume/propagate in the theory. - [get] operations should only be used for integers [ start <= i < start + length]. - [push clause proof] allows to add a tautological clause to the sat solver. *) +(** The type for a slice of assertions to assume/propagate in the theory. *) module type S = sig (** Signature for theories to be given to the Model Constructing Solver. *) diff --git a/src/core/res.mli b/src/core/res.mli index 5781ec3a..a2c8bdc9 100644 --- a/src/core/res.mli +++ b/src/core/res.mli @@ -4,7 +4,14 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +(** Resolution proofs + + This modules defines functions to create and manipulate resolution proofs. +*) + module type S = Res_intf.S +(** Interface for a module manipulating resolution proofs. *) module Make : functor (St : Solver_types.S) -> S with module St = St (** Functor to create a module building proofs from a sat-solver unsat trace. *) + diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml index dd600568..4630cae7 100644 --- a/src/core/res_intf.ml +++ b/src/core/res_intf.ml @@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +(** Interface for proofs *) + module type S = sig (** Signature for a module handling proof by resolution from sat solving traces *) @@ -21,19 +23,28 @@ module type S = sig (** Abstract types for atoms, clauses and theory-specific lemmas *) type proof - and proof_node = { - conclusion : clause; - step : step; - } - and step = - | Hypothesis - | Assumption - | Lemma of lemma - | Resolution of proof * proof * atom (** Lazy type for proof trees. Proofs are persistent objects, and can be extended to proof nodes using functions defined later. *) + and proof_node = { + conclusion : clause; (** The conclusion of the proof *) + step : step; (** The reasoning step used to prove the conclusion *) + } + (** A proof can be expanded into a proof node, which show the first step of the proof. *) + and step = + | Hypothesis + (** The conclusion is a user-provided hypothesis *) + | Assumption + (** The conclusion has been locally assumed by the user *) + | Lemma of lemma + (** The conclusion is a tautology provided by the theory, with associated proof *) + | Resolution of proof * proof * atom + (** The conclusion can be deduced by performing a resolution between the conclusions + of the two given proofs. The atom on which to perform the resolution is also given. *) + (** The type of reasoning steps allowed in a proof. *) + (** {3 Resolution helpers} *) + val to_list : clause -> atom list (** Returns the sorted list of atoms of a clause. *) @@ -45,6 +56,7 @@ module type S = sig [resolve (List.merge l1 l2)] where [l1] and [l2] are sorted atom lists should return the pair [\[a\], l'], where [l'] is the result of the resolution of [l1] and [l2] over [a]. *) + (** {3 Proof building functions} *) val prove : clause -> proof @@ -58,6 +70,7 @@ module type S = sig val prove_atom : atom -> proof option (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *) + (** {3 Proof Manipulation} *) val expand : proof -> proof_node @@ -72,6 +85,7 @@ module type S = sig (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. More efficient than using the [fold] function since it has access to the internal representation of proofs *) + (** {3 Misc} *) val check : proof -> unit diff --git a/src/core/solver_intf.ml b/src/core/solver_intf.ml index 4e922930..c79d4457 100644 --- a/src/core/solver_intf.ml +++ b/src/core/solver_intf.ml @@ -4,6 +4,11 @@ Copyright 2016 Guillaume Bury Copyright 2016 Simon Cruanes *) +(** Interface for Solvers + This modules defines the safe external interface for solvers. + Solvers that implements this interface can be obtained using the [Make] + functor in {!Solver} or {!Mcsolver}. *) + type ('term, 'form) sat_state = { eval: 'form -> bool; (** Returns the valuation of a formula in the current state @@ -21,6 +26,7 @@ type ('term, 'form) sat_state = { model: unit -> ('term * 'term) list; (** Returns the model found if the formula is satisfiable. *) } +(** The type of values returned when the solver reaches a SAT state. *) type ('clause, 'proof) unsat_state = { unsat_conflict : unit -> 'clause; @@ -28,7 +34,10 @@ type ('clause, 'proof) unsat_state = { get_proof : unit -> 'proof; (** returns a persistent proof of the empty clause from the Unsat result. *) } +(** The type of values returned when the solver reaches an UNSAT state. *) +(** The external interface implemented by safe solvers, such as the one + created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) module type S = sig (** {2 Internal modules} @@ -36,8 +45,11 @@ module type S = sig 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. *) (** {2 Types} *) @@ -46,7 +58,7 @@ module type S = sig type res = | Sat of (St.term,St.formula) sat_state - | Unsat of (St.clause,Proof.proof) unsat_state + | Unsat of (St.clause,Proof.proof) unsat_state (**) (** Result type for the solver *) exception UndecidedLit diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml index d02a0017..f6e9c263 100644 --- a/src/core/theory_intf.ml +++ b/src/core/theory_intf.ml @@ -12,23 +12,33 @@ (* *) (**************************************************************************) +(** SMT Theory + + This module defines what a theory must implement in order to + be used in an SMT solver. +*) + type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res = | Sat + (** The current set of assumptions is satisfiable. *) | Unsat of 'formula list * 'proof -(** Type returned by the theory, either the current set of assumptions is satisfiable, - or it is not, in which case a tautological clause (hopefully minimal) is returned. - Formulas in the unsat clause must come from the current set of assumptions, i.e - must have been encountered in a slice. *) + (** The current set of assumptions is *NOT* satisfiable, and here is a + theory tautology (with its proof), for which every litteral is false + under the current assumptions. *) +(** Type returned by the theory. Formulas in the unsat clause must come from the + current set of assumptions, i.e must have been encountered in a slice. *) type ('form, 'proof) slice = { - start : int; - length : int; - get : int -> 'form; - push : 'form list -> 'proof -> unit; + start : int; (** Start of the slice *) + length : int; (** Length of the slice *) + get : int -> 'form; (** Accesor for the formuals in the slice. + Should only be called on integers [i] s.t. + [start <= i < start + length] *) + push : 'form list -> 'proof -> unit; (** Allows to add to the solver a clause. *) } -(** The type for a slice of literals to assume/propagate in the theory. - [get] operations should only be used for integers [ start <= i < start + length]. - [push clause proof] allows to add a tautological clause to the sat solver. *) +(** The type for a slice. Slices are some kind of view of the current + propagation queue. They allow to look at the propagated literals, + and to add new clauses to the solver. *) module type S = sig (** Signature for theories to be given to the Solver. *) diff --git a/src/doc.txt b/src/doc.txt index fa385768..f147b970 100644 --- a/src/doc.txt +++ b/src/doc.txt @@ -6,10 +6,10 @@ This code is free, under the Apache 2.0 license. {2 Contents} -mSAT is an ocaml library provinding SAT/SMT/McSat solvers. More precisely, +mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely, what mSAT provides are functors to easily create such solvers. Indeed, the core of a sat solver does not need much information about neither the exact representation -of terms nor the innner workings of a theory. +of terms nor the inner workings of a theory. {4 Solver creation} @@ -18,6 +18,7 @@ simply an SMT solver with an empty theory). {!modules: Solver +Solver_intf Formula_intf Theory_intf } @@ -26,6 +27,7 @@ The following modules allow the creation of a McSat solver (Model Constructing s {!modules: Mcsolver +Solver_intf Expr_intf Plugin_intf } diff --git a/src/msat.odocl b/src/msat.odocl index 94e2d9ec..ac01fe3f 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -27,17 +27,17 @@ backend/Dedukti backend/Backend_intf # SAT solver frontend -sat/Sat -sat/Expr_sat -sat/Type_sat +#sat/Sat +#sat/Expr_sat +#sat/Type_sat # SMT solver frontend -smt/Smt -smt/Expr_smt -smt/Type_smt -smt/Unionfind +#smt/Smt +#smt/Expr_smt +#smt/Type_smt +#smt/Unionfind # MCsat solver frontend -mcsat/Mcsat -mcsat/Eclosure -mcsat/Plugin_mcsat +#mcsat/Mcsat +#mcsat/Eclosure +#mcsat/Plugin_mcsat diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli index 8e16f22b..53e81531 100644 --- a/src/solver/mcsolver.mli +++ b/src/solver/mcsolver.mli @@ -4,7 +4,11 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +(** Create McSat solver + This module provides a functor to create an McSAt solver. *) + module type S = Solver_intf.S +(** The interface exposed by the solver. *) module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t diff --git a/src/solver/solver.mli b/src/solver/solver.mli index 17a25f31..15e49b10 100644 --- a/src/solver/solver.mli +++ b/src/solver/solver.mli @@ -4,12 +4,18 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module type S = Solver_intf.S +(** Create SAT/SMT Solvers + This module provides a functor to create an SMT solver. Additionally, it also + gives a functor that produce an adequate empty theory that can be given to the [Make] + functor in order to create a pure SAT solver. *) + +module type S = Solver_intf.S +(** The interface of instantiated solvers. *) -(** Simple case where the proof type is [unit] and the theory is empty *) module DummyTheory(F : Formula_intf.S) : Theory_intf.S with type formula = F.t and type proof = F.proof +(** Simple case where the proof type is [unit] and the theory is empty *) module Make (F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t @@ -17,6 +23,6 @@ module Make (F : Formula_intf.S) (Dummy: sig end) : S with type St.formula = F.t and type St.proof = F.proof - (** Functor to create a SMT Solver parametrised by the atomic - formulas and a theory. *) +(** Functor to create a SMT Solver parametrised by the atomic + formulas and a theory. *) diff --git a/src/solver/tseitin.mli b/src/solver/tseitin.mli index 12e8066c..498667c5 100644 --- a/src/solver/tseitin.mli +++ b/src/solver/tseitin.mli @@ -4,8 +4,19 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +(** Tseitin CNF conversion + + This modules implements Tseitin's Conjunctive Normal Form conversion, i.e. + the ability to transform an arbitrary boolean formula into an equi-satisfiable + CNF, that can then be fed to a SAT/SMT/McSat solver. +*) + +module type Arg = Tseitin_intf.Arg +(** The implementation of formulas required to implement Tseitin's CNF conversion. *) + module type S = Tseitin_intf.S +(** The exposed interface of Tseitin's CNF conversion. *) -module Make : functor - (F : Tseitin_intf.Arg) -> S with type atom = F.t +module Make : functor (F : Arg) -> S with type atom = F.t +(** This functor provides an implementation of Tseitin's CNF conversion. *) diff --git a/src/solver/tseitin_intf.ml b/src/solver/tseitin_intf.ml index 3f02b4f8..abdfcf63 100644 --- a/src/solver/tseitin_intf.ml +++ b/src/solver/tseitin_intf.ml @@ -10,46 +10,75 @@ (* *) (**************************************************************************) +(** Interfaces for Tseitin's CNF conversion *) + module type Arg = sig + (** Formulas + + This defines what is needed of formulas in order to implement + Tseitin's CNF conversion. + *) type t - (** Type of atomic formulas *) + (** Type of atomic formulas. *) val neg : t -> t - (** Negation of atomic formulas *) + (** Negation of atomic formulas. *) val fresh : unit -> t - (** Generate fresh formulas *) + (** Generate fresh formulas (that are different from any other). *) val print : Format.formatter -> t -> unit - (** Print the given formula *) + (** Print the given formula. *) end module type S = sig + (** CNF conversion + + This modules allows to convert arbitrary boolean formulas + into CNF. + *) - (** The type of ground formulas *) - type t type atom + (** The type of atomic formulas. *) + + type t + (** The type of arbitrary boolean formulas. Arbitrary boolean formulas + can be built using functions in this module, and then converted + to a CNF, which is a list of clauses that only use atomic formulas. *) val f_true : t + (** The [true] formula, i.e a formula that is always satisfied. *) + val f_false : t + (** The [false] formula, i.e a formula that cannot be satisfied. *) val make_atom : atom -> t - (** [make_pred p] builds the atomic formula [p = true]. - @param sign the polarity of the atomic formula *) + (** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *) val make_not : t -> t + (** Creates the negation of a boolean formula. *) + val make_and : t list -> t + (** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *) + val make_or : t list -> t - val make_imply : t -> t -> t - val make_equiv : t -> t -> t + (** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *) + val make_xor : t -> t -> t + (** [make_xor p q] creates the boolean formula "[p] xor [q]". *) + + val make_imply : t -> t -> t + (** [make_imply p q] creates the boolean formula "[p] implies [q]". *) + + val make_equiv : t -> t -> t + (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *) val make_cnf : t -> atom list list (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a list (which is a conjunction) of lists (which are disjunctions) of - literals. *) + atomic formulas. *) val print : Format.formatter -> t -> unit (** [print fmt f] prints the formula on the formatter [fmt].*)