All Packages

Package Summary
This is the root package for SARL, and contains the single class SARL.
Implementation of the configuration classes specified in package
This package deals with the represention of boolean symbolic expressions in a conjunctive normal form.
Implementation classes for generic symbolic expressions, symbolic expression factories, and a comparator on symbolic expressions.
This package provides the internal interface for the representation of basic symbolic expressions.
Implementation classes for the herbrand module.
This package provides the internal interface supporting Herbrand arithmetic, i.e., arithmetic in which all operations are treated as uninterpreted operations.
Implementation classes for the ideal2 module.
The ideal module supports reasoning about numerical expressions using "ideal" mathematical reals and integers.
This package and its subpackages provide the "public interface" to SARL.
The config module provides a SARLConfig type, which encapsulates configuration information such as the list of available theorem provers with information on each.
The public interface package dealing with symbolic expressions.
The number package supports infinite-precision integer and rational numbers.
The object package provides the SymbolicObject interface, which is the root of the symbolic object type hierarchy.
The type package provides interfaces for all of the symbolic types.
A utility package supporting infinite precision integer and rational numbers, and a variety of arithmetic operations on them.
An implementation of the number module.
Implementation of the symbolic object module, specified in and
Internal interface for the symbolic object module, providing mechanisms for creating SymbolicObjects.
This package provides the implementation of PreUniverse module.
This package provides all of the functionality of a symbolic universe except reasoning.
This package provides implementation classes common to all theorem provers.
This package provides implementations of the TheoremProver and TheoremProverFactory interfaces based on the CVC3 and CVC4 theorem provers.
Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.
This package provides implementations of the TheoremProver and TheoremProverFactory interfaces based on Microsoft's Z3 theorem prover.
Some generic implementations of the Reasoner interface and the interfaces of
The internal interface for the "reason" module, which deals with Reasoners --- objects used to prove theorems and simplify symbolic expressions.
Partial and full implementations of simplification interfaces specified in
Interfaces for the simplification of symbolic expressions.
This package implements the main simplifier, which is based around a Context.
Implementations of the interfaces specified in and
Internal interface for the "type" module, providing a SymbolicTypeFactory for producing SymbolicType s.
Implementations of SymbolicUniverses.
Internal interface for the "universe" module.
General utility classes used throughout SARL.