Interface BooleanExpressionFactory


public interface BooleanExpressionFactory
  • Method Details

    • setNumericExpressionFactory

      void setNumericExpressionFactory(NumericExpressionFactory numericExpressionFactory)
      The boolean factory needs a numeric expression factory in order to negate expressions like "ainvalid input: '<'b" or "ainvalid input: '<'=b".
      Parameters:
      numericFactory -
    • booleanExpression

      Returns an expression, given the operator and an array of arguments
      Parameters:
      operator - A SymbolicOperator
      args - 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

      BooleanExpression symbolic(BooleanObject object)
      The symbolic expression wrapping the given boolean object (true or false).
    • symbolic

      BooleanExpression symbolic(boolean value)
      Short cut for symbolic(booleanObject(value)).
      Parameters:
      value -
      Returns:
      symbolic expression wrapping boolean value
    • booleanSymbolicConstant

      BooleanSymbolicConstant booleanSymbolicConstant(StringObject name)
    • 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 type
      arg1 - 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 type
      arg1 - 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

      BooleanExpression forall(SymbolicConstant boundVariable, BooleanExpression predicate)
      Returns the universally quantified expression forall(x).e.
      Parameters:
      boundVariable - the bound variable x
      predicate - the expression e (of boolean type)
      Returns:
      the expression forall(x).e
    • exists

      BooleanExpression exists(SymbolicConstant boundVariable, BooleanExpression predicate)
      Returns the existentially quantified expression exists(x).e.
      Parameters:
      boundVariable - the bound variable x
      predicate - the expression e (of boolean type)
      Returns:
      the expression exists(x).e
    • getBooleanComparator

      Comparator<BooleanExpression> getBooleanComparator()
      Returns a Comparator on BooleanExpressions produced by this factory.
      Returns:
      the Comparator for the boolean expressions produced by this factory
    • init

      void init()
      Initializes fields; should be called after comparators have been set and linked.
    • containsArgument

      boolean containsArgument(BooleanExpression expression, SymbolicObject arg)
      Is one of the arguments of the given expression equal to arg?
      Parameters:
      expression - a non-null boolean expression
      arg - a symbolic object
      Returns:
      true if and only if one of the arguments of the expression equals arg
    • getArgumentsAsArray

      BooleanExpression[] getArgumentsAsArray(BooleanExpression expression)
      Given a BooleanExpression with operator SymbolicExpression.SymbolicOperator.AND, SymbolicExpression.SymbolicOperator.OR, or SymbolicExpression.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 invoking SymbolicExpression.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

      BooleanExpression factorOrs(BooleanExpression[] orExpressions)
      Given an array of or-expressions (expressions with operation SymbolicExpression.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 operator SymbolicExpression.SymbolicOperator.OR
      Returns:
      the expression that results by taking the "or" over all clauses which occur in every one of the given or-expressions