Class/Object

ap.interpolants

InterpolationContext

Related Docs: object InterpolationContext | package interpolants

Permalink

class InterpolationContext extends AnyRef

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

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 addCommon(commons: Iterable[CertFormula]): InterpolationContext

    Permalink

  5. def addCommon(common: CertFormula): InterpolationContext

    Permalink

  6. def addConstants(consts: Seq[ConstantTerm]): InterpolationContext

    Permalink

  7. def addDoubleConstant(const: ConstantTerm, d1: ConstantTerm, d2: ConstantTerm): InterpolationContext

    Permalink

  8. def addDoubleConstants(consts: Iterator[ConstantTerm]): Iterator[ConstantTerm]

    Permalink

  9. def addDoubleConstants(consts: Iterable[ConstantTerm]): Iterator[ConstantTerm]

    Permalink

  10. def addLeft(lefts: Iterable[CertFormula]): InterpolationContext

    Permalink

  11. def addLeft(left: CertFormula): InterpolationContext

    Permalink

  12. def addParameter(const: ConstantTerm): InterpolationContext

    Permalink

  13. def addPartialInterpolant(literal: CertArithLiteral, partialInter: PartialInterpolant): InterpolationContext

    Permalink

  14. def addRight(rights: Iterable[CertFormula]): InterpolationContext

    Permalink

  15. def addRight(right: CertFormula): InterpolationContext

    Permalink

  16. lazy val allConstants: Set[ConstantTerm]

    Permalink

  17. lazy val allPredicates: Set[Predicate]

    Permalink

  18. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any

  19. def clone(): AnyRef

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

  20. lazy val commonFormulaConstants: Set[ConstantTerm]

    Permalink

  21. lazy val commonFormulaPredicates: Set[Predicate]

    Permalink

  22. val commonFormulae: Set[CertFormula]

    Permalink

  23. val doubleConstants: Map[ConstantTerm, (ConstantTerm, ConstantTerm)]

    Permalink

  24. lazy val doubleConstantsSubst: Substitution

    Permalink

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

    Permalink
    Definition Classes
    AnyRef

  26. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  28. def getPIConverseFormula(literal: CertArithLiteral): Formula

    Permalink

  29. def getPartialInterpolant(literal: CertArithLiteral): PartialInterpolant

    Permalink

  30. def getPredAtomRewriting(rewrittenLit: CertPredLiteral): (Seq[Seq[(IdealInt, CertEquation)]], CertPredLiteral)

    Permalink

  31. lazy val globalConstants: Set[ConstantTerm]

    Permalink

  32. lazy val globalPredicates: Set[Predicate]

    Permalink

  33. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  34. def isCommon(conj: CertFormula): Boolean

    Permalink

  35. def isFromLeft(conj: CertFormula): Boolean

    Permalink

  36. def isFromRight(conj: CertFormula): Boolean

    Permalink

  37. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  38. def isRewrittenLeftLit(lit: CertPredLiteral): Boolean

    Permalink

  39. def isRewrittenRightLit(lit: CertPredLiteral): Boolean

    Permalink

  40. val leftConstants: Set[ConstantTerm]

    Permalink

  41. val leftFormulae: Set[CertFormula]

    Permalink

  42. lazy val leftLocalConstants: Set[ConstantTerm]

    Permalink

  43. lazy val leftLocalPredicates: Set[Predicate]

    Permalink

  44. lazy val leftPredicates: Set[Predicate]

    Permalink

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

    Permalink
    Definition Classes
    AnyRef

  46. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  47. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  48. val order: TermOrder

    Permalink

  49. val parameters: Set[ConstantTerm]

    Permalink

  50. val partialInterpolants: Map[CertArithLiteral, PartialInterpolant]

    Permalink

  51. def rewritePredAtom(equations: Seq[Seq[(IdealInt, CertEquation)]], targetLit: CertPredLiteral, result: CertPredLiteral): InterpolationContext

    Permalink

  52. val rightConstants: Set[ConstantTerm]

    Permalink

  53. val rightFormulae: Set[CertFormula]

    Permalink

  54. lazy val rightLocalConstants: Set[ConstantTerm]

    Permalink

  55. lazy val rightPredicates: Set[Predicate]

    Permalink

  56. def setOrder(newOrder: TermOrder): InterpolationContext

    Permalink

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

    Permalink
    Definition Classes
    AnyRef

  58. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

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

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

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

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

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