Packages

object SMTLineariser

Class for printing IFormulas in the SMT-LIB 2 format

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

Type Members

  1. class IllegalStringException extends Exception

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 apply(term: ITerm): Unit
  5. def apply(formula: IFormula, constantType: (ConstantTerm) => Option[SMTType], functionType: (IFunction) => Option[SMTFunctionType], predType: (Predicate) => Option[SMTFunctionType], prettyBitvectors: Boolean = true): Unit
  6. def apply(formula: IFormula): Unit
  7. def apply(expr: IExpression): Unit
  8. def applyNoPrettyBitvectors(term: ITerm): Unit
  9. def applyNoPrettyBitvectors(formula: IFormula): Unit
  10. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  11. def asString(t: ITerm): String
  12. def asString(formula: IFormula): String
  13. def asString(t: IExpression): String
  14. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  17. def escapeSQString(str: String): String

    Unescape a single-quoted string; the only recognised escape sequence is

  18. def escapeString(str: String): String
  19. val functionTypeFromSort: (IFunction) => Option[SMTFunctionType]
  20. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  21. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  25. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  26. val predTypeFromSort: (Predicate) => Option[SMTFunctionType]
  27. def printArguments(argSorts: Seq[Sort], formalArgs: Seq[ConstantTerm]): Unit
  28. def printDefineFun(f: IFunction, functionType: (Seq[Sort], Sort), formalArgs: Seq[ConstantTerm], body: IExpression): Unit
  29. def printModel(model: IFormula): Unit
  30. def printSMTType(t: SMTType): Unit
  31. def printWithDecls(formulas: Seq[IFormula], constsToDeclare: Seq[ConstantTerm] = List(), predsToDeclare: Seq[Predicate] = List(), funsToDeclare: Seq[IFunction] = List(), extraTheories: Seq[Theory] = List(), benchmarkName: String = "", logic: String = "AUFLIA", status: String = "unknown"): Unit
  32. def printWithDeclsSig(formulas: Seq[IFormula], signature: Signature, extraTheories: Seq[Theory] = List(), benchmarkName: String = "", logic: String = "AUFLIA", status: String = "unknown"): Unit
  33. def quoteIdentifier(str: String): String
  34. def simpleUnescapeIt(it: Iterator[Int]): Seq[Int]

    Unescaping strictly following the SMT-LIB standard.

  35. def smtTypeAsString(t: SMTType): String
  36. def sort2SMTString(sort: Sort): String
  37. def sort2SMTType(sort: Sort): (SMTType, Option[(ITerm) => IFormula])
  38. def sortTheoryDeps(theories: Seq[Theory]): Seq[Theory]

    Topologically sort theories to be declared: dependencies of a theory preceed the theory in the resulting list.

  39. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  40. def toSMTExpr(value: IdealInt): String
  41. def toString(): String
    Definition Classes
    AnyRef → Any
  42. def unescapeIt(it: Iterator[Int]): Seq[Int]
  43. def unescapeSQString(str: String): String

    Unescape a single-quoted string; the only recognised escape sequence is

  44. def unescapeString(str: String): String
  45. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  46. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  47. 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