| Ac |
Inference system for theories with single AC symbol
|
| Acsym |
Associative-commutative simplification
|
| App |
Operations on uninterpreted terms
|
| Apply |
Theory of lambda calculus.
|
| Arith |
Linear arithmetic.
|
| Arr |
Inference system for the theory
Th.arr of functional array
|
| Atom |
Atomic predicates.
|
| Bitv |
Bitvector constants.
|
| Bitvector |
Theory of bitvectors.
|
| Boolean |
Propositional logic
|
| Bv |
Inference system for bitvector theory
Th.bv.
|
| Can |
Inference system for canonizable, ground confluent theories.
|
| Clause |
Datatype of clauses
|
| Combine |
Combined inference system
|
| Context |
Logical contexts
|
| Cop |
Inference system for coproducts
|
| Coproduct |
Theory of coproducts
|
| D |
Disequality context.
|
| Dom |
Various subdomains of numbers.
|
| Euclid |
Module
Euclid: Euclidean solver for diophantine equations.
|
| Exc |
The module
Exc defines the exceptions for indicating
inconsistencies and validity.
|
| Fact |
Datatype of facts (justified atoms)
|
| Funarr |
Theory of arrays.
|
| G |
Global input facts.
|
| Infsys |
Definition and operations on inference systems.
|
| Jst |
Justifications
|
| L |
Equality sets for theory
L of combinatory logic
|
| La |
Linear arithmetic decision procedure
|
| Mpa |
Multi-precision arithmetic.
|
| Name |
Datatype of strings with constant equality
|
| Nl |
Inference system for the theory of nonlinear multiplication.
|
| P |
Shostak inference system for the theory of products
|
| Partition |
Variable partitioning.
|
| Pprod |
Theory of power products.
|
| Pretty |
Pretty-printing methods for various datatypes.
|
| Product |
Theory of products.
|
| Prop |
Propositional logic
|
| Propset |
Theory of propositional sets
|
| Pset |
Decision procedures for propositional sets
|
| Shostak |
Inference system for Shostak theories.
|
| Solution |
Solution sets.
|
| Sym |
Function symbols
|
| Term |
Datatype of terms
|
| Th |
Classification of function symbols
|
| Three |
Three-valued datatype.
|
| Tools |
Collection of useful functions used throughout ICS.
|
| Trace |
Rudimentary tracing capability.
|
| U |
Congruence closure
|
| V |
Context for handling equivalence classes of variables.
|
| Var |
Abstract datatype for variables.
|
| Version |
Version number
|