Uses of Interface
dev.civl.sarl.preuniverse.IF.PreUniverse

Packages that use PreUniverse

Package	Description
dev.civl.sarl.preuniverse.IF	This package provides all of the functionality of a symbolic universe except reasoning.
dev.civl.sarl.prove.IF	Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.
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.
dev.civl.sarl.simplify.IF	Interfaces for the simplification of symbolic expressions.

Uses of PreUniverse in dev.civl.sarl.preuniverse.IF

Methods in dev.civl.sarl.preuniverse.IF that return PreUniverse

Modifier and Type	Method	Description
static PreUniverse	PreUniverses.newPreUniverse(FactorySystem system)

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

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

Modifier and Type	Method	Description
static TheoremProverFactory	Prove.newMultiProverFactory(PreUniverse universe, SARLConfig config, Path workingDirectory)	Constructs a new theorem prover factory based on the given configuration.
static TheoremProverFactory	Prove.newProverFactory(PreUniverse universe, ProverInfo prover, Path workingDirectory)	Constructs a new theorem prover factory based on a single underlying theorem prover.

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

Methods in dev.civl.sarl.reason.IF with parameters of type PreUniverse

Modifier and Type	Method	Description
static ReasonerFactory	Reason.newReasonerFactory(PreUniverse universe, IdealFactory idealFactory, TheoremProverFactory proverFactory)	Create a reasoner factory

Uses of PreUniverse in dev.civl.sarl.simplify.IF

Methods in dev.civl.sarl.simplify.IF with parameters of type PreUniverse

Modifier and Type	Method	Description
List<BooleanExpression>	ContextPartition.minimizeFor(SymbolicExpression expr, PreUniverse universe)	Returns a formula equivalent to or weaker than the original context but which can be used as the context for check validity or simplifying expr.
static ContextPartition	Simplify.newContextPartition(PreUniverse universe, List<BooleanExpression> contextStack)
BooleanExpression	Range.symbolicRepresentation(NumericExpression x, PreUniverse universe)	Given a NumericExpression x, returns a BooleanExpression which holds iff x is in this Range.