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

sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba

sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb

module X : Theory.S

type t

type tbox = X.t

type instances = (Expr.gformula * Explanation.t) list

val empty : t

val add_terms : t -> Expr.Set.t -> Expr.gformula -> t

val add_lemma : t -> Expr.gformula -> Explanation.t -> t

val add_predicate : 
  t ->
  guard:Expr.t ->
  name:string ->
  Expr.gformula ->
  Explanation.t ->
  t

val ground_pred_defn : Expr.t -> t -> (Expr.t * Expr.t * Explanation.t) option

val pop : t -> guard:Expr.t -> t

val m_lemmas : 
  Util.matching_env ->
  t ->
  tbox ->
  (Expr.t -> Expr.t -> bool) ->
  int ->
  instances * instances

val m_predicates : 
  Util.matching_env ->
  t ->
  tbox ->
  (Expr.t -> Expr.t -> bool) ->
  int ->
  instances * instances

val register_max_term_depth : t -> int -> t

val matching_terms_info : 
  t ->
  Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t

val reinit_em_cache : unit -> unit

Reinitializes the E-matching functor instance's inner cache

On This Page