Packages

t

edu.cmu.cs.ls.keymaerax.hydra

DBAbstraction

trait DBAbstraction extends AnyRef

Proof database

Linear Supertypes
AnyRef, Any
Known Subclasses
InMemoryDB, SQLiteDB
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DBAbstraction
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def addAgendaItem(proofId: Int, initialProofNode: ProofTreeNodeId, displayName: String): Int
  2. abstract def addAlternative(alternativeTo: Int, inputProvable: ProvableSig, trace: ExecutionTrace): Unit

    Truncate the execution trace at the beginning of alternativeTo and replace it with trace.

  3. abstract def addBelleExpr(expr: BelleExpr): Int

    Adds a bellerophon expression as an executable and returns the new executableId

  4. abstract def addExecutionStep(step: ExecutionStepPOJO): Int

    Adds an execution step to an existing execution

    Adds an execution step to an existing execution

    Note

    Implementations should enforce additional invarants -- never insert when branches or alt orderings overlap.

  5. abstract def addModelTactic(modelId: String, tactic: String): Option[Int]

    Adds a tactic script to the model

  6. abstract def agendaItemsForProof(proofId: Int): List[AgendaItemPOJO]
  7. abstract def checkPassword(username: String, password: String): Boolean
  8. abstract def cleanup(): Unit

    Initializes a new database.

  9. abstract def createModel(userId: String, name: String, fileContents: String, date: String, description: Option[String] = None, publink: Option[String] = None, title: Option[String] = None, tactic: Option[String] = None): Option[Int]

    Creates a new model in the database if name does not exist yet.

    Creates a new model in the database if name does not exist yet. Returns the ID of the created model. Otherwise (if the model name is used already) returns None and the database is unmodified.

  10. abstract def createProof(provable: ProvableSig): Int

    Create a temporary proof without model, starting from 'provable'.

  11. abstract def createProofForModel(modelId: Int, name: String, description: String, date: String, tactic: Option[String]): Int
  12. abstract def createProvable(p: ProvableSig): Int

    Stores a Provable in the database and returns its ID

  13. abstract def createUser(username: String, password: String, group: String): Unit

    Creates a new user, identified by the unique username with password.

    Creates a new user, identified by the unique username with password. The user belongs to group group.

  14. abstract def deleteExecutionStep(proofId: Int, stepId: Int): Unit

    Delete an execution step.

  15. abstract def deleteModel(modelId: Int): Boolean

    Deletes this model and all associated proofs.

  16. abstract def deleteProof(proofId: Int): Boolean

    Deletes the proof.

  17. abstract def deleteProofSteps(proofId: Int): Int

    Deletes the recorded proof steps, but keeps the proof and its tactic.

    Deletes the recorded proof steps, but keeps the proof and its tactic. Returns the number of deleted steps.

  18. abstract def deleteProvable(provableId: Int): Boolean

    Deletes a provable and all associated sequents / formulas

  19. abstract def getAgendaItem(proofId: Int, initialProofNode: ProofTreeNodeId): Option[AgendaItemPOJO]
  20. abstract def getAllConfigurations: Set[ConfigurationPOJO]
  21. abstract def getConfiguration(configName: String): ConfigurationPOJO
  22. abstract def getExecutable(executableId: Int): ExecutablePOJO

    Returns the executable with ID executableId

  23. abstract def getExecutionStep(proofId: Int, stepId: Int): Option[ExecutionStep]

    Returns the execution step with id stepId of proof proofId with all provables etc.

    Returns the execution step with id stepId of proof proofId with all provables etc. filled in.

  24. abstract def getExecutionSteps(executionId: Int): List[ExecutionStepPOJO]

    Return a list of all finished execution steps in the current history of the execution, in the order in which they occurred.

    Return a list of all finished execution steps in the current history of the execution, in the order in which they occurred.

    Note

    For most purposes, getExecutionTrace is more convenient, but slower.

  25. abstract def getExecutionTrace(proofID: Int, withProvables: Boolean = true): ExecutionTrace

    Return the sequence of steps that led to the current state of the proof.

    Return the sequence of steps that led to the current state of the proof. Loading a trace with provables is slow.

  26. abstract def getFirstExecutionStep(proofId: Int): Option[ExecutionStepPOJO]

    Returns the first step of the proof

  27. abstract def getInvariants(modelId: Int): Map[Expression, Formula]
  28. abstract def getModel(modelId: Int): ModelPOJO
  29. abstract def getModelList(userId: String): List[ModelPOJO]
  30. abstract def getPlainExecutionStep(proofId: Int, stepId: Int): Option[ExecutionStepPOJO]

    Returns the execution step with id stepId of proof proofId in plain database form.

  31. abstract def getPlainOpenSteps(proofId: Int): List[(ExecutionStepPOJO, List[Int])]

    Returns a list of steps that do not have successors for each of their subgoals.

    Returns a list of steps that do not have successors for each of their subgoals. Along with each step, it lists the step's subgoals that are actually closed.

  32. abstract def getPlainStepSuccessors(proofId: Int, prevStepId: Int, branchOrder: Int): List[ExecutionStepPOJO]

    Returns the successors of the execution step with id stepId of proof proofId in plain database form.

  33. abstract def getProofInfo(proofId: Int): ProofPOJO
  34. abstract def getProofsForModel(modelId: Int): List[ProofPOJO]
  35. abstract def getProofsForUser(userId: String): List[(ProofPOJO, String)]
  36. abstract def getProvable(provableId: Int): ProvablePOJO

    Reconstruct a stored Provable

  37. abstract def getStepProvable(proofId: Int, stepId: Option[Int], subgoal: Option[Int]): Option[ProvableSig]

    Returns the subgoal of execution step stepId of proof proofId; proof conclusion if both None.

  38. abstract def getTempUsers: List[UserPOJO]

    Returns all temporary users (group 3).

  39. abstract def getUniqueModelName(userId: String, modelName: String): String

    Returns a unique model name by appending an index, if modelName already exists.

  40. abstract def getUser(username: String): Option[UserPOJO]

    Returns the user identified by username, if any.

  41. abstract def isProofClosed(proofId: Int): Boolean
  42. abstract def proofExists(proofId: Int): Boolean
  43. abstract def syncDatabase(): Unit

    Ensures any changes which might currently reside in auxilliary storage have been synced to main storage.

  44. abstract def updateAgendaItem(item: AgendaItemPOJO): Unit
  45. abstract def updateConfiguration(config: ConfigurationPOJO): Unit
  46. abstract def updateExecutionStep(executionStepId: Int, step: ExecutionStepPOJO): Unit

    Update existing execution step.

  47. abstract def updateModel(modelId: Int, name: String, title: Option[String], description: Option[String], content: Option[String], tactic: Option[String]): Unit
  48. abstract def updateProofInfo(proof: ProofPOJO): Unit
  49. abstract def userExists(username: String): Boolean
  50. abstract def userOwnsProof(userId: String, proofId: String): Boolean

    Indicates whether or not the user userId owns the proof proofId.

Concrete 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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. def createProofForModel(modelId: String, name: String, description: String, date: String, tactic: Option[String]): String
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. def getModel(modelId: String): ModelPOJO
  12. def getProofInfo(proofId: String): ProofPOJO
  13. def getProofsForModel(modelId: String): List[ProofPOJO]
  14. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  19. def openProofs(userId: String): List[ProofPOJO]
  20. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  21. def toString(): String
    Definition Classes
    AnyRef → Any
  22. def updateProofName(proofId: String, name: String): Unit
  23. def updateProofName(proofId: Int, name: String): Unit
  24. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  25. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped