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

Dune Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

O

OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.3.tar.gz

sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388

md5=3b060044767d16d1de3416944abd2dd5

doc/alt-ergo-lib/AltErgoLib/Util/index.html

Module `AltErgoLib.Util`Source

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 =

| AfterTheoryAssume
| BeforeMatching
| 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 =

| Normal
| Forward
| Backward

Sourcetype sat_solver =

| Tableaux
| Tableaux_CDCL
| CDCL
| CDCL_Tableaux

Sourcetype theories_extensions =

| Sum
| Adt
| Arrays
| Records
| Bitv
| LIA
| LRA
| NRA
| NIA
| FPA

Sourcetype axiom_kind =

| Default
| 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 = {

nb_triggers : int;
triggers_var : bool;
no_ematching : bool;
greedy : bool;
use_cs : bool;
backward : inst_kind;

}

Source

val print_list : 
  sep:string ->
  pp:(Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a list ->
  unit