package alt-ergo-lib

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

Module Fun_sat.MakeSource

Parameters

module Th : Theory.S

Signature

Sourcetype t
Sourceexception Sat of t
Sourceexception Unsat of Explanation.t
Sourceexception I_dont_know of t
Sourceval empty : unit -> t

the empty sat-solver context

Sourceval empty_with_inst : (Expr.t -> bool) -> t
Sourceval push : t -> int -> t

push env n add n new assertion levels. A guard g is added for every expression e assumed at the current assertion level. Ie. assuming e after the push will become g -> e, a g will be forced to be true (but not propagated at level 0)

Sourceval pop : t -> int -> t

pop env n remove an assertion level. Internally, the guard g introduced in the push correponsding to this pop will be propagated to false (at level 0)

Sourceval assume : t -> Expr.gformula -> Explanation.t -> t

assume env f assume a new formula f in env. Raises Unsat if f is unsatisfiable in env

Sourceval assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
Sourceval pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t

pred_def env f assume a new predicate definition f in env.

unsat env f size checks the unsatisfiability of f in env. Raises I_dont_know when the proof tree's height reaches size. Raises Sat if f is satisfiable in env

Sourceval print_model : header:bool -> Format.formatter -> t -> unit
Sourceval reset_refs : unit -> unit
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