Uses of Interface
dev.civl.sarl.IF.config.ProverInfo

Packages that use ProverInfo

Package	Description
dev.civl.sarl	This is the root package for SARL, and contains the single class SARL.
dev.civl.sarl.IF.config	The config module provides a SARLConfig type, which encapsulates configuration information such as the list of available theorem provers with information on each.
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 ProverInfo in dev.civl.sarl

Methods in dev.civl.sarl with parameters of type ProverInfo

Modifier and Type	Method	Description
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.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.

Uses of ProverInfo in dev.civl.sarl.IF.config

Methods in dev.civl.sarl.IF.config that return ProverInfo

Modifier and Type	Method	Description
ProverInfo	SARLConfig.getProver(int index)	Gets the index-th theorem prover.
ProverInfo	SARLConfig.getProverWithAlias(String alias)	Finds a prover supported by this configuration with the given alias.
ProverInfo	SARLConfig.getProverWithKind(ProverInfo.ProverKind kind)	Finds a prover of the given kind supported by this configuration.

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

Modifier and Type	Method	Description
Iterable<ProverInfo>	SARLConfig.getProvers()	Returns all the provers supported by this configuration as an iterable sequence.

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

Modifier and Type	Method	Description
static SARLConfig	Configurations.newConfiguration(Collection<ProverInfo> provers)	Creates a new SARLConfig object based on the given list of prover information objects.

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

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

Modifier and Type	Method	Description
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 ProverInfo in dev.civl.sarl.universe.IF

Methods in dev.civl.sarl.universe.IF with parameters of type ProverInfo

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