public interface BooleanExpressionFactory
-
Method Summary
Modifier and TypeMethodDescriptionand(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the conjunction of the two given arguments.booleanExpression(SymbolicExpression.SymbolicOperator operator, SymbolicObject... args) Returns an expression, given the operator and an array of argumentsbooleancontainsArgument(BooleanExpression expression, SymbolicObject arg) Is one of the arguments of the given expression equal toarg?exists(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the existentially quantified expression exists(x).e.factorOrs(BooleanExpression[] orExpressions) Given an array of or-expressions (expressions with operationSymbolicExpression.SymbolicOperator.OR), this method computes the "greatest common divisor" of those expressions and replaces each element of the array with the expressions that results from "dividing by" that gcd.Returns a false BooleanExpressionforall(SymbolicConstant boundVariable, BooleanExpression predicate) Returns the universally quantified expression forall(x).e.getArgumentsAsArray(BooleanExpression expression) Given aBooleanExpressionwith operatorSymbolicExpression.SymbolicOperator.AND,SymbolicExpression.SymbolicOperator.OR, orSymbolicExpression.SymbolicOperator.NOT, this method returns the arguments of that operator as an array.Returns aComparatoronBooleanExpressions produced by this factory.voidinit()Initializes fields; should be called after comparators have been set and linked.not(BooleanExpression arg) Returns a symbolic expression representing the logical negation of the given expression arg.or(BooleanExpression arg0, BooleanExpression arg1) Returns a symbolic expression representing the disjunction of the two given arguments.or(Iterable<? extends BooleanExpression> args) Returns a symbolic expression which represents the disjunction of the expressions in the given array args.voidsetNumericExpressionFactory(NumericExpressionFactory numericExpressionFactory) The boolean factory needs a numeric expression factory in order to negate expressions like "ainvalid input: '<'b" or "ainvalid input: '<'=b".symbolic(boolean value) Short cut for symbolic(booleanObject(value)).symbolic(BooleanObject object) The symbolic expression wrapping the given boolean object (true or false).trueExpr()Returns a true BooleanExpression
-
Method Details
-
setNumericExpressionFactory
The boolean factory needs a numeric expression factory in order to negate expressions like "ainvalid input: '<'b" or "ainvalid input: '<'=b".- Parameters:
numericFactory-
-
booleanExpression
BooleanExpression booleanExpression(SymbolicExpression.SymbolicOperator operator, SymbolicObject... args) Returns an expression, given the operator and an array of arguments- Parameters:
operator- A SymbolicOperatorargs- Array of arguments- Returns:
- Returns a BooleanExpression
-
trueExpr
BooleanExpression trueExpr()Returns a true BooleanExpression- Returns:
- BooleanExpression
-
falseExpr
BooleanExpression falseExpr()Returns a false BooleanExpression- Returns:
- BooleanExpression
-
symbolic
The symbolic expression wrapping the given boolean object (true or false). -
symbolic
Short cut for symbolic(booleanObject(value)).- Parameters:
value-- Returns:
- symbolic expression wrapping boolean value
-
booleanSymbolicConstant
-
and
Returns a symbolic expression representing the conjunction of the two given arguments. Each argument must be non-null and have boolean type.- Parameters:
arg0- a symbolic expression of boolean typearg1- a symbolic expression of boolean type- Returns:
- conjunction of arg0 and arg1
-
or
Returns a symbolic expression representing the disjunction of the two given arguments. Each argument must be non-null and have boolean type.- Parameters:
arg0- a symbolic expression of boolean typearg1- a symbolic expression of boolean type- Returns:
- disjunction of arg0 and arg1
-
or
Returns a symbolic expression which represents the disjunction of the expressions in the given array args. Each expression in args must have boolean type. args must be non-null, and may have any length, including 0. If the length of args is 0, the resulting expression is equivalent to "false".- Parameters:
args- a sequence of expressions of boolean type- Returns:
- the disjunction of the expressions in args
-
not
Returns a symbolic expression representing the logical negation of the given expression arg. arg must be non-null and have boolean type.- Parameters:
arg- a symbolic expression of boolean type- Returns:
- negation of arg
-
forall
Returns the universally quantified expression forall(x).e.- Parameters:
boundVariable- the bound variable xpredicate- the expression e (of boolean type)- Returns:
- the expression forall(x).e
-
exists
Returns the existentially quantified expression exists(x).e.- Parameters:
boundVariable- the bound variable xpredicate- the expression e (of boolean type)- Returns:
- the expression exists(x).e
-
getBooleanComparator
Comparator<BooleanExpression> getBooleanComparator()Returns aComparatoronBooleanExpressions produced by this factory.- Returns:
- the
Comparatorfor the boolean expressions produced by this factory
-
init
void init()Initializes fields; should be called after comparators have been set and linked. -
containsArgument
Is one of the arguments of the given expression equal toarg?- Parameters:
expression- a non-nullboolean expressionarg- a symbolic object- Returns:
trueif and only if one of the arguments of the expression equalsarg
-
getArgumentsAsArray
Given aBooleanExpressionwith operatorSymbolicExpression.SymbolicOperator.AND,SymbolicExpression.SymbolicOperator.OR, orSymbolicExpression.SymbolicOperator.NOT, this method returns the arguments of that operator as an array. The arguments occur in order, the same order as would be returned by invokingSymbolicExpression.argument(int). The array returned should only be read, not modified. Any attempts to modify it will result in undefined behavior.- Parameters:
expression- a boolean expression with operator AND, OR, or NOT.- Returns:
- the arguments of that expression
-
factorOrs
Given an array of or-expressions (expressions with operationSymbolicExpression.SymbolicOperator.OR), this method computes the "greatest common divisor" of those expressions and replaces each element of the array with the expressions that results from "dividing by" that gcd. NOTE this method modifies the given array.- Parameters:
orExpressions- an array of symbolic expressions with operatorSymbolicExpression.SymbolicOperator.OR- Returns:
- the expression that results by taking the "or" over all clauses which occur in every one of the given or-expressions
-