abstract class SoftwareInterpolationFramework extends AnyRef
Abstract class providing some functionality commonly needed for interpolation-based software verification, e.g., axioms and prover for bitvector arithmetic, arrays, etc.
- Alphabetic
- By Inheritance
- SoftwareInterpolationFramework
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new SoftwareInterpolationFramework()
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def dumpInterpolationProblem(transitionParts: Map[PartName, Conjunction], sig: Signature): Unit
- Attributes
- protected
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- val frameworkVocabulary: FrameworkVocabulary
- Attributes
- protected
- def genInterpolants(formulas: Seq[Conjunction], commonFormula: Conjunction, order: TermOrder): Either[Conjunction, Iterator[Conjunction]]
- Attributes
- protected
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- var interpolationProblemBasename: String
- Attributes
- protected
- var interpolationProblemNum: Int
- Attributes
- protected
- lazy val interpolationProver: IncProver
- Attributes
- protected
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def parseAndSimplify(input: Reader): (Map[PartName, Conjunction], Signature)
Read a given problem, split it into the different parts, try to simplify bitvector expressions as far as possible, and convert it to internal presentation.
Read a given problem, split it into the different parts, try to simplify bitvector expressions as far as possible, and convert it to internal presentation. Bitvector simplifications are done based on the type declarations inSigned, inUnsigned, and inArray. The problem will also be restructured such that the type declaration of a constant occurs in the first part in which the constant is used (sorted the partitions lexicographically according to their name).
- Attributes
- protected
- def parseProblem(reader: Reader): (IFormula, Signature)
- Attributes
- protected
- val preludeSignature: Signature
- Attributes
- protected
- def simplifyBitvectorFor(f: IFormula, typeAssumptions: IFormula): IFormula
- Attributes
- protected
- def sortNamesLex[A](transitionParts: Map[PartName, A]): Seq[PartName]
Sort the transition relations lexicographically according to their name; NO_NAME is ignored and removed
Sort the transition relations lexicographically according to their name; NO_NAME is ignored and removed
- Attributes
- protected
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toInputAbsyAndSimplify(c: Conjunction): IFormula
- Attributes
- protected
- def toInternal(f: IFormula, sig: Signature): (Conjunction, TermOrder)
- Attributes
- protected
- def toNamedParts(f: IFormula, sig: Signature): (Map[PartName, Conjunction], Signature)
- Attributes
- protected
- def toString(): String
- Definition Classes
- AnyRef → Any
- lazy val validityCheckProver: IncProver
- Attributes
- protected
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)