package alt-ergo-lib

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

Module Shostak.AdtSource

Type of terms of the theory

Type of representants of terms of the theory

Sourceval name : string

Name of the theory

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

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

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

Give a representant of a term of the theory

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

Give the leaves of a term of the theory

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

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

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