Class

ap.AbstractFileProver

Translation

Related Doc: package AbstractFileProver

Permalink

class Translation extends AnyRef

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

Attributes
protected
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Translation
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Translation(rawFormula: IFormula, settings: GlobalSettings)

    Permalink

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. def XtoIFormula(c: Conjunction, onlyNonTheory: Boolean = false): IFormula

    Permalink

  5. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any

  6. lazy val canUseModelSearchProver: Boolean

    Permalink

  7. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )

  8. def constructProofTree(name: String): (ProofTree, Boolean)

    Permalink

  9. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef

  10. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  11. def findCounterModelTimeout(f: Seq[Conjunction]): Either[Conjunction, Certificate]

    Permalink

  12. def findCounterModelTimeout: Either[Conjunction, Certificate]

    Permalink

  13. def findModel(f: Conjunction): Conjunction

    Permalink

  14. def findModelTimeout: Either[Conjunction, Certificate]

    Permalink

  15. lazy val formulaConstants: Set[ConstantTerm]

    Permalink

  16. lazy val formulaQuantifiers: Set[Quantifier]

    Permalink

  17. val formulas: Seq[Conjunction]

    Permalink

  18. val functionEncoder: FunctionEncoder

    Permalink

  19. val gcedFunctions: Set[Predicate]

    Permalink

  20. def getAssumedFormulaParts(cert: Certificate): Set[PartName]

    Permalink

  21. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  22. def getFormulaParts: Map[PartName, Conjunction]

    Permalink

  23. def getInputFormulaParts: Map[PartName, IFormula]

    Permalink

  24. def getPredTranslation: Map[Predicate, IFunction]

    Permalink

  25. val goalSettings: GoalSettings

    Permalink

  26. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  27. val ignoredQuantifiers: Boolean

    Permalink

  28. val ignoredQuantifiers2: Boolean

    Permalink

  29. val incompletePreproc: Boolean

    Permalink

  30. val inputFormulas: List[INamedPart]

    Permalink

  31. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  32. val matchedTotalFunctions: Boolean

    Permalink

  33. val namedParts: Map[PartName, Conjunction]

    Permalink

  34. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef

  35. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  36. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  37. val order: TermOrder

    Permalink

  38. val preprocInterpolantSpecs: List[IInterpolantSpec]

    Permalink

  39. def processConstraint(c: Conjunction): IFormula

    Permalink

  40. def processInterpolant(c: Conjunction): IFormula

    Permalink

  41. def processModel(c: Conjunction): IFormula

    Permalink

  42. lazy val soundForSat: Boolean

    Permalink

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

    Permalink
    Definition Classes
    AnyRef

  44. val theories: Seq[Theory]

    Permalink

  45. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

  46. val transSignature: Signature

    Permalink

  47. final def wait(arg0: Long, arg1: Int): Unit

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

  48. final def wait(arg0: Long): Unit

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

  49. 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 AnyRef

Inherited from Any

Ungrouped