package alt-ergo-lib

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

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.1.tbz
sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba
sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb

doc/alt-ergo-lib/AltErgoLib/Instances/Make/index.html

Module Instances.Make

Parameters

module X : Theory.S

Signature

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