Previous  Up  Next

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
module Var: sig .. end
module VMap: Map.S  with type key = Var.t
type cst =
| CInt of Num.num
| CReal of Num.num
| CName of Hstring.t 
type poly = cst VMap.t * cst 
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.