package alt-ergo-lib

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

Module AltErgoLib.UtilSource

Sourceexception Timeout
Sourceexception Unsolvable
Sourceexception Cmp of int
Sourcemodule MI : Map.S with type key = int
Sourcemodule SS : Set.S with type elt = string
Sourcetype case_split_policy =
  1. | AfterTheoryAssume
  2. | BeforeMatching
  3. | AfterMatching

Different values for -case-split-policy option: -after-theory-assume (default value): after assuming facts in theory by the SAT -before-matching: just before performing a matching round -after-matching: just after performing a matching round *

Sourcetype inst_kind =
  1. | Normal
  2. | Forward
  3. | Backward
Sourcetype sat_solver =
  1. | Tableaux
  2. | Tableaux_CDCL
  3. | CDCL
  4. | CDCL_Tableaux
Sourcetype theories_extensions =
  1. | Sum
  2. | Adt
  3. | Arrays
  4. | Records
  5. | Bitv
  6. | LIA
  7. | LRA
  8. | NRA
  9. | NIA
  10. | FPA
Sourcetype axiom_kind =
  1. | Default
  2. | Propagator
Sourceval th_ext_of_string : string -> theories_extensions option
Sourceval string_of_th_ext : theories_extensions -> string
Sourceval compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int

generic function for comparing algebraic data types. compare_algebraic a b f

  • Pervasives.compare a b is used if
Sourceval cmp_lists : 'a list -> 'a list -> ('a -> 'a -> int) -> int
Sourcetype matching_env = {
  1. nb_triggers : int;
  2. triggers_var : bool;
  3. no_ematching : bool;
  4. greedy : bool;
  5. use_cs : bool;
  6. backward : inst_kind;
}
Sourceval print_list : sep:string -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
Sourceval print_list_pp : sep:(Format.formatter -> unit -> unit) -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> 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