Packages

class Evaluator extends AnyRef

A class representing a first-order model of some formula. The class will internally start from the partial model computed by a SimpleAPI, and extend this model on demand. The class will make use of the SimpleAPI instance to compute missing parts of the model, and can therefore mutate the state of the SimpleAPI. To reset the SimpleAPI to the state before creating the Evaluator, use the method resetModelExtension; a safer way is to apply the method SimpleAPI.withCompleteModel to spawn the Evaluator.

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

Instance Constructors

  1. new Evaluator(api: SimpleAPI)

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

    Evaluate a formula to a Boolean.

    Evaluate a formula to a Boolean. This method has the same effect as evalToBool.

  5. def apply(t: ITerm): ITerm

    Evaluate a term to a constructor term.

    Evaluate a term to a constructor term. This method has the same effect as evalToTerm.

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  10. def evalToBool(f: IFormula): Boolean

    Evaluate a formula to a Boolean.

  11. def evalToInt(t: ITerm): IdealInt

    Evaluate a term to an integer.

    Evaluate a term to an integer. This method should be used for integer or bit-vector terms, but can in principle be applied to any term.

  12. def evalToTerm(t: ITerm): ITerm

    Evaluate a term to a constructor term.

  13. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  14. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  18. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  19. def shutDown: Unit

    Reset the evaluator and the connected SimpleAPI instance.

  20. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  21. def toString(): String
    Definition Classes
    AnyRef → Any
  22. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  23. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  24. 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