Class/Object

ap

AbstractFileProver

Related Docs: object AbstractFileProver | package ap

Permalink

abstract class AbstractFileProver extends Prover

Linear Supertypes
Prover, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. AbstractFileProver
  2. Prover
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new AbstractFileProver(reader: Reader, output: Boolean, timeout: Int, userDefStoppingCond: ⇒ Boolean, settings: GlobalSettings)

    Permalink

Type Members

  1. class Translation extends AnyRef

    Permalink

    Class taking care of pre-processing, and translation to internal data-structures.

    Class taking care of pre-processing, and translation to internal data-structures.

    Attributes
    protected

Abstract Value Members

  1. abstract val result: Result

    Permalink
    Definition Classes
    Prover
  2. abstract val usedTranslation: Translation

    Permalink
    Attributes
    protected

Concrete Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. object AllExVisitor extends ContextAwareVisitor[Unit, Unit]

    Permalink

    Visitor to check whether a formula is in the forall-exists fragment (when proving that the formula is valid)

    Visitor to check whether a formula is in the forall-exists fragment (when proving that the formula is valid)

    Attributes
    protected
  5. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  6. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )
  7. val constructProofs: Boolean

    Permalink
  8. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  10. def getAssumedFormulaParts(cert: Certificate): Set[PartName]

    Permalink
    Definition Classes
    AbstractFileProverProver
  11. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  12. def getFormulaParts: Map[PartName, Conjunction]

    Permalink
    Definition Classes
    AbstractFileProverProver
  13. def getInputFormulaParts: Map[PartName, IFormula]

    Permalink
    Definition Classes
    AbstractFileProverProver
  14. def getPredTranslation: Map[Predicate, IFunction]

    Permalink
    Definition Classes
    AbstractFileProverProver
  15. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  16. def inputFormulas: List[INamedPart]

    Permalink
  17. def interpolantSpecs: List[IInterpolantSpec]

    Permalink
  18. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  19. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  20. lazy val negTranslation: Translation

    Permalink
    Attributes
    protected
  21. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  22. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  23. lazy val posTranslation: Translation

    Permalink
    Attributes
    protected
  24. def println(str: ⇒ String): Unit

    Permalink
    Attributes
    protected
  25. def println(obj: Any): Unit

    Permalink
    Attributes
    protected
  26. lazy val rawConstants: Set[ConstantTerm]

    Permalink
  27. val rawInputFormula: IFormula

    Permalink
  28. val rawInterpolantSpecs: List[IInterpolantSpec]

    Permalink
  29. lazy val rawQuantifiers: Set[Quantifier]

    Permalink
  30. val rawSignature: Signature

    Permalink
  31. def signature: Signature

    Permalink
  32. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  33. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  34. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  36. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from Prover

Inherited from AnyRef

Inherited from Any

Ungrouped