package dose3

  1. Overview
  2. Docs
Dose library (part of Mancoosi tools)

Install

Dune Dependency

Authors

Maintainers

Sources

dose3-7.0.0.tar.gz
md5=bc99cbcea8fca29dca3ebbee54be45e1
sha512=98dc4bd28e9f4aa8384be71b31783ae1afac577ea587118b8457b554ffe302c98e83d0098971e6b81803ee5c4f2befe3a98ef196d6b0da8feb4121e982ad5c2f

doc/dose3.algo/Dose_algo/Depsolver_int/S/index.html

Module Depsolver_int.SSource

Sourcemodule X = R

generic failure reason

Sourcetype state

state of the solver

Sourcetype var = int

variables are integers numbered from 0 to (size - 1)

Sourcetype value =
  1. | True
  2. | False
  3. | Unknown

The value of a literal

Sourcetype lit

A literal. Literals can be positive or negative

Sourceval lit_of_var : var -> bool -> lit

lit_of_var given a variable create a positive or a negative literal. By default the assigment of all variables (that is its value) is Unknown.

Sourceval initialize_problem : ?print_var:(Format.formatter -> int -> unit) -> ?buffer:bool -> int -> state

initialize the solver initialize_problem n

  • parameter print_var

    a function to print a variable

  • parameter buffer

    decide weather or not to store a human readable representaion of the sat problem.

  • parameter n

    the size of the sat problem. that is the max number of variables to consider

Sourceval copy : state -> state

provide a deep copy of the current state of the solver

Sourceval propagate : state -> unit
Sourceval protect : state -> unit
Sourceval reset : state -> unit

reset reset the state of the solver to a state that would be obtained by re initializing the solver with an identical constraints set

Sourceval assignment : state -> value array

assignment st return the array of values associated to every variable.

Sourceval assignment_true : state -> var list

assignment_true st return the list of variables that are true

Sourceval add_rule : state -> lit array -> X.reason list -> unit

add_rule st l add a disjuction to the solver of type \Bigvee l

Sourceval associate_vars : state -> lit -> var list -> unit

associate_vars st lit vl associate a variable to a list of variables. The solver will use this information to guide the search heuristic

Sourceval solve_all : (state -> unit) -> state -> var -> bool
Sourceval solve : state -> var -> bool

solve st v finds a variable assignment that makes v True

Sourceval solve_lst : state -> var list -> bool

solve st l finds a variable assignment that makes True all variables in l

Sourceval collect_reasons : state -> var -> X.reason list

in case of failure return the list of associated reasons

Sourceval collect_reasons_lst : state -> var list -> X.reason list

in case of failure return the list of associated reasons

Sourceval dump : state -> (int * bool) list list

if the solver was initialized with buffer = true, dump the state of the solver. Return an empty list otherwise

Sourceval debug : bool -> unit

enable debug messages

Sourceval stats : state -> unit
OCaml

Innovation. Community. Security.