package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Micromega_plugin.LinsolveSource

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).

Sourcetype system
Sourcetype var = int

var is the type of variables

Sourcetype id = int

id are used to identify equations in a system

Sourcetype eqn

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

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

output_equations o l prints the list of equations

Sourceval empty : system

empty is the system with no equation

Sourceval 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

Sourceval 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

Sourceval 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

Sourcetype solution = (var * int) list

solution assigns a value to each variable

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

output_solutions o l outputs the list of solutions

Sourceval 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