Package edu.udel.cis.vsl.sarl

Class SARL

java.lang.Object
edu.udel.cis.vsl.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 Details

    • SARL

      public SARL()

  • Method Details

    • newStandardUniverse

      public static SymbolicUniverse newStandardUniverse(SARLConfig config, ProverInfo prover)
      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

    • newIdealUniverse

      public static SymbolicUniverse newIdealUniverse(SARLConfig config, ProverInfo prover)
      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

    • newStandardUniverse

      public static SymbolicUniverse newStandardUniverse()

      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 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

    • newIdealUniverse

      public static SymbolicUniverse newIdealUniverse()

      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 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