package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Mc = Micromega
val use_simplex : unit -> bool

use_simplex is bound to the Coq option Simplex. If set, use the Simplex method, otherwise use Fourier

type ('prf, 'model) res =
  1. | Prf of 'prf
  2. | Model of 'model
  3. | Unknown
type zres = (Mc.zArithProof, int * Mc.z list) res
type qres = (Mc.q Mc.psatz, int * Mc.q list) res

q_cert_of_pos prf converts a Sos proof into a rational Coq proof

z_cert_of_pos prf converts a Sos proof into an integer Coq proof

val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres

lia enum depth sys generates an unsat proof for the linear constraints in sys. If the Simplex option is set, any failure to find a proof should be considered as a bug.

val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres

nlia enum depth sys generates an unsat proof for the non-linear constraints in sys. The solver is incomplete -- the problem is undecidable

val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres

linear_prover_with_cert depth sys generates an unsat proof for the linear constraints in sys. Over the rationals, the solver is complete.

val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres

nlinear depth sys generates an unsat proof for the non-linear constraints in sys. The solver is incompete -- the problem is decidable.

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