package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

Dune Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

O

OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.1.tar.gz

sha256=0fd6594f30d4e2bea97350a7906ecc2528c37e8fdd32588818a162aacc409688

md5=a0e9dda8f17c1f4f03119badd24d1bf5

doc/alt-ergo-lib/AltErgoLib/Arith/Shostak/argument-2-P/index.html

Parameter `Shostak.P`

include Polynome.T with type r = X.r

type r = X.r

type t

val compare : t -> t -> int

val equal : t -> t -> bool

val hash : t -> int

val create : (Numbers.Q.t * r) list -> Numbers.Q.t -> Ty.t -> t

val add : t -> t -> t

val sub : t -> t -> t

val mult : t -> t -> t

val mult_const : Numbers.Q.t -> t -> t

val add_const : Numbers.Q.t -> t -> t

val div : t -> t -> t * bool

val modulo : t -> t -> t

val is_const : t -> Numbers.Q.t option

val is_empty : t -> bool

val find : r -> t -> Numbers.Q.t

val choose : t -> Numbers.Q.t * r

val subst : r -> t -> t -> t

val remove : r -> t -> t

val to_list : t -> (Numbers.Q.t * r) list * Numbers.Q.t

val leaves : t -> r list

val print : Format.formatter -> t -> unit

val type_info : t -> Ty.t

val is_monomial : t -> (Numbers.Q.t * r * Numbers.Q.t) option

val ppmc_denominators : t -> Numbers.Q.t

val pgcd_numerators : t -> Numbers.Q.t

val normal_form : t -> t * Numbers.Q.t * Numbers.Q.t

val normal_form_pos : t -> t * Numbers.Q.t * Numbers.Q.t

val abstract_selectors : t -> (r * r) list -> t * (r * r) list

val separate_constant : t -> t * Numbers.Q.t

val extract : r -> t option

val embed : t -> r