package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module X : ALIEN

Signature

type t = X.r abstract

Type of terms of the theory

type r = X.r

Type of representants of terms of the theory

val name : string

Name of the theory

val is_mine_symb : Symbols.t -> Ty.t -> bool

return true if the symbol and the type are owned by the theory

val make : Expr.t -> r * Expr.t list

Give a representant of a term of the theory

val term_extract : r -> Expr.t option * bool
val color : r Sig.ac -> r
val type_info : t -> Ty.t
val embed : r -> t
val is_mine : t -> r
val leaves : t -> r list

Give the leaves of a term of the theory

val subst : r -> r -> t -> r
val compare : r -> r -> int
val equal : t -> t -> bool
val hash : t -> int

solve r1 r2, solve the equality r1=r2 and return the substitution

val solve : r -> r -> r Sig.solve_pb -> r Sig.solve_pb
val print : Stdlib.Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool
val abstract_selectors : t -> (r * r) list -> r * (r * r) list
val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string
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