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

md5=35d6c6f3fa43bcd10fe7f524b1eb59ca

sha512=c3eee41d3c588ca89c2a1eebe9f10914ef647743b58fb562b682172cf6b6bdeb0920ebbba8a850820c0cb53bad0260f11b82fe71f00830ea9b33f5bb5d4fd048

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.

val type_parsed : 
  env ->
  env Stack.t ->
  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