Module dev.civl.sarl

Package dev.civl.sarl.IF.expr

Interface BooleanExpression

All Superinterfaces:

SymbolicExpression, SymbolicObject

All Known Subinterfaces:

BooleanSymbolicConstant

public interface BooleanExpression
extends SymbolicExpression

A symbolic expression of boolean type.

Nested Class Summary

Nested classes/interfaces inherited from interface dev.civl.sarl.IF.expr.SymbolicExpression

SymbolicExpression.SymbolicOperator

Nested classes/interfaces inherited from interface dev.civl.sarl.IF.object.SymbolicObject

SymbolicObject.SymbolicObjectKind

Method Summary

Modifier and Type	Method	Description
BooleanExpression[]	getClauses()	Returns a sequence of boolean expressions whose conjunction is equivalent to this.
ValidityResult.ResultType	getUnsatisfiability()	Is this boolean expression unsatisfiable, i.e., equivalent to false,? The result is cached here for convenience, using method invalid reference #setUnsatisfiable(ResultType) .
ValidityResult.ResultType	getValidity()	Is this boolean expression valid, i.e., equivalent to true, i.e., a tautology? The result is cached here for convenience, using method setValidity(ResultType).
void	setUnsatisfiability(ValidityResult.ResultType value)	Store the unsatisfiability result for this boolean expression.
void	setValidity(ValidityResult.ResultType value)	Store the validity result for this boolean expression.

Methods inherited from interface dev.civl.sarl.IF.expr.SymbolicExpression

argument, atomString, getArguments, getFreeVars, isFalse, isNull, isNumeric, isOne, isTrue, isZero, numArguments, operator, printCompressedTree, size, type

Methods inherited from interface dev.civl.sarl.IF.object.SymbolicObject

containsQuantifier, containsSubobject, containsSubobjectIgnoringType, equals, getOrder, hashCode, id, isCanonic, setInCanonic, setOrder, symbolicObjectKind, toString, toStringBuffer, toStringBufferLong

Method Details

getClauses

BooleanExpression[] getClauses()

Returns a sequence of boolean expressions whose conjunction is equivalent to this. The decomposition should be highly non-trivial in general, and this method should be efficient.

Returns:

sequence of symbolic expressions whose conjunction is equivalent to this

getValidity

ValidityResult.ResultType getValidity()

Is this boolean expression valid, i.e., equivalent to true, i.e., a tautology? The result is cached here for convenience, using method setValidity(ResultType). There are four possible values: (1) null: nothing is known and nothing has been tried to figure it out, (2) ValidityResult.ResultType.YES: it is definitely valid, (3) ValidityResult.ResultType.NO: it is definitely not valid, and (4) ValidityResult.ResultType.MAYBE: unknown. The difference between null and ValidityResult.ResultType.MAYBE is that with ValidityResult.ResultType.MAYBE you know we already tried to figure out if it is valid and couldn't, hence, there is no need to try again.

Returns:

the cached validity result

See Also:

• setValidity(ResultType)

setValidity

void setValidity(ValidityResult.ResultType value)

Store the validity result for this boolean expression.

Parameters:

value - the validity result to cache

See Also:

• getValidity()

getUnsatisfiability

ValidityResult.ResultType getUnsatisfiability()

Is this boolean expression unsatisfiable, i.e., equivalent to false,? The result is cached here for convenience, using method

invalid reference

#setUnsatisfiable(ResultType)

. There are four possible values: (1) null: nothing is known and nothing has been tried to figure it out, (2) ValidityResult.ResultType.YES: it is definitely unsatisfiable, (3) ValidityResult.ResultType.NO: it is definitely satisfiable, and (4) ValidityResult.ResultType.MAYBE: unknown. The difference between null and ValidityResult.ResultType.MAYBE is that with ValidityResult.ResultType.MAYBE you know we already tried to figure out if it is unsatisfiable and couldn't, hence, there is no need to try again.

Returns:

setUnsatisfiability

void setUnsatisfiability(ValidityResult.ResultType value)

Store the unsatisfiability result for this boolean expression.

Parameters:

value - the unsatisfiability result to cache

See Also:

• getUnsatisfiability()