Index of modules


A
Ac []
Inference system for theories with single AC symbol
Acsym []
Associative-commutative simplification
App [Term]
Operations on term applications.
App []
Operations on uninterpreted terms
Apply []
Theory of lambda calculus.
Arith [Sym]
Operation on linear arithmetic function symbols.
Arith []
Linear arithmetic.
Arr []
Inference system for the theory Th.arr of functional array
Array [Sym]
Operation on function symbols of the theory Th.arr of functional arrays.
Assignment [Prop]
Assignments for propositional formulas over literals including equalities and arithmetic inequalities.
Atom []
Atomic predicates.

B
Bitv []
Bitvector constants.
Bitvector []
Theory of bitvectors.
Boolean []
Propositional logic
Bv [Sym]
Operation on function symbols of the bitvector theory Th.bv.
Bv []
Inference system for bitvector theory Th.bv.

C
Can []
Inference system for canonizable, ground confluent theories.
Cl [Sym]
Operation on function symbols of the theory Th.app of combinatory logic with case split.
Clause []
Datatype of clauses
Cnstrnt [Var]
Variable constraints.
Combine []
Combined inference system
Config [Infsys]
A configuration (g; e; p) consists of Input facts g,, an equality set e, and, a variable partitioning p.
Context []
Logical contexts
Cop []
Inference system for coproducts
Coproduct [Sym]
Operation on function symbols of the coproduct theory Th.cop.
Coproduct []
Theory of coproducts

D
D []
Disequality context.
Dep [Solution.SET]
Iterators over dependency index.
Diseq [Fact]
Disequality Facts
Dom []
Various subdomains of numbers.

E
E [Combine]
Combination of individual equality sets.
Empty [Infsys]
Inference system for the empty theory.
Eqtrans [Jst]
Justifying equality Transformers
Equal [Term]
Following to be deprecated.
Equal [Fact]
Equality Facts
Euclid []
Module Euclid: Euclidean solver for diophantine equations.
Exc []
The module Exc defines the exceptions for indicating inconsistencies and validity.

F
Fact []
Datatype of facts (justified atoms)
Flat [Funarr]
Funarr []
Theory of arrays.

G
G []
Global input facts.

H
Hash [Name]
Hash table with names as keys.
Hash [Mpa.Q]

I
Infsys [U]
A congruence closure state represents the conjunction of a set of equalities x = f(x1,...,xn) with x, xi term variables and f an uninterpreted function symbol.
Infsys [Pset]
Inference system for the theory Th.set of products as described in module Propset.
Infsys [P]
Inference system for the theory Th.p of products as described in module Product.
Infsys [Nl]
Inference system for nonlinear multiplication as an extension of the AC inference system Ac.Make instantiated with the signature Pprod.Sig of nonlinear multiplication.
Infsys [La]
Inference system for linear arithmetic.
Infsys [L]
Tracing inference system.
Infsys []
Definition and operations on inference systems.
Infsys [Cop]
Inference system for the theory Th.cop of coproducts as defined in module Coproduct.
Infsys [Bv]
Inference system for the bitvector theory Th.bv as defined in module Bitvector.
Infsys [Arr]
Inference system for the theory Th.arr of extensional arrays as defined in module Funarr.
Infsys [Ac]
Inference system for a theory with a single AC symbol.

J
Jst []
Justifications

L
L []
Equality sets for theory L of combinatory logic
La []
Linear arithmetic decision procedure

M
Make [Solution]
Functor for constructing an equality set for theory specification T.
Make [Shostak]
Constructing an inference system from a Shostak theory Th.
Make [Euclid]
Functor building an implementation of the Euclid.S signature given an input structure Euclid.Rat isomorphic to the rationals.
Make [Can]
Constructing an inference system from the specification Can of a canonizable and ground confluent theory.
Make [Acsym]
Canonizer for a theory with one AC symbol, say *.
Make [Ac]
Canonizer for a theory with one AC symbol, say *.
Map [Term]
Maps with terms as keys.
Map [Term.Var]
Maplets with variables in the domain.
Map [Name]
Maps with names in the domain.
Map [Atom]
Maplets with atoms as keys.
Mode [Pretty]
Pretty-printing modes.
Mode [Jst]
Proof Mode
Mode [Context]
Pretty-printing mode for processing.
Monomials [Arith]
Iterators over monomials.
Mpa []
Multi-precision arithmetic.

N
Name []
Datatype of strings with constant equality
Neg [Arith.Monomials]
Iterators over negative monomials.
Nl []
Inference system for the theory of nonlinear multiplication.
Nonneg [Fact]
Nonnegativity facts

O
Ops [Nl]
Various operations with a set of flat equalities of the form u = x * y as context.
Ops [Can]
Operations on canonizable theories.
Ops [Arr]
Various operations with a set of flat equalities of the form u = x * y as context.
Ops [Ac]
Various operations on flat equalities.

P
P []
Shostak inference system for the theory of products
Partition []
Variable partitioning.
Pos [Fact]
Nonnegativity facts
Pos [Arith.Monomials]
Iterators over positive monomials.
Pprod [Sym]
Operation on function symbols of nonlinear multiplication theory Th.nl.
Pprod []
Theory of power products.
Pred [Jst]
Justifying predicates over terms.
Pred2 [Jst]
Justifying predicates over pair of terms.
Pretty []
Pretty-printing methods for various datatypes.
Product [Sym]
Operation on function symbols of the product theory Th.p.
Product []
Theory of products.
Proj [Solution]
Projecting out extensions of a solution set.
Prop []
Propositional logic
Propset [Sym]
Theory of propositional sets
Propset []
Theory of propositional sets
Pset []
Decision procedures for propositional sets

Q
Q [Mpa]
Multi-precision rationals.

R
Rel1 [Jst]
Justifying ternary relations over terms.
Rel2 [Jst]
Justifying ternary relations over pairs of terms.

S
S [U]
S [La]
States s consist of two solution sets (r, t) with r the regular solution set with equalities of the form x = a with x a nonslack variable (see Term.Var.is_slack) and a a linear arithmetic term., t a tableau with equalities k = b with k a slack variable, and all variables in the linear arithmetic term b are slack variables, too. A state s represents the conjunction of equalities in r and t.
Set [Th]
Set [Term]
Set of terms.
Set [Term.Var]
Sets of variables.
Set [Solution]
Functor for constructing a solution set for theory specification T0.
Set [Name]
Sets of names.
Set [Fact.Diseq]
Set [D]
Set of disequal terms together with justifications.
Set [Atom]
Sets of atoms.
Set2 [Term]
Set of pair of terms.
Shostak []
Inference system for Shostak theories.
Sig [Pprod]
Solution []
Solution sets.
Status [Context]
Result of processing.
Subst [Term]
Term Substitutions
Sym []
Function symbols

T
T [Ac]
Specification of a theory with a single AC symbol by means of canonizers and ground completion functions.
Term []
Datatype of terms
Th []
Classification of function symbols
Three []
Three-valued datatype.
Three [Jst]
Justifying ternary relations.
Tools []
Collection of useful functions used throughout ICS.
Trace []
Rudimentary tracing capability.
Trace [Infsys]
Tracing rule applications.
TraceArith [Infsys]
Tracing rule applications.

U
U []
Congruence closure
Uninterp [Sym]
Operations on uninterpreted function symbols.

V
V []
Context for handling equivalence classes of variables.
Var []
Abstract datatype for variables.
Var [Term]
Operations on term variables.
Version []
Version number

Z
Z [Mpa]
Multi-precision integers.