escjava.prover
Class TriggerlessQuantWarning

java.lang.Object
  escjava.prover.SimplifyOutput
      escjava.prover.SimplifyResult
          escjava.prover.TriggerlessQuantWarning

public class TriggerlessQuantWarning

extends SimplifyResult

An object of this class represent a "result" produced by Simplify.

See Also:

Simplify, CECEnum, SExp

Field Summary

SExp	e0
SExp	e1
(package private) int	n

Fields inherited from class escjava.prover.SimplifyResult

context, labels

Fields inherited from class escjava.prover.SimplifyOutput

COMMENT, COUNTEREXAMPLE, END, EXCEEDED_PROVER_KILL_ITER, EXCEEDED_PROVER_KILL_TIME, EXCEEDED_PROVER_SUBGOAL_KILL_ITER, EXCEEDED_PROVER_SUBGOAL_KILL_TIME, INVALID, kind, REACHED_CC_LIMIT, UNKNOWN, VALID, WARNING_TRIGGERLESS_QUANT

Constructor Summary

(package private)

TriggerlessQuantWarning(SList labels, SList context, SExp e0, int n, SExp e1)

Method Summary

int	getLocation() Attempts to glean a location from the name of the dummy variable appearing in e1.
java.lang.String	toString()

Methods inherited from class escjava.prover.SimplifyResult

getContext, getLabels

Methods inherited from class escjava.prover.SimplifyOutput

getKind

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

e0

public SExp e0

n

int n

e1

public SExp e1

Constructor Detail

TriggerlessQuantWarning

TriggerlessQuantWarning(SList labels,
                        SList context,
                        SExp e0,
                        int n,
                        SExp e1)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class SimplifyResult

getLocation

public int getLocation()

Attempts to glean a location from the name of the dummy variable appearing in e1. If none can be retrieved, the null location is returned.