Module Sym

module Sym: sig  end

Function symbols
Author(s): Harald Ruess This module provides constructors for all the function symbols for the theories in {!Th.t}.

The set of function symbols is partitioned into uninterpreted and interpreted function symbols, and the interpreted function symbols are partitioned themselves into function symbols for the interpreted theories in Th.t of

linear arithmetic,
products,
coproducts,
bitvectors,
functional arrays,
power products, and
function abstraction and application.

In particular, function symbols from different theories are pairwise disjoint. Some theories contain an infinite number of function and constant symbols. For example, the theory of linear arithmetic contains a constant symbol for every rational number.

This module provides functions for creating, manipulating, and comparing function symbols. Since representations of function symbols are hashconsed, equality tests Sym.eq and comparison Sym.cmp are performed in constant time.

Symbols should only be constructed using the explicitly provided constructors as the definition of the type Sym.sym is only given to allow for convenient pattern matching.

Also, Tools.do_at_reset resets internal structures and therefore invalidates all uses of symbols. In particular, symbols should never be stored in global constants.

type t = sym * int

Representation type for function symbols. This includes the function symbol itself together with a hash value. This type is purposely not kept abstract as to allow for pattern matching.

type sym =

`\|`	`Uninterp of uninterp`
`\|`	`Arith of arith`
`\|`	`Product of product`
`\|`	`Coproduct of coproduct`
`\|`	`Bv of bv`
`\|`	`Pp of pprod`
`\|`	`Cl of cl`
`\|`	`Arrays of arrays`
`\|`	`Propset of propset`

type uninterp = Name.t

An uninterpreted function symbol in Th.u just consists of a name. There is no arity associated with it.

type arith =

`\|`	`Num of Mpa.Q.t`
`\|`	`Add`
`\|`	`Multq of Mpa.Q.t`

Function symbols for linear arithmetic Th.la are

Num(q) for representing rational number q,
Add for addition,
Multq(q) for multiplication by a rational q.

type product =

`\|`	`Cons`
`\|`	`Car`
`\|`	`Cdr`

Function symbols for the theory Th.p of products are

Cons for constructing pairs
Car for projection to first component
Cdr for projection to second component.

type coproduct =

`\|`	`In of direction`
`\|`	`Out of direction`

Function symbols for the theory Th.cop of cotuples are

In(Left) for left injection,
In(Right) for right injection,
Out(Right) for right unpacking,
Out(Left) for left unpacking.

type direction =

`\|`	`Left`
`\|`	`Right`

type arrays =

`\|`	`Create`
`\|`	`Select`
`\|`	`Update`

Function symbols of the theory Th.arr of arrays

Create for creating constant arrays,
Select for array lookup, and
Update for array update.

type cl =

`\|`	`Apply`
`\|`	`S`
`\|`	`K`
`\|`	`I`
`\|`	`C`
`\|`	`Reify of t * int`

Function symbols of the theory Th.app of functions

Apply of function application, and
combinators S, K, I

type propset =

`\|`	`Empty`
`\|`	`Full`
`\|`	`Ite`

type bv =

`\|`	`Const of Bitv.t`
`\|`	`Conc of int * int`
`\|`	`Sub of int * int * int`

Function symbols for the theory Th.bv of bitvectors are

Const(b) for constructing constant bitvectors such as 0111001.
Conc(n, m), for integers n, m >= 0, for concatenating bitvectors of width n and m,
Sub(i, j, n), for integers 0 <= i <= j < n, for extracting bits i through j in a bitvector of width n.

type pprod =

| Mult

Function symbols of the theory Th.nl of nonlinear arithmetic or power products are

Mult for nonlinear multiplication

type tsym = t

nickname

val theory_of : t -> Th.t

theory_of f returns the theory of type Th.t associated with f.

Parameters:

? : t

val eq : t -> t -> bool

eq f g succeeds iff f and g represent the same function symbol. This test is performed in constant time (in particular, independent of the length of names of uninterpreted function symbols).

Parameters:

f	:	`t`
g	:	`t`

val cmp : t -> t -> int

cmp f g returns 0 iff eq f g holds, and cmp f g is positive iff cmp g f is negative. Otherwise, the result is unspecified. cmp f g might thus be viewed as representing a total ordering <= on function symbols with f <= g iff cmp f g is, say, nonpositive.

Parameters:

f	:	`t`
g	:	`t`

val hash : t -> int

Nonnegative hash value for function symbols. This value is not unique to a function symbol.

Parameters:

? : t

val pp : 'a Pretty.printer -> (t * 'a list) Pretty.printer

Pretty-printing applications of symbols to an argument list. The exact form of printing applications is determined by the flag Pretty.flag. For details see also Sym.Uninterp.pp etc. below.

Parameters:

p	:	`'a Pretty.printer`
fmt	:	`Format.formatter`
((sym,()),al)	:	`(sym * 'b) * 'c list`

module Uninterp: sig  end

Operations on uninterpreted function symbols.

module Arith: sig  end

Operation on linear arithmetic function symbols.

module Product: sig  end

Operation on function symbols of the product theory Th.p.

module Coproduct: sig  end

Operation on function symbols of the coproduct theory Th.cop.

module Pprod: sig  end

Operation on function symbols of nonlinear multiplication theory Th.nl.

module Bv: sig  end

Operation on function symbols of the bitvector theory Th.bv.

module Array: sig  end

Operation on function symbols of the theory Th.arr of functional arrays.

module Cl: sig  end

Operation on function symbols of the theory Th.app of combinatory logic with case split.

module Propset: sig  end

Theory of propositional sets

val get : t -> sym

get f returns a theory-specific operator together with a tag for specifying the theory corresponding to f.

Parameters:

? : t