Class/Object

ap.parser

SMTParser2InputAbsy

Related Docs: object SMTParser2InputAbsy | package parser

Permalink

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

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

Instance Constructors

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

    Permalink

Type Members

  1. abstract class ASTConnective extends AnyRef

    Permalink
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  2. type GrammarExpression = Term

    Permalink
    Definition Classes
    SMTParser2InputAbsyParser2InputAbsy

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 addAxiom(f: IFormula): Unit

    Permalink
    Attributes
    protected
    Definition Classes
    SMTParser2InputAbsyParser2InputAbsy
  5. def addTheory(t: Theory): Unit

    Permalink
    Attributes
    protected
    Definition Classes
    SMTParser2InputAbsyParser2InputAbsy
  6. def apply(input: Reader): (IFormula, List[IInterpolantSpec], Signature)

    Permalink

    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
    SMTParser2InputAbsyParser2InputAbsy
  7. def asFormula(expr: (IExpression, SMTType)): IFormula

    Permalink
    Attributes
    protected
  8. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  9. def asTerm(expr: (IExpression, SMTType)): ITerm

    Permalink
    Attributes
    protected
  10. def checkArgNum(op: String, expected: Int, args: Seq[Term]): Unit

    Permalink
    Attributes
    protected
  11. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )
  12. def collectSubExpressions(f: GrammarExpression, cont: (GrammarExpression) ⇒ Boolean, Connective: ASTConnective): Seq[GrammarExpression]

    Permalink
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  13. def constantTypeMap: Map[ConstantTerm, SMTType]

    Permalink
  14. def ensureEnvironmentCopy: Unit

    Permalink

    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
  15. def env: Environment[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType]

    Permalink
    Definition Classes
    Parser2InputAbsy
  16. final def eq(arg0: AnyRef): Boolean

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

    Permalink
    Definition Classes
    AnyRef → Any
  18. def extractAssertions(input: Reader): Seq[IFormula]

    Permalink
  19. def extractHeap(args: Seq[Term]): Option[(Option[ITerm], Heap)]

    Permalink
    Attributes
    protected
  20. def functionTypeMap: Map[IFunction, SMTFunctionType]

    Permalink
  21. def genSignature(completeFor: IExpression): Signature

    Permalink
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  22. def getAxioms: IFormula

    Permalink
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  23. final def getClass(): Class[_]

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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  25. def incrementalityMessage(thing: String, warnOnly: Boolean): String

    Permalink
    Attributes
    protected
  26. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  27. lazy val mulTheory: MulTheory

    Permalink
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  28. def mult(t1: ITerm, t2: ITerm): ITerm

    Permalink
    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  29. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  30. def neverInline(expr: IExpression): Boolean

    Permalink

    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
  31. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  32. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  33. def objectType(heapTheory: Heap): SMTType

    Permalink
    Attributes
    protected
  34. def parseExpression(str: String): IExpression

    Permalink
  35. def parseIgnoreCommand(input: Reader): IExpression

    Permalink

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

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

  36. def pop: Unit

    Permalink

    Pop a frame from the settings stack.

    Pop a frame from the settings stack.

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

    Permalink

    Pop a frame from the settings stack.

    Pop a frame from the settings stack.

    Attributes
    protected
    Definition Classes
    Parser2InputAbsy
  38. def predicateTypeMap: Map[Predicate, SMTFunctionType]

    Permalink
  39. def processIncrementally(input: Reader, timeout: Int, _timeoutPer: Int, userDefStoppingCond: ⇒ Boolean): Unit

    Permalink
  40. def push: Unit

    Permalink

    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
  41. def pushState(state: (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])): Unit

    Permalink

    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
  42. def registerRecFunctions(funs: Seq[(IFunction, (IExpression, SMTType))]): Unit

    Permalink
    Attributes
    protected
  43. def reset: Unit

    Permalink

    Erase all stored information.

    Erase all stored information.

    Attributes
    protected
    Definition Classes
    SMTParser2InputAbsyParser2InputAbsy
  44. def symApp(sym: SymbolRef, args: Seq[Term], polarity: Int): (IExpression, SMTType)

    Permalink
    Attributes
    protected
  45. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  46. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  47. def translateHeapFun(funF: (Heap) ⇒ IFunction, args: Seq[Term], argTypesF: (Heap) ⇒ Seq[SMTType], resTypeF: (Heap) ⇒ SMTType): Option[(IExpression, SMTType)]

    Permalink
    Attributes
    protected
  48. def translateSort(s: Sort): SMTType

    Permalink
    Attributes
    protected
  49. def translateSpecConstant(c: SpecConstant): (ITerm, SMTType)

    Permalink
    Attributes
    protected
  50. def translateTerm(t: Term, polarity: Int): (IExpression, SMTType)

    Permalink
    Attributes
    protected
  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( ... )
  53. final def wait(): Unit

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

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from AnyRef

Inherited from Any

Ungrouped