Module `AltErgoLib.Util`

exception Timeout

exception Unsolvable

exception Cmp of int

exception Not_implemented of string

module MI : Map.S with type key = int

module SI : Set.S with type elt = int

module SS : Set.S with type elt = string

type 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 *

type inst_kind =

| Normal
| Forward
| Backward

type sat_solver =

| Tableaux
| Tableaux_CDCL
| CDCL
| CDCL_Tableaux

val pp_sat_solver : Format.formatter -> sat_solver -> unit

type theories_extensions =

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

type axiom_kind =

| Default
| Propagator

val th_ext_of_string : string -> theories_extensions option

val string_of_th_ext : theories_extensions -> string

val compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int

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

Stdlib.compare a b is used if

val cmp_lists : 'a list -> 'a list -> ('a -> 'a -> int) -> int

type matching_env = {

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

}

val loop : f:(int -> 'a -> 'b -> 'b) -> max:int -> elt:'a -> init:'b -> 'b

Loops from 0 to max and returns (f max elt ... (f 1 elt (f 0 elt init)))...). Returns init if max < 0

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

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

val failwith : ('a, Format.formatter, unit, 'b) format4 -> 'a

val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `AltErgoLib.Util`

package alt-ergo-lib

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module AltErgoLib.Util

Module `AltErgoLib.Util`