Package mepk.kernel

Class Statement

java.lang.Object

mepk.kernel.Statement

public final class Statement
extends Object

This class represents an statement. Statements are values: they cannot be modified after they have been created. They are equal if (and only if) they have the same structure. It is only possible to create an instance using the static methods in this class.

Method Summary

Modifier and Type	Method	Description
boolean	equals(Object obj)
Set<Statement>	expand(Abbreviation abbreviation)	Expand this statement by applying the given abbreviation.
Expression	getConclusion()	Returns the conclusion of this statement.
DVRSet	getDVRs()	Returns the distinct-variable restrictions (DVRs) of this statement.
Collection<? extends Expression>	getHypotheses()	Returns the hypotheses of this statement.
int	hashCode()
static Statement	Stat(List<Expression> hypotheses, Expression conclusion)	Create a new instance with an empty set of DVRs.
static Statement	Stat(DVRSet dvrs, List<Expression> hypotheses, Expression conclusion)	Create a new instance.
Statement	substitute(String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create a new statement, by replacing one variable in this statement by an expression, and optionally adding type expressions (to make resulting statement type-correct).
String	toString()
Statement	weaken(DVRSet addedDVRs, Expression... addedHypotheses)	Create a new statement, by adding hypotheses and DVRs to this statement.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

Stat

public static Statement Stat(List<Expression> hypotheses,
 Expression conclusion)

Create a new instance with an empty set of DVRs.

Parameters:

hypotheses - the hypotheses

conclusion - the conclusion

Returns:

the created statement

Stat

public static Statement Stat(DVRSet dvrs,
 List<Expression> hypotheses,
 Expression conclusion)

Create a new instance.

Parameters:

dvrs - the DVRs

hypotheses - the hypotheses

conclusion - the conclusion

Returns:

the created statement

getDVRs

public DVRSet getDVRs()

Returns the distinct-variable restrictions (DVRs) of this statement.

Returns:

the DVRs

getHypotheses

public Collection<? extends Expression> getHypotheses()

Returns the hypotheses of this statement.

Returns:

the hypotheses

getConclusion

public Expression getConclusion()

Returns the conclusion of this statement.

Returns:

the conclusion

hashCode

public int hashCode()

Overrides:

hashCode in class Object

equals

public boolean equals(Object obj)

Overrides:

equals in class Object

toString

public String toString()

Overrides:

toString in class Object

substitute

public Statement substitute(String varName,
 Expression replacement,
 Map<String,String> typesOfNewVars)

Create a new statement, by replacing one variable in this statement by an expression, and optionally adding type expressions (to make resulting statement type-correct).

Parameters:

varName - the variable name

replacement - the replacement expression

typesOfNewVars - the additional type expressions

Returns:

the new statement

weaken

public Statement weaken(DVRSet addedDVRs,
 Expression... addedHypotheses)

Create a new statement, by adding hypotheses and DVRs to this statement.

Parameters:

addedDVRs - the added DVRs

addedHypotheses - the added hypotheses

Returns:

the new statement

expand

public Set<Statement> expand(Abbreviation abbreviation)

Expand this statement by applying the given abbreviation. Note that if conditions are used, then this will usually result in multiple statements, e.g., abbreviation "(group-elem x) abbreviates (Real x) for which (> x (0))" would expand (group-elem x) AND (group-elem y) ==> (group-elem (op x y)) to

• (Real x) AND (> x (0)) AND (Real y) AND (> y (0)) ==> (Real (op x y))
• (Real x) AND (> x (0)) AND (Real y) AND (> y (0)) ==> (> (op x y) (0))

Parameters:

abbreviation - the abbreviation to expand

Returns:

the set of statements resulting from the expansion