Packages

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. Protected

Instance Constructors

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

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 XtoIFormula(c: Conjunction, onlyNonTheory: Boolean = false): IFormula
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. lazy val canUseModelSearchProver: Boolean
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  8. def constructProofTree(name: String): (ProofTree, Boolean)
  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  11. def findCounterModelTimeout(f: Seq[Conjunction]): Either[Conjunction, Certificate]
  12. def findCounterModelTimeout: Either[Conjunction, Certificate]
  13. def findModel(f: Conjunction): Conjunction
  14. def findModelTimeout: Either[Conjunction, Certificate]
  15. lazy val formulaConstants: Set[ConstantTerm]
  16. lazy val formulaQuantifiers: Set[Quantifier]
  17. val formulas: Seq[Conjunction]
  18. val functionEncoder: FunctionEncoder
  19. val gcedFunctions: Set[Predicate]
  20. def getAssumedFormulaParts(cert: Certificate): Set[PartName]
  21. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  22. def getFormulaParts: Map[PartName, Conjunction]
  23. def getInputFormulaParts: Map[PartName, IFormula]
  24. def getPredTranslation: Map[Predicate, IFunction]
  25. val goalSettings: GoalSettings
  26. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  27. val ignoredQuantifiers: Boolean
  28. val ignoredQuantifiers2: Boolean
  29. val incompletePreproc: Boolean
  30. val inputFormulas: List[INamedPart]
  31. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  32. val matchedTotalFunctions: Boolean
  33. val namedParts: Map[PartName, Conjunction]
  34. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  35. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  36. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  37. val order: TermOrder
  38. val preprocInterpolantSpecs: List[IInterpolantSpec]
  39. def processConstraint(c: Conjunction): IFormula
  40. def processInterpolant(c: Conjunction): IFormula
  41. def processModel(c: Conjunction): IFormula
  42. lazy val soundForSat: Boolean
  43. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  44. val theories: Seq[Theory]
  45. def toString(): String
    Definition Classes
    AnyRef → Any
  46. val transSignature: Signature
  47. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  48. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  49. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped