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.