package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/micromega_plugin/Micromega_plugin/Linsolve/index.html

Module `Micromega_plugin.Linsolve`Source

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