Module Types (.ml)

module Types: sig .. end
Terms, atoms and conjunctions


Terms


type sort = 
| Glob (*global variable*)
| Constr (*constructor*)
| Var (*variable of the paramterized domain*)
sort of single symbol
type const = 
| ConstInt of Num.num
| ConstReal of Num.num
| ConstName of Hstring.t
constant: it can be an integer, a real or a constant name
module MConst: sig .. end
val compare_constants : int MConst.t -> int MConst.t -> int
val add_constants : int MConst.t -> int MConst.t -> int MConst.t
val const_sign : int MConst.t -> int option
val const_nul : int MConst.t -> bool
val mult_const : int -> int MConst.t -> int MConst.t
type term = 
| Const of int MConst.t (*constant given as a map. 1*2 + 3*c is the map [2 -> 1; c -> 3]*)
| Elem of Hstring.t * sort (*element, can be a variable or a process*)
| Access of Hstring.t * Variable.t list (*an access to an array*)
| Arith of term * int MConst.t (*arithmetic term: Arith (t, c) is the term t + c*)
the type of terms
module Term: sig .. end
Module interface for terms

Atoms


type op_comp = 
| Eq (*equality, =*)
| Lt (*comparison less than, <*)
| Le (*comparison less or equal, <=*)
| Neq (*disequality, <>*)
comparison operators for litterals
module Atom: sig .. end
Interface for the atoms of the language

Conjunctions


module SAtom: sig .. end
Interface for the conjunctions of atoms seen as sets of atoms.
module ArrayAtom: sig .. end
Interface for the conjunctions of atoms seen as arrays of atoms.