Module Syntax

module Syntax: sig .. end
Defines Formulas, Terms, Symbols, Types, and Contexts. Syntactic manipulation of terms and formulas.

type 'a context 
A context manages symbols and sharing between expressions. context is a phantom type: the 'a type parameter ensures that expressions don't cross contexts.
module Env: sig .. end
Environments are maps whose domain is a set of free variable symbols.
type typ_arith = [ `TyInt | `TyReal ] 

Types


type typ_fo = [ `TyBool | `TyInt | `TyReal ] 
type typ = [ `TyBool | `TyFun of typ_fo list * typ_fo | `TyInt | `TyReal ] 
type typ_bool = [ `TyBool ] 
type 'a typ_fun = [ `TyFun of typ_fo list * 'a ] 
val pp_typ : Format.formatter -> [< typ ] -> unit

Symbols


type symbol 
Symbols are represented as non-negative integers, but the type definition is hidden. The isomorphism is witnessed by int_of_symbol and symbol_of_int.
val mk_symbol : 'a context -> ?name:string -> typ -> symbol
val register_named_symbol : 'a context -> string -> typ -> unit
Register a named symbol. The strings identifying named symbols must be unique. The symbol associated with a name can be retrieved with get_named_symbol.
val is_registered_name : 'a context -> string -> bool
Test if a name is already associated with a symbol
val get_named_symbol : 'a context -> string -> symbol
Retrieve the symbol associated with a given name. Raises Not_found if there is no such symbol.
val symbol_name : 'a context -> symbol -> string option
Retrieve the name of a named symbol. Evaluates to None for ordinary (non-named) symbols.
val pp_symbol : 'a context -> Format.formatter -> symbol -> unit
val typ_symbol : 'a context -> symbol -> typ
val show_symbol : 'a context -> symbol -> string
val int_of_symbol : symbol -> int
val symbol_of_int : int -> symbol
val compare_symbol : symbol -> symbol -> int
module Symbol: sig .. end

Expressions


