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

Packages that use SARLConfig

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 SARLConfig in dev.civl.sarl

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

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 SARLConfig in dev.civl.sarl.IF.config

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

Modifier and Type	Method	Description
static SARLConfig	Configurations.getDefaultConfiguration()	Looks for a SARL configuration file, and, if one is not found, creates one in the user's home directory.
static SARLConfig	Configurations.newConfiguration(File configFile)	Parses the specified SARL configuration file.
static SARLConfig	Configurations.newConfiguration(Collection<ProverInfo> provers)	Creates a new SARLConfig object based on the given list of prover information objects.

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

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

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.

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

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

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)