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 escapeString(str: String): String

    Permalink
  21. def finalize(): Unit

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    Permalink
  37. def smtTypeAsString(t: SMTType): String

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

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

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

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

    Permalink
  42. def toString(): String

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

    Permalink
  44. def unescapeString(str: String): String

    Permalink
  45. final def wait(): Unit

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped