Index of types

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.

Function symbols of the theory Th.arr of arrays Create for creating constant arrays,, Select for array lookup, and, Update for array update.

An atomic predicate is either one of the constants True or False,, an equality a = b,, a disequality a <> b, or , an arithmetic inequality a > 0 or a >= 0.

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.

Function symbols of the theory Th.app of functions Apply of function application, and, combinators S, K, I

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.

Extension field.

Nickname.

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

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.

Rationals.

Facts are partitioned into facts over variable terms, facts over pure terms with all function symbols drawn from a single theory i, facts over mixed terms.

Representation type for variables.

Elements of t represent conjunctions of variable equalities.

There is an implicit partial ordering with Yes < X and No < X.

Representation type for function symbols.

Type t for representing a partitioning consists of a set of variable equalities of type V.t, a set of variable disequalities of type D.t The variable disequalities are always kept in canonical form w.r.t the variable equalities.

Representation of strings with constant time equality.

Abstract type of rationals.

Abstract type of integers.

Representation of a set of equalities of the form rho |- x = a, where x is a variable, a a non-variable term, and rho is a justification of the equality x = a.

Set of input facts of type Fact.t.

A fact is an atom together with a justification (proof) of this atom in terms of axioms.

Elements of type D.t represent sets of variable disequalities.

Representation of logical contexts.

Combined equality set.

Configurations (g, e, p) for the combined inference system consist of a global input g,, a combined euqality set e, and, a variable partition p.

For each atom, a unique index is maintained.

Synonym for avoiding name clashes

nickname

An uninterpreted function symbol in Th.u just consists of a name.