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

sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388

md5=3b060044767d16d1de3416944abd2dd5

Sourcetype env

The type of global environment of the typechecker.

Sourceval empty_env : env

The empty/initial environment

val type_expr : 
  env ->
  (Symbols.t * Ty.t) list ->
  Parsed.lexpr ->
  int Typed.atterm

Typecheck an input expression (i.e. term (or formula ?)), given a local environment and a list of local types used to extend the initial environment.

Sourceval type_parsed : env -> Parsed.decl -> int Typed.atdecl list * env

Type a single declaration.

Sourceval type_file : Parsed.file -> (int Typed.atdecl * env) list * env

Type an input file. Returns the successive global environments obtained after typing each declaration.

val split_goals : 
  (int Typed.atdecl * 'a) list ->
  ((int Typed.atdecl * 'a) list * string) list

val split_goals_and_cnf : 
  (int Typed.atdecl * 'a) list ->
  (Commands.sat_tdecl list * string) list