Object/Class

ap.parser

SMTLineariser

Related Docs: class SMTLineariser | package parser

Permalink

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

Type Members

  1. class IllegalStringException extends Exception

    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 apply(benchmarkName: String, logic: String, status: String, constsToDeclare: Seq[ConstantTerm], predsToDeclare: Seq[Predicate], formulas: Seq[IFormula]): Unit

    Permalink
  5. def apply(formulas: Seq[IFormula], signature: Signature, logic: String, status: String, benchmarkName: String): Unit

    Permalink
  6. def apply(formulas: Seq[IFormula], signature: Signature, benchmarkName: String): Unit

    Permalink
  7. def apply(term: ITerm): Unit

    Permalink
  8. def apply(formula: IFormula, constantType: (ConstantTerm) ⇒ Option[SMTType], functionType: (IFunction) ⇒ Option[SMTFunctionType], predType: (Predicate) ⇒ Option[SMTFunctionType], prettyBitvectors: Boolean = true): Unit

    Permalink
  9. def apply(formula: IFormula): Unit

    Permalink
  10. def apply(expr: IExpression): Unit

    Permalink
  11. def applyNoPrettyBitvectors(term: ITerm): Unit

    Permalink
  12. def applyNoPrettyBitvectors(formula: IFormula): Unit

    Permalink
  13. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  14. def asString(t: ITerm): String

    Permalink
  15. def asString(formula: IFormula): String

    Permalink
  16. def asString(t: IExpression): String

    Permalink
  17. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  18. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  19. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  20. def escapeSQString(str: String): String

    Permalink

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

  21. def escapeString(str: String): String

    Permalink
  22. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  23. val functionTypeFromSort: (IFunction) ⇒ Option[SMTFunctionType]

    Permalink
  24. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  25. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  26. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  27. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  28. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  29. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  30. val predTypeFromSort: (Predicate) ⇒ Option[SMTFunctionType]

    Permalink
  31. def printADTDeclaration(adt: ADT): Unit

    Permalink
  32. def printADTDeclarations(adts: Seq[ADT]): Unit

    Permalink
  33. def printArguments(argSorts: Seq[Sort], formalArgs: Seq[ConstantTerm]): Unit

    Permalink
  34. def printDefineFun(f: IFunction, functionType: (Seq[Sort], Sort), formalArgs: Seq[ConstantTerm], body: IExpression): Unit

    Permalink
  35. def printHeapDeclaration(heap: Heap): Unit

    Permalink
  36. def printHeapDeclarations(heaps: Seq[Heap]): Unit

    Permalink
  37. def printModel(model: IFormula): Unit

    Permalink
  38. def printSMTType(t: SMTType): Unit

    Permalink
  39. def quoteIdentifier(str: String): String

    Permalink
  40. def simpleUnescapeIt(it: Iterator[Int]): Seq[Int]

    Permalink

    Unescaping strictly following the SMT-LIB standard.

  41. def smtTypeAsString(t: SMTType): String

    Permalink
  42. def sort2SMTString(sort: Sort): String

    Permalink
  43. def sort2SMTType(sort: Sort): (SMTType, Option[(ITerm) ⇒ IFormula])

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

    Permalink
    Definition Classes
    AnyRef
  45. def toSMTExpr(value: IdealInt): String

    Permalink
  46. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  47. def unescapeIt(it: Iterator[Int]): Seq[Int]

    Permalink
  48. def unescapeSQString(str: String): String

    Permalink

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

  49. def unescapeString(str: String): String

    Permalink
  50. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  51. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  52. final def wait(arg0: Long): Unit

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

Inherited from AnyRef

Inherited from Any

Ungrouped