Package edu.udel.cis.vsl.sarl.reason.common

package edu.udel.cis.vsl.sarl.reason.common

Some generic implementations of the Reasoner interface and the interfaces of edu.udel.cis.vsl.sarl.reason.IF.

Classes

Class	Description
ArrayLambdaCanonicalization	Briefly, this transformer canonicalizes all bound variable names of the lambda expressions in array lambdas.
CommonReasoner	A very basic implementation of Reasoner based on a given Simplifier and TheoremProverFactory.
CommonReasonerFactory	Basic factory for producing instances of CommonReasoner.
ContextMinimizingReasoner	A Reasoner based on context minimization.
ContextMinimizingReasonerFactory	A factory for producing instances of ContextMinimizingReasoner.
ReasonerCacheKey	The key of cached Reasoners which is a pair of a BooleanExpression which represents the context and an array of ProverFunctionInterpretation
SimpleReasoner	Very basic reasoner that does not use any theorem prover, only simplification.
StatefulSigmaAdaptor	Transform sigma (sum) expressions to the forms that are accepted by all provers
TaylorSubstituter	A substituter that replaces certain function calls with their truncated Taylor polynomial expansions.
Why3ReasonerFactory	A factory that generates new Why3Reasoners.