public final class Context
extends java.lang.Object
Constructor and Description 

Context()
construct a new context empty of assumptions

Modifier and Type  Method and Description 

void 
abort()
return to the parent context discarding all the formulas that were added
to the subcontext since the last call of open().

void 
assume(Expression formula)
add an assumption to the current (sub)context

void 
close()
close formula on top of formula stack with respect to current scope.

void 
commit()
return to the parent context and add to it all the formulas that were
added to the subcontext since the last call of open().

Expression 
getFormula()
return the formula currently on the top of the stack

void 
implies(Expression formula)
conjoin formula to the current formula on the top of the stack

void 
open()
open a new subcontext
subcontexts may be arbitrarily nested; every subcontext must be
ultimately either aborted or commited.

public Expression getFormula()
public void assume(Expression formula)
formula
 the assumption to be addedpublic void implies(Expression formula)
formula
 formula to be conjoined to top of stackpublic void open()
public void abort()
public void commit()
public void close()