package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

The purpose of the solver is to generate *all* the integer solutions of a system of linear equations of the following form: 1- all the variables are positive 2- all the coefficients are positive

We expect the systems and the number of solutions to be small. This motivates a simple solver which performs 1 - interval analysis 2 - substitutions 3 - enumeration

system represents a system of equation. Each equation is indexed by a unique identifier id (an integer).

type system
type var = int

var is the type of variables

type id = int

id are used to identify equations in a system

type eqn

An equation eqn is of the form a1.x1 + ... + an.xn = a0 where the ai are integer coefficients and xi are variables.

val output_equations : Stdlib.out_channel -> eqn list -> unit

output_equations o l prints the list of equations

val empty : system

empty is the system with no equation

val set_constant : id -> int -> system -> eqn

set_constant i c s returns the equation i of the system s where the constant a0 is set to c

val make_mon : id -> var -> int -> system -> system

make_mon i x a s augments the system s with the equation a.x = 0 indexed by i

val merge : system -> system -> system

merge s1 s2 returns a system s such that the equation i is obtained by adding of the equations s1(i) and s2(i) i.e. s(i) = s1(i) + s2(i) NB: the operation is only well-defined if the variables in s1(i) and s2(i) is disjoint

type solution = (var * int) list

solution assigns a value to each variable

val output_solutions : Stdlib.out_channel -> solution list -> unit

output_solutions o l outputs the list of solutions

val solve_and_enum : eqn list -> solution list

solve_and_enum l solves the system of equations and enumerate all the solutions

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct