Packages

c

edu.cmu.cs.ls.keymaerax.lemma

FileLemmaDB

class FileLemmaDB extends LemmaDBBase with Logging

File-based lemma DB implementation. Stores one lemma per file in the user's KeYmaera X home directory under cache/lemmadb/. Lemma file names are created automatically and in a thread-safe manner.

Note

Prefer LemmaDBFactory.lemmaDB over instantiating directly to get an instance of a lemma database and ensure thread safety. Created by smitsch on 4/27/15.

Linear Supertypes
Logging, LemmaDBBase, LemmaDB, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. FileLemmaDB
  2. Logging
  3. LemmaDBBase
  4. LemmaDB
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new FileLemmaDB()

Type Members

  1. type LemmaID = String
    Definition Classes
    LemmaDB

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def add(lemma: Lemma): LemmaID

    Adds a new lemma to this lemma DB, with a unique name or None, which will automatically assign a name.

    Adds a new lemma to this lemma DB, with a unique name or None, which will automatically assign a name.

    lemma

    The lemma whose Provable will be inserted under its name.

    returns

    Internal lemma identifier.

    Definition Classes
    LemmaDBBaseLemmaDB
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  7. def contains(lemmaID: LemmaID): Boolean

    Indicates whether or not this lemma DB contains a lemma with the specified ID.

    Indicates whether or not this lemma DB contains a lemma with the specified ID.

    lemmaID

    Identifies the lemma.

    returns

    True, if this lemma DB contains a lemma with the specified ID; false otherwise.

    Definition Classes
    LemmaDB
  8. def createLemma(): LemmaID

    Creates an identifier for a lemma, without any content.

    Creates an identifier for a lemma, without any content.

    Definition Classes
    FileLemmaDBLemmaDBBase
  9. def deleteDatabase(): Unit

    Delete the whole lemma database

    Delete the whole lemma database

    Definition Classes
    FileLemmaDBLemmaDB
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  12. def escapeSeparator(str: String): String
  13. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. def flatOpt[T](L: List[Option[T]]): Option[List[T]]

    Turns a list of options into a list or to a None if any list element was None.

    Turns a list of options into a list or to a None if any list element was None. For convenience when implementing bulk get() from individual get()

    Attributes
    protected
    Definition Classes
    LemmaDBBase
  15. def get(ids: List[LemmaID]): Option[List[Lemma]]
    Definition Classes
    LemmaDBBaseLemmaDB
  16. def get(lemmaID: LemmaID): Option[Lemma]

    Returns the lemma with the given name or None if non-existent.

    Returns the lemma with the given name or None if non-existent.

    lemmaID

    Identifies the lemma.

    returns

    The lemma, if found under the given lemma ID. None otherwise.

    Definition Classes
    LemmaDB
  17. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  18. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  19. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  20. val logger: Logger
    Attributes
    protected
    Definition Classes
    Logging
  21. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  23. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. def readLemmas(ids: List[LemmaID]): Option[List[String]]

    Reads the lemma content of the lemmas ids.

    Reads the lemma content of the lemmas ids. None if any of the ids does not exist.

    Definition Classes
    FileLemmaDBLemmaDBBase
  25. def remove(id: String): Unit

    Delete the lemma of the given identifier, throwing exceptions if that was unsuccessful.

    Delete the lemma of the given identifier, throwing exceptions if that was unsuccessful.

    Definition Classes
    FileLemmaDBLemmaDB
  26. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  27. def toString(): String
    Definition Classes
    AnyRef → Any
  28. def version(): String

    Returns the version of this lemma database.

    Returns the version of this lemma database.

    Definition Classes
    FileLemmaDBLemmaDB
  29. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  31. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  32. def writeLemma(id: LemmaID, lemma: String): Unit

    Write the string representation lemma of a lemma under the name id.

    Write the string representation lemma of a lemma under the name id.

    Definition Classes
    FileLemmaDBLemmaDBBase

Inherited from Logging

Inherited from LemmaDBBase

Inherited from LemmaDB

Inherited from AnyRef

Inherited from Any

Ungrouped