Module dev.civl.sarl

Package dev.civl.sarl.universe.IF

Class Universes

java.lang.Object

dev.civl.sarl.universe.IF.Universes

public class Universes
extends Object

This class provides static methods for the creation of new SymbolicUniverses.

Constructor Summary

Constructors

Constructor	Description
Universes()

Method Summary

Modifier and Type	Method	Description
static final Path	makeProverDir()	Creates a new directory to be used by theorem provers.
static SymbolicUniverse	newHerbrandUniverse()
static SymbolicUniverse	newHerbrandUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	newHerbrandUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)
static SymbolicUniverse	newHerbrandUniverse(Path workingDirectory)
static SymbolicUniverse	newIdealUniverse()
static SymbolicUniverse	newIdealUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	newIdealUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)
static SymbolicUniverse	newIdealUniverse(Path workingDirectory)
static SymbolicUniverse	newStandardUniverse()
static SymbolicUniverse	newStandardUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	newStandardUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)
static SymbolicUniverse	newStandardUniverse(Path workingDirectory)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

Universes

public Universes()

Method Details

makeProverDir

public static final Path makeProverDir()

Creates a new directory to be used by theorem provers. The new directory will be created in ./defaultProofDir, i.e., within a directory named defaultProofDir in the current working directory, where defaultProofDir is a string constant defined in SARLConstants.defaultProofDir. The directory ./defaultProofDir will be created if it does not already exist.

Returns:

the default working directory for provers

newIdealUniverse

public static SymbolicUniverse newIdealUniverse(SARLConfig config,
 ProverInfo prover,
 Path workingDirectory)

newIdealUniverse

public static SymbolicUniverse newIdealUniverse(SARLConfig config,
 ProverInfo prover)

newIdealUniverse

public static SymbolicUniverse newIdealUniverse(Path workingDirectory)

newIdealUniverse

public static SymbolicUniverse newIdealUniverse()

newHerbrandUniverse

public static SymbolicUniverse newHerbrandUniverse(SARLConfig config,
 ProverInfo prover,
 Path workingDirectory)

newHerbrandUniverse

public static SymbolicUniverse newHerbrandUniverse(SARLConfig config,
 ProverInfo prover)

newHerbrandUniverse

public static SymbolicUniverse newHerbrandUniverse(Path workingDirectory)

newHerbrandUniverse

public static SymbolicUniverse newHerbrandUniverse()

newStandardUniverse

public static SymbolicUniverse newStandardUniverse(SARLConfig config,
 ProverInfo prover,
 Path workingDirectory)

newStandardUniverse

public static SymbolicUniverse newStandardUniverse(SARLConfig config,
 ProverInfo prover)

newStandardUniverse

public static SymbolicUniverse newStandardUniverse(Path workingDirectory)

newStandardUniverse

public static SymbolicUniverse newStandardUniverse()