package alt-ergo-lib

  1. Overview
  2. Docs

Parameters

module Th : Theory.S

Signature

type t
exception Bottom of Explanation.t * Expr.Set.t list * t
val empty : unit -> t
val is_true : t -> Expr.t -> (Explanation.t Lazy.t * int) option
val assume : bool -> t -> (Expr.gformula * Explanation.t) list -> t
val decide : t -> Expr.t -> int -> t
val forget_decision : t -> Expr.t -> int -> t
val reset_decisions : t -> t
val get_decisions : t -> (int * Expr.t) list
OCaml

Innovation. Community. Security.