type ('a, +'typ) expr 
type 'a term = ('a, typ_arith) expr 
type 'a formula = ('a, typ_bool) expr 
val compare_expr : ('a, 'typ) expr -> ('a, 'typ) expr -> int
val compare_formula : 'a formula -> 'a formula -> int
val compare_term : 'a term -> 'a term -> int
val destruct : 'a context ->
('a, 'b) expr ->
[ `Add of 'a term list
| `And of 'a formula list
| `App of symbol * ('a, typ_fo) expr list
| `Atom of [ `Eq | `Leq | `Lt ] * 'a term * 'a term
| `Binop of [ `Div | `Mod ] * 'a term * 'a term
| `Fls
| `Ite of 'a formula * ('a, 'b) expr * ('a, 'b) expr
| `Mul of 'a term list
| `Not of 'a formula
| `Or of 'a formula list
| `Proposition of
[ `App of symbol * ('b, typ_fo) expr list
| `Var of int ]
| `Quantify of
[ `Exists | `Forall ] * string * typ_fo * 'a formula
| `Real of QQ.t
| `Tru
| `Unop of [ `Floor | `Neg ] * 'a term
| `Var of int * typ_arith ]
val expr_typ : 'a context -> ('a, 'b) expr -> typ
val free_vars : ('a, 'b) expr -> (int, typ_fo) BatHashtbl.t
val size : ('a, 'b) expr -> int
val mk_const : 'a context -> symbol -> ('a, 'typ) expr
val mk_app : 'a context ->
symbol -> ('a, 'b) expr list -> ('a, 'typ) expr
val mk_var : 'a context -> int -> typ_fo -> ('a, 'typ) expr
val mk_ite : 'a context ->
'a formula ->
('a, 'typ) expr -> ('a, 'typ) expr -> ('a, 'typ) expr
val mk_if : 'a context ->
'a formula -> 'a formula -> 'a formula
val mk_iff : 'a context ->
'a formula -> 'a formula -> 'a formula
val substitute : 'a context ->
(int -> ('a, 'b) expr) ->
('a, 'typ) expr -> ('a, 'typ) expr
val substitute_const : 'a context ->
(symbol -> ('a, 'b) expr) ->
('a, 'typ) expr -> ('a, 'typ) expr
val substitute_map : 'a context ->
('a, 'b) expr Symbol.Map.t ->
('a, 'typ) expr -> ('a, 'typ) expr
val fold_constants : (symbol -> 'a -> 'a) -> ('b, 'c) expr -> 'a -> 'a
val symbols : ('a, 'b) expr -> Symbol.Set.t

Expression rewriting


type 'a rewriter = ('a, typ_fo) expr -> ('a, typ_fo) expr 
A rewriter is a function that transforms an expression into another. The transformation should preserve types; if not, rewrite will fail.
val rewrite : 'a context ->
?down:'a rewriter ->
?up:'a rewriter -> ('a, 'typ) expr -> ('a, 'typ) expr
Rewrite an expression. The down rewriter is applied to each expression going down the expression tree, and the up rewriter is applied to each expression going up the tree.
val nnf_rewriter : 'a context -> 'a rewriter
Convert to negation normal form (down pass).
module Expr: sig .. end

Terms


type ('a, 'b) open_term = [ `Add of 'a list
| `App of symbol * ('b, typ_fo) expr list
| `Binop of [ `Div | `Mod ] * 'a * 'a
| `Ite of 'b formula * 'a * 'a
| `Mul of 'a list
| `Real of QQ.t
| `Unop of [ `Floor | `Neg ] * 'a
| `Var of int * typ_arith ]
val mk_add : 'a context -> 'a term list -> 'a term
val mk_mul : 'a context -> 'a term list -> 'a term
val mk_div : 'a context -> 'a term -> 'a term -> 'a term
val mk_pow : 'a context -> 'a term -> int -> 'a term
val mk_idiv : 'a context -> 'a term -> 'a term -> 'a term
C99 integer division. Equivalent to truncate(x/y).
val mk_mod : 'a context -> 'a term -> 'a term -> 'a term
val mk_real : 'a context -> QQ.t -> 'a term
val mk_floor : 'a context -> 'a term -> 'a term
val mk_ceiling : 'a context -> 'a term -> 'a term
val mk_truncate : 'a context -> 'a term -> 'a term
truncate(t) removes the fractional part of t (rounding it towards 0).
val mk_neg : 'a context -> 'a term -> 'a term
Unary negation
val mk_sub : 'a context -> 'a term -> 'a term -> 'a term
Subtraction
val term_typ : 'a context -> 'a term -> typ_arith
module Term: sig .. end

Formulas


type ('a, 'b) open_formula = [ `And of 'a list
| `Atom of [ `Eq | `Leq | `Lt ] * 'b term * 'b term
| `Fls
| `Ite of 'a * 'a * 'a
| `Not of 'a
| `Or of 'a list
| `Proposition of
[ `App of symbol * ('b, typ_fo) expr list
| `Var of int ]
| `Quantify of [ `Exists | `Forall ] * string * typ_fo * 'a
| `Tru ]
val mk_forall : 'a context ->
?name:string -> typ_fo -> 'a formula -> 'a formula
val mk_exists : 'a context ->
?name:string -> typ_fo -> 'a formula -> 'a formula
val mk_forall_const : 'a context -> symbol -> 'a formula -> 'a formula
val mk_exists_const : 'a context -> symbol -> 'a formula -> 'a formula
val mk_and : 'a context -> 'a formula list -> 'a formula
val mk_or : 'a context -> 'a formula list -> 'a formula
val mk_not : 'a context -> 'a formula -> 'a formula
val mk_eq : 'a context -> 'a term -> 'a term -> 'a formula
val mk_lt : 'a context -> 'a term -> 'a term -> 'a formula
val mk_leq : 'a context -> 'a term -> 'a term -> 'a formula
val mk_true : 'a context -> 'a formula
val mk_false : 'a context -> 'a formula
val eliminate_ite : 'a context -> 'a formula -> 'a formula
val pp_smtlib2 : ?env:string Env.t ->
'a context -> Format.formatter -> 'a formula -> unit
Print a formula as a satisfiability query in SMTLIB2 format. The query includes function declarations and (check-sat).
module Formula: sig .. end

Contexts


module type Context = sig .. end
module MakeContext: 
functor (* : sig
end) -> Context
module MakeSimplifyingContext: 
functor (* : sig
end) -> Context
Create a context which simplifies expressions on the fly
module Infix: 
functor (C : sig
type t 
val context : t Syntax.context
end) -> sig .. end
module ContextTable: sig .. end
A context table is a hash table mapping contents to values.