Package edu.udel.cis.vsl.sarl.IF.config

Interface SARLConfig

All Known Implementing Classes:
CommonSARLConfig
public interface SARLConfig
A SARL configuration encapsulates information about the complete set of external theorem provers available to SARL.

  • Method Details

    • getNumProvers

      int getNumProvers()
      The number of theorem provers supported by this configuration.
      Returns:
      the number of theorem provers

    • getProver

      ProverInfo getProver(int index)
      Gets the index-th theorem prover.
      Parameters:
      index -
      Returns:
      the index-th prover

    • getProvers

      Iterable<ProverInfo> getProvers()
      Returns all the provers supported by this configuration as an iterable sequence.
      Returns:
      all provers supported by this configuration

    • getProverWithAlias

      ProverInfo getProverWithAlias(String alias)
      Finds a prover supported by this configuration with the given alias.
      Parameters:
      alias - the alias to search for
      Returns:
      a prover supported by this configuration with given alias or null if there is no such prover

    • getProverWithKind

      ProverInfo getProverWithKind(ProverInfo.ProverKind kind)
      Finds a prover of the given kind supported by this configuration.
      Parameters:
      kind - the kind to search for
      Returns:
      a prover supported by this configuration of the given kind, or null if there is no such prover

    • getWhy3ProvePlatform

      ProverInfo getWhy3ProvePlatform()
      Finds the why3 prove platform supported by this configuration
      Returns:
      The ProverInfo for why3 or null if there is no why3 prove platform.

    • setWhy3ProvePlatform

      void setWhy3ProvePlatform(ProverInfo why3Info)
      Set the why3 prove platform supported by this configuration
      Parameters:
      why3Info - An object contains all the informations of the why3 prove platform.

    • getOutputFileDir

      Path getOutputFileDir()
      Returns:
      the directory where SARL should put its generated temporary files in