Module dev.civl.sarl

Package dev.civl.sarl

Class SARL

java.lang.Object

dev.civl.sarl.SARL

public class SARL
extends Object

The SARL class provides static methods for creating new symbolic universes. (A symbolic universe provides methods for creating, manipulating, and reasoning about symbolic expressions that belong to that universe.) A typical user applications will call one of these static methods once, near the beginning of the execution, and use the universe returned for all symbolic expression operations.

Constructor Summary

Constructors

Constructor	Description
SARL()

Method Summary

Modifier and Type	Method	Description
static SymbolicUniverse	newIdealUniverse()
static SymbolicUniverse	newIdealUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	newIdealUniverse(SARLConfig config, ProverInfo prover, Path workingDirectory)	Returns a symbolic universe that only deals with ideal (mathematical) integers and reals.
static SymbolicUniverse	newIdealUniverse(Path workingDirectory)	Returns a symbolic universe that only deals with ideal (mathematical) integers and reals.
static SymbolicUniverse	newStandardUniverse()
static SymbolicUniverse	newStandardUniverse(SARLConfig config, ProverInfo prover)
static SymbolicUniverse	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	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.

Methods inherited from class java.lang.Object

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

Constructor Details

SARL

public SARL()

Method Details

newStandardUniverse

public static SymbolicUniverse 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.

Parameters:

config - a SARL configuration object providing information on the external theorem provers available to SARL

prover - either one of the ProverInfo objects in the configuration, or null. If non-null, this specifies the sole prover to use for resolving queries. If null, a query will be resolved by starting with the first prover in the configuration, and, if that result is inconclusive, going to the second, and so on, until either a conclusive result is achieved or every prover in the configuration has been exhausted.

Returns:

a new standard symbolic universe

newStandardUniverse

public static SymbolicUniverse newStandardUniverse(SARLConfig config,
 ProverInfo prover)

newIdealUniverse

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

Returns a symbolic universe that only deals with ideal (mathematical) integers and reals. There might be slight performance advantages over the standard universe (if no non-ideal expressions are used).

Parameters:

config - a SARL configuration object providing information on the external theorem provers available to SARL

prover - either one of the ProverInfo objects in the configuration, or null. If non-null, this specifies the sole prover to use for resolving queries. If null, a query will be resolved by starting with the first prover in the configuration, and, if that result is inconclusive, going to the second, and so on, until either a conclusive result is achieved or every prover in the configuration has been exhausted.

Returns:

an ideal symbolic universe

newIdealUniverse

public static SymbolicUniverse newIdealUniverse(SARLConfig config,
 ProverInfo prover)

newStandardUniverse

public static SymbolicUniverse 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.

The SARL configuration is determined by looking for a SARL configuration file. See

invalid reference

Configurations#findOrMakeConfiguration()

for details on how the configuration file is found.

A query will be resolved by starting with the first prover in the configuration, and, if that result is inconclusive, going to the second, and so on, until either a conclusive result is achieved or every prover in the configuration has been exhausted.

Returns:

a new standard symbolic universe

newStandardUniverse

public static SymbolicUniverse newStandardUniverse()

newIdealUniverse

public static SymbolicUniverse newIdealUniverse(Path workingDirectory)

Returns a symbolic universe that only deals with ideal (mathematical) integers and reals. There might be slight performance advantages over the standard universe (if no non-ideal expressions are used).

The SARL configuration is determined by looking for a SARL configuration file. See

invalid reference

Configurations#findOrMakeConfiguration()

for details on how the configuration file is found.

A query will be resolved by starting with the first prover in the configuration, and, if that result is inconclusive, going to the second, and so on, until either a conclusive result is achieved or every prover in the configuration has been exhausted.

Returns:

an ideal symbolic universe

newIdealUniverse

public static SymbolicUniverse newIdealUniverse()