Module Ast_smtlib

module Ast_smtlib: sig .. end

AST requirement for the Smtlib format. The smtlib format is widely used among SMT solvers, and is the language of the smtlib benchmark library. Terms are expressed as s-expressions, and top-level directives include everything needed to use a prover in an interactive loop (so it includes directive for getting and setting options, getting information about the solver's internal model, etc...)

module type Id = sig .. end

module type Term = sig .. end

module type Statement = sig .. end