Module dev.civl.sarl
Package dev.civl.sarl.IF.config

Interface ProverInfo

All Superinterfaces:
Comparable<ProverInfo>
public interface ProverInfo extends Comparable<ProverInfo>
Abstract interface representing information about an external theorem prover: what kind of prover it is, where it can be found, etc.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Interface
    Description
    static enum 
    ProverInfo.ProverKind
    A classification of the different kinds of theorem provers.

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    addAlias(String value)
    Adds the given string to the set of aliases.
    void
    addOption(String value)
    Adds the given string to the end of the list of options.
    Set<String>
    getAliases()
    Returns the set of aliases associated to this theorem prover.
    String
    getFirstAlias()
    Returns one of the alias strings in the set of aliases.
    ProverInfo.ProverKind
    getKind()
    The kind of theorem prover this is.
    List<String>
    getOptions()
    Returns the sequence of command line options that should be used when invoking this theorem prover.
    File
    getPath()
    The path to the executable theorem prover.
    boolean
    getShowErrors()
    Should the prover print a message every time the underlying theorem prover reports an error? (In any case, the error is interpreted as an inconclusive result.)
    boolean
    getShowInconclusives()
    Should the prover print a message every time it reports an inconclusive result?
    boolean
    getShowQueries()
    Should the prover print all the queries?
    double
    getTimeout()
    Returns time limit in seconds or -1 if the time is unlimited.
    String
    getVersion()
    The version, e.g.
    void
    print(PrintStream out)
    Prints a complete representation of this object in the format that is expected in a SARL configuration file.
    void
    setKind(ProverInfo.ProverKind value)
    Sets the prover kind.
    void
    setPath(File value)
    Sets the path to the executable theorem prover.
    void
    setShowErrors(boolean value)
    Sets whether the prover prints a message every time the underlying theorem prover reports an error.
    void
    setShowInconclusives(boolean value)
    Sets whether the prover prints a message every time it reports an inconclusive result.
    void
    setShowQueries(boolean value)
    Tell this prover whether it should print every query.
    void
    setTimeout(double value)
    Sets the timeout, i.e., the time limit in seconds.
    void
    setVersion(String value)
    Sets the version string.

    Methods inherited from interface java.lang.Comparable

    compareTo

  • Method Details

    • getAliases

      Set<String> getAliases()
      Returns the set of aliases associated to this theorem prover. The set should not be modified.
      Returns:
      the set of aliases associated to this theorem prover

    • getFirstAlias

      String getFirstAlias()
      Returns one of the alias strings in the set of aliases.
      Returns:
      an alias string

    • addAlias

      boolean addAlias(String value)
      Adds the given string to the set of aliases.
      Parameters:
      value - the string to add to the set of aliases
      Returns:
      true if the set of aliases did not already contain the given value

    • getOptions

      List<String> getOptions()
      Returns the sequence of command line options that should be used when invoking this theorem prover.
      Returns:
      list of command line options

    • addOption

      void addOption(String value)
      Adds the given string to the end of the list of options.
      Parameters:
      value - the string to add

    • getTimeout

      double getTimeout()
      Returns time limit in seconds or -1 if the time is unlimited.
      Returns:
      time limit in seconds

    • setTimeout

      void setTimeout(double value)
      Sets the timeout, i.e., the time limit in seconds.
      Parameters:
      value - the time limit in seconds or -1 if the time is unlimited

    • getKind

      ProverInfo.ProverKind getKind()
      The kind of theorem prover this is. This is a classification by kind of input language the prover expects.
      Returns:
      kind of this prover

    • setKind

      void setKind(ProverInfo.ProverKind value)
      Sets the prover kind.
      Parameters:
      value - the prover kind

    • getPath

      File getPath()
      The path to the executable theorem prover. This should be an absolute path to an executable file.
      Returns:
      path to executable

    • setPath

      void setPath(File value)
      Sets the path to the executable theorem prover. This should be an absolute path to an executable file.
      Parameters:
      value -

    • getVersion

      String getVersion()
      The version, e.g. "1.4".
      Returns:
      version string

    • setVersion

      void setVersion(String value)
      Sets the version string.
      Parameters:
      value - the version string

    • getShowQueries

      boolean getShowQueries()
      Should the prover print all the queries?
      Returns:
      true if this prover should print queries

    • setShowQueries

      void setShowQueries(boolean value)
      Tell this prover whether it should print every query.
      Parameters:
      value - true if this prover should print queries

    • getShowInconclusives

      boolean getShowInconclusives()
      Should the prover print a message every time it reports an inconclusive result?
      Returns:
      true if a message should be printed for every inconclusive result

    • setShowInconclusives

      void setShowInconclusives(boolean value)
      Sets whether the prover prints a message every time it reports an inconclusive result.
      Parameters:
      value - true if a message should be printed for every inconclusive result

    • getShowErrors

      boolean getShowErrors()
      Should the prover print a message every time the underlying theorem prover reports an error? (In any case, the error is interpreted as an inconclusive result.)
      Returns:
      true if a message should be printed for every error

    • setShowErrors

      void setShowErrors(boolean value)
      Sets whether the prover prints a message every time the underlying theorem prover reports an error. (In any case, the error is interpreted as an inconclusive result.)
      Type Parameters:
      code - true if a message should be printed for every error

    • print

      void print(PrintStream out)
      Prints a complete representation of this object in the format that is expected in a SARL configuration file.
      Parameters:
      out - where to print