package touist

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

CNF to clauses
Solving clauses (using Minisat)

package touist

touist
- TouistCnf
- TouistErr
- TouistEval
- TouistLatex
- TouistParse
- TouistPprint
- TouistQbf
- TouistSatSolve
  - Model
  - ModelSet
- TouistSmt
- TouistTypes
  - Ast
  - AstSet
- TouistVersion

Legend:
Library
Module
Module type
Parameter
Class
Class type

Requires minisat Process a CNF AST to clauses in order to solve them with Minisat.

CNF to clauses

val minisat_clauses_of_cnf : 
  TouistTypes.Ast.t ->
  Minisat.Lit.t list list * (Minisat.Lit.t, string) Hashtbl.t

minisat_clauses_of_cnf ast takes a CNF ast and outputs

a list of lists of Minisat litterals,
a mapping table (Minisat litterals -> name of the proposition)

Solving clauses (using Minisat)

module Model : sig ... end

module ModelSet : sig ... end

val solve_clauses : 
  ?verbose:bool ->
  ?print:(Model.t -> int -> unit) ->
  ?continue:(Model.t -> int -> bool) ->
  (Minisat.Lit.t list list * (Minisat.Lit.t, string) Hashtbl.t) ->
  ModelSet.t Pervasives.ref

solve_clauses finds the models for the given clauses.

print model N is a function that will print a model as soon as it is found. N is the number of the model, it begins at 1. It can be useful to print the models as they appear because finding all models (if limit is large) can be extremely long. Example: ~print:(TouistSatSolve.Model.pprint table model)

verbose allows to turn on the verbose mode of minisat; apparently, this minisat feature doesn't seem to be working and doesn't display any time information.

continue model nth is a function called after every model that has been found. model contains the found model and N says that this model was the nth model found. This function tells solve_clauses to go on searching models or not.

val string_of_clause : Minisat.Lit.t list -> string

val string_of_clauses : Minisat.Lit.t list list -> string