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

Packages that use SymbolicUniverse

Package	Description
dev.civl.sarl	This is the root package for SARL, and contains the single class SARL.
dev.civl.sarl.prove.IF	Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.
dev.civl.sarl.universe.IF	Internal interface for the "universe" module.

Uses of SymbolicUniverse in dev.civl.sarl

Methods in dev.civl.sarl that return SymbolicUniverse

Modifier and Type	Method	Description
static SymbolicUniverse	SARL.newIdealUniverse()
static SymbolicUniverse	SARL.newIdealUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	SARL.newIdealUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)	Returns a symbolic universe that only deals with ideal (mathematical) integers and reals.
static SymbolicUniverse	SARL.newIdealUniverse(Path workingDirectory)	Returns a symbolic universe that only deals with ideal (mathematical) integers and reals.
static SymbolicUniverse	SARL.newStandardUniverse()
static SymbolicUniverse	SARL.newStandardUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	SARL.newStandardUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)	Returns a new standard symbolic universe, which supports all symbolic types, including Herbrand integer and real types, and ideal (mathematical) integers and reals.
static SymbolicUniverse	SARL.newStandardUniverse(Path workingDirectory)	Returns a new standard symbolic universe, which supports all symbolic types, including Herbrand integer and real types, and ideal (mathematical) integers and reals.

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

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

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

Uses of SymbolicUniverse in dev.civl.sarl.universe.IF

Methods in dev.civl.sarl.universe.IF that return SymbolicUniverse

Modifier and Type	Method	Description
static SymbolicUniverse	Universes.newHerbrandUniverse()
static SymbolicUniverse	Universes.newHerbrandUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	Universes.newHerbrandUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)
static SymbolicUniverse	Universes.newHerbrandUniverse(Path workingDirectory)
static SymbolicUniverse	Universes.newIdealUniverse()
static SymbolicUniverse	Universes.newIdealUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	Universes.newIdealUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)
static SymbolicUniverse	Universes.newIdealUniverse(Path workingDirectory)
static SymbolicUniverse	Universes.newStandardUniverse()
static SymbolicUniverse	Universes.newStandardUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	Universes.newStandardUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)
static SymbolicUniverse	Universes.newStandardUniverse(Path workingDirectory)