Uses of Interface
dev.civl.sarl.IF.Reasoner

Packages that use Reasoner

Package	Description
dev.civl.sarl.expr.IF	This package provides the internal interface for the representation of basic symbolic expressions.
dev.civl.sarl.IF	This package and its subpackages provide the "public interface" to SARL.
dev.civl.sarl.reason.IF	The internal interface for the "reason" module, which deals with Reasoners --- objects used to prove theorems and simplify symbolic expressions.

Uses of Reasoner in dev.civl.sarl.expr.IF

Methods in dev.civl.sarl.expr.IF with parameters of type Reasoner

Modifier and Type	Method	Description
SymbolicRange	SymbolicRangeFactory.tryUnion(Reasoner reasoner, SymbolicRange range0, SymbolicRange range1)	Attempts to create a single SymbolicRange which is equivalent to the union of the input SymbolicRanges range0 and range1.
SymbolicExpression	ExpressionFactory.valueSetElimWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr, SymbolicExpression elimExpr, NumericExpression lower, NumericExpression upper)
SymbolicExpression	ExpressionFactory.valueSetProtectiveWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArrM, SymbolicExpression refArrP)
SymbolicExpression	ExpressionFactory.valueSetWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr)	Apply a default widening operator to a value set template, which is in the form of an array of value set references and a symbolic type that is referred by these references.

Uses of Reasoner in dev.civl.sarl.IF

Methods in dev.civl.sarl.IF that return Reasoner

Modifier and Type	Method	Description
Reasoner	SymbolicUniverse.reasoner(BooleanExpression context)	Returns a Reasoner for the given context.
Reasoner	SymbolicUniverse.reasoner(List<BooleanExpression> contextStack)

Uses of Reasoner in dev.civl.sarl.reason.IF

Methods in dev.civl.sarl.reason.IF that return Reasoner

Modifier and Type	Method	Description
Reasoner	ReasonerFactory.getReasoner(BooleanExpression context, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates)	Gets a Reasoner for the given context.
Reasoner	ReasonerFactory.getReasoner(List<BooleanExpression> contextStack, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates)