Uses of Interface
dev.civl.sarl.IF.expr.SymbolicConstant

Packages that use SymbolicConstant

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.IF.expr	The public interface package dealing with symbolic expressions.
dev.civl.sarl.prove.IF	Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.

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

Methods in dev.civl.sarl.expr.IF that return SymbolicConstant

Modifier and Type	Method	Description
SymbolicConstant	ExpressionFactory.symbolicConstant(StringObject name, SymbolicType type)

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

Modifier and Type	Method	Description
BooleanExpression	BooleanExpressionFactory.exists(SymbolicConstant boundVariable, BooleanExpression predicate)	Returns the existentially quantified expression exists(x).e.
BooleanExpression	BooleanExpressionFactory.forall(SymbolicConstant boundVariable, BooleanExpression predicate)	Returns the universally quantified expression forall(x).e.

Uses of SymbolicConstant in dev.civl.sarl.IF

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

Modifier and Type	Method	Description
SymbolicConstant	CoreUniverse.symbolicConstant(StringObject name, SymbolicType type)	Returns the SymbolicConstant with the given name and type.

Methods in dev.civl.sarl.IF that return types with arguments of type SymbolicConstant

Modifier and Type	Method	Description
Map<SymbolicConstant,SymbolicExpression>	Reasoner.constantSubstitutionMap()	In the process of simplifying the initial context, this simplifier may have "solved" for some of the symbolic constants occurring in the context.
Set<SymbolicConstant>	CoreUniverse.getFreeSymbolicConstants(SymbolicExpression expr)	Returns the set of unbound symbolic constants occurring in an expression.
Map<SymbolicConstant,SymbolicExpression>	ModelResult.getModel()	Returns the model, a map assigning a concrete symbolic expression value to each symbolic constant occurring in the query.

Methods in dev.civl.sarl.IF with parameters of type SymbolicConstant

Modifier and Type	Method	Description
Interval	Reasoner.assumptionAsInterval(SymbolicConstant symbolicConstant)	If the context can be represented as a simple interval constraint, i.e., an expression of the form A invalid input: '<'= x invalid input: '<'= B, where A and B are concrete numbers, x is the given symbolic constant, and invalid input: '<'= could be invalid input: '<' in either case, this returns the interval [A,B] (or (A,B], or, ...).
BooleanExpression	CoreUniverse.exists(SymbolicConstant boundVariable, BooleanExpression predicate)	Returns the existentially quantified expression exists(x).e.
BooleanExpression	CoreUniverse.forall(SymbolicConstant boundVariable, BooleanExpression predicate)	Returns the universally quantified expression forall(x).e.
SymbolicExpression	CoreUniverse.lambda(SymbolicConstant boundVariable, SymbolicExpression expression)	Returns the lambda expression lambda(x).e, i.e., the expression representing the function which given x returns e, where e might possibly involve the variable x.
UnaryOperator<SymbolicExpression>	CoreUniverse.simpleSubstituter(SymbolicConstant var, SymbolicExpression value)	Returns a substituter that replaces a specific symbolic constant with some specific value.

Method parameters in dev.civl.sarl.IF with type arguments of type SymbolicConstant

Modifier and Type	Method	Description
void	Reasoner.aggressivelySimplifyTopContext(Set<SymbolicConstant> aggressiveSet)
CanonicalRenamer	CoreUniverse.canonicalRenamer(String root, Predicate<SymbolicConstant> ignore)	Returns an operator on SymbolicExpressions that replaces all symbolic constants (including bound ones) with symbolic constants with unique canonical names.
UnaryOperator<SymbolicExpression>	CoreUniverse.constantSubstituter(Map<SymbolicConstant,SymbolicExpression> map)	Returns a substituter for which the base substitutions are specified by an explicit Java Map.
<T extends SymbolicExpression> T	Reasoner.simplify(T expression, Set<SymbolicConstant> aggressiveSet)

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

Subinterfaces of SymbolicConstant in dev.civl.sarl.IF.expr

Modifier and Type	Interface	Description
interface	BooleanSymbolicConstant	A SymbolicConstant of boolean type.
interface	NumericSymbolicConstant	A SymbolicConstant which has integer or real type, i.e., type belonging to SymbolicIntegerType or SymbolicRealType.

Methods in dev.civl.sarl.IF.expr that return types with arguments of type SymbolicConstant

Modifier and Type	Method	Description
Set<SymbolicConstant>	SymbolicExpression.getFreeVars()	Get the set of free variables occurring in this symbolic expression.

Uses of SymbolicConstant in dev.civl.sarl.prove.IF

Fields in dev.civl.sarl.prove.IF declared as SymbolicConstant

Modifier and Type	Field	Description
final SymbolicConstant	ProverFunctionInterpretation.function
final SymbolicConstant[]	ProverFunctionInterpretation.parameters

Methods in dev.civl.sarl.prove.IF with parameters of type SymbolicConstant

Modifier and Type	Method	Description
static ProverFunctionInterpretation	ProverFunctionInterpretation.newProverPredicate(SymbolicUniverse universe, String identifier, SymbolicConstant[] parameters, SymbolicExpression definition)

Method parameters in dev.civl.sarl.prove.IF with type arguments of type SymbolicConstant

Modifier and Type	Method	Description
static ModelResult	Prove.modelResult(Map<SymbolicConstant,SymbolicExpression> model)	Constructs a new ModelResult wrapping the given mapping from symbolic constants to symbolic expressions.