Packages

class SMTParser2InputAbsy extends Parser2InputAbsy[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType, (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])]

Linear Supertypes
Parser2InputAbsy[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType, (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])], AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SMTParser2InputAbsy
  2. Parser2InputAbsy
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new SMTParser2InputAbsy(_env: Environment[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType], settings: ParserSettings, _prover: api.SimpleAPI)

Type Members

  1. abstract class ASTConnective extends AnyRef
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  2. type GrammarExpression = Term
    Definition Classes
    SMTParser2InputAbsy → Parser2InputAbsy

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 addAxiom(f: IFormula): Unit
    Attributes
    protected
    Definition Classes
    SMTParser2InputAbsy → Parser2InputAbsy
  5. def addTheory(t: Theory): Unit
    Attributes
    protected
    Definition Classes
    SMTParser2InputAbsy → Parser2InputAbsy
  6. def apply(input: Reader): (IFormula, List[IInterpolantSpec], Signature)

    Parse a problem from a character stream.

    Parse a problem from a character stream. The result is the formula contained in the input, a list of interpolation specifications present in the input, and the Signature declared in the input (constants, and the TermOrder that was used for the formula).

    Definition Classes
    SMTParser2InputAbsy → Parser2InputAbsy
  7. def asFormula(expr: (IExpression, SMTType)): IFormula
    Attributes
    protected
  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. def checkArgNum(op: String, expected: Int, args: Seq[Term]): Unit
    Attributes
    protected
  10. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  11. def collectSubExpressions(f: GrammarExpression, cont: (GrammarExpression) => Boolean, Connective: ASTConnective): Seq[GrammarExpression]
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  12. def constantTypeMap: Map[ConstantTerm, SMTType]
  13. def ensureEnvironmentCopy: Unit

    Make sure that the current settings frame contains a local copy of the Environment.

    Make sure that the current settings frame contains a local copy of the Environment. To be called before changing anything in the Environment.

    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  14. def env: Environment[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType]
    Definition Classes
    Parser2InputAbsy
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  17. def extractAssertions(input: Reader): Seq[IFormula]
  18. def extractHeap(args: Seq[Term]): Option[(Option[ITerm], Heap)]
    Attributes
    protected
  19. def functionTypeMap: Map[IFunction, SMTFunctionType]
  20. def genSignature(completeFor: IExpression): Signature
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  21. def getAxioms: IFormula
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  22. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  23. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  24. def incrementalityMessage(thing: String, warnOnly: Boolean): String
    Attributes
    protected
  25. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  26. lazy val mulTheory: MulTheory
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  27. def mult(t1: ITerm, t2: ITerm): ITerm
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  28. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  29. def neverInline(expr: IExpression): Boolean

    Check whether the given expression should never be inlined, e.g., because it is too big.

    Check whether the given expression should never be inlined, e.g., because it is too big. This method is meant to be redefinable in subclasses

    Attributes
    protected
  30. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  31. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  32. def objectType(heapTheory: Heap): SMTType
    Attributes
    protected
  33. def parseExpression(str: String): IExpression
  34. def parseIgnoreCommand(input: Reader): IExpression

    Parse an SMT-LIB script of the form (ignore expression).

  35. def pop: Unit

    Pop a frame from the settings stack.

    Pop a frame from the settings stack.

    Attributes
    protected
  36. def popState: (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])

    Pop a frame from the settings stack.

    Pop a frame from the settings stack.

    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  37. def predicateTypeMap: Map[Predicate, SMTFunctionType]
  38. def processIncrementally(input: Reader, timeout: Int, _timeoutPer: Int, userDefStoppingCond: => Boolean): Unit
  39. def push: Unit

    Add a new frame to the settings stack; this in particular affects the Environment.

    Add a new frame to the settings stack; this in particular affects the Environment.

    Attributes
    protected
  40. def pushState(state: (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])): Unit

    Add a new frame to the settings stack; this in particular affects the Environment.

    Add a new frame to the settings stack; this in particular affects the Environment.

    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  41. def registerRecFunctions(funs: Seq[(IFunction, (IExpression, SMTType))]): Unit
    Attributes
    protected
  42. def reset: Unit

    Erase all stored information.

    Erase all stored information.

    Attributes
    protected
    Definition Classes
    SMTParser2InputAbsy → Parser2InputAbsy
  43. def symApp(sym: SymbolRef, args: Seq[Term], polarity: Int): (IExpression, SMTType)
    Attributes
    protected
  44. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  45. def toString(): String
    Definition Classes
    AnyRef → Any
  46. def translateExtraTheorySort(s: Sort): Option[SMTType]
    Attributes
    protected
  47. def translateHeapFun(funF: (Heap) => IFunction, args: Seq[Term], argTypesF: (Heap) => Seq[SMTType], resTypeF: (Heap) => SMTType): Option[(IExpression, SMTType)]
    Attributes
    protected
  48. def translateSort(s: Sort): SMTType
    Attributes
    protected
  49. def translateSpecConstant(c: SpecConstant): (ITerm, SMTType)
    Attributes
    protected
  50. def translateTerm(t: Term, polarity: Int): (IExpression, SMTType)
    Attributes
    protected
  51. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  52. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  53. 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 Parser2InputAbsy[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType, (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])]

Inherited from AnyRef

Inherited from Any

Ungrouped