package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

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

Authors

  1. A
    Alt-Ergo developers

Maintainers

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