Evaluator

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

Instance Constructors

new Evaluator(api: SimpleAPI)

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
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.
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.
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

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

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def evalToBool(f: IFormula): Boolean

Evaluate a formula to a Boolean.
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.
def evalToTerm(t: ITerm): ITerm

Evaluate a term to a constructor term.
final def getClass(): Class[_]

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

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
final def isInstanceOf[T0]: Boolean

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

Definition Classes
AnyRef
final def notify(): Unit

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

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
def shutDown: Unit

Reset the evaluator and the connected SimpleAPI instance.
Reset the evaluator and the connected SimpleAPI instance.
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
AnyRef → Any
final def wait(arg0: Long, arg1: Int): Unit

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

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: object Evaluator | package api

class Evaluator extends AnyRef

Instance Constructors

new Evaluator(api: SimpleAPI)

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def apply(f: IFormula): Boolean

def apply(t: ITerm): ITerm

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def evalToBool(f: IFormula): Boolean

def evalToInt(t: ITerm): IdealInt

def evalToTerm(t: ITerm): ITerm

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def shutDown: Unit

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

Deprecated Value Members

def finalize(): Unit

Inherited from AnyRef

Inherited from Any

Ungrouped