private Formula constructOr(final LinkedHashSet<? extends Formula> operands) {
    Or tempOr = null;
    Map<LinkedHashSet<? extends Formula>, Or> opOrMap = this.orsN;
    if (operands.size() > 1) {
      switch (operands.size()) {
        case 2:
          opOrMap = this.ors2;
          break;
        case 3:
          opOrMap = this.ors3;
          break;
        case 4:
          opOrMap = this.ors4;
          break;
        default:
          break;
      }
      tempOr = opOrMap.get(operands);
    }
    if (tempOr != null)
      return tempOr;
    final LinkedHashSet<? extends Formula> condensedOperands = operands.size() < 2
            ? operands
            : this.condenseOperandsOr(operands);
    if (condensedOperands == null)
      return this.verum();
    if (condensedOperands.isEmpty())
      return this.falsum();
    if (condensedOperands.size() == 1)
      return condensedOperands.iterator().next();
    final Or or;
    Map<LinkedHashSet<? extends Formula>, Or> condOrMap = this.orsN;
    switch (condensedOperands.size()) {
      case 2:
        condOrMap = this.ors2;
        break;
      case 3:
        condOrMap = this.ors3;
        break;
      case 4:
        condOrMap = this.ors4;
        break;
      default:
        break;
    }
    or = condOrMap.get(condensedOperands);
    if (or == null) {
      tempOr = new Or(condensedOperands, this, this.cnfCheck);
      opOrMap.put(operands, tempOr);
      condOrMap.put(condensedOperands, tempOr);
      return tempOr;
    }
    opOrMap.put(operands, or);
    return or;
  }
private Formula constructOr ( final LinkedHashSet < ? extends Formula > operands ) { Or tempOr = null ; Map < LinkedHashSet < ? extends Formula > , Or > opOrMap = this . orsN ; if ( operands . size ( ) > 1 ) { switch ( operands . size ( ) ) { case 2 : opOrMap = this . ors2 ; break ; case 3 : opOrMap = this . ors3 ; break ; case 4 : opOrMap = this . ors4 ; break ; default : break ; } tempOr = opOrMap . get ( operands ) ; } if ( tempOr != null ) return tempOr ; final LinkedHashSet < ? extends Formula > condensedOperands = operands . size ( ) < 2 ? operands : this . condenseOperandsOr ( operands ) ; if ( condensedOperands == null ) return this . verum ( ) ; if ( condensedOperands . isEmpty ( ) ) return this . falsum ( ) ; if ( condensedOperands . size ( ) == 1 ) return condensedOperands . iterator ( ) . next ( ) ; final Or or ; Map < LinkedHashSet < ? extends Formula > , Or > condOrMap = this . orsN ; switch ( condensedOperands . size ( ) ) { case 2 : condOrMap = this . ors2 ; break ; case 3 : condOrMap = this . ors3 ; break ; case 4 : condOrMap = this . ors4 ; break ; default : break ; } or = condOrMap . get ( condensedOperands ) ; if ( or == null ) { tempOr = new Or ( condensedOperands , this , this . cnfCheck ) ; opOrMap . put ( operands , tempOr ) ; condOrMap . put ( condensedOperands , tempOr ) ; return tempOr ; } opOrMap . put ( operands , or ) ; return or ; }
Creates a new disjunction.
@param operands the formulas
@return a new disjunction