public static void simulateAndOptimizeQuery(Proposition proposition) {
    { Vector arguments = proposition.arguments;
      Keyword kind = proposition.kind;

      if (((Boolean)(Logic.$REVERSEPOLARITYp$.get())).booleanValue()) {
        if (kind == Logic.KWD_AND) {
          kind = Logic.KWD_OR;
        }
        else if (kind == Logic.KWD_OR) {
          kind = Logic.KWD_AND;
        }
        else if (kind == Logic.KWD_IMPLIES) {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("REVERSE POLARITY NOT YET IMPLEMENTED FOR :IMPLIES WITHIN QUERY OPTIMIZER");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
        else {
        }
      }
      if ((kind == Logic.KWD_ISA) ||
          ((kind == Logic.KWD_PREDICATE) ||
           ((kind == Logic.KWD_FUNCTION) ||
            (kind == Logic.KWD_EQUIVALENT)))) {
        Proposition.simulateGoalEvaluation(proposition);
        { Stella_Object arg = null;
          Vector vector000 = arguments;
          int index000 = 0;
          int length000 = vector000.length();

          for (;index000 < length000; index000 = index000 + 1) {
            arg = (vector000.theArray)[index000];
            Logic.simulateAndOptimizeArgument(arg);
          }
        }
      }
      else if (kind == Logic.KWD_AND) {
        { int choicepointunbindingoffset = Logic.simulateCreateChoicePoint();

          Logic.initializeOptimizerMemory(-1);
          Proposition.optimizeOrderingOfConjuncts(proposition);
          PatternRecord.unbindVariablesBeginningAt(((QueryIterator)(Logic.$QUERYITERATOR$.get())).currentPatternRecord, choicepointunbindingoffset);
        }
        { Stella_Object arg = null;
          Vector vector001 = proposition.arguments;
          int index001 = 0;
          int length001 = vector001.length();

          for (;index001 < length001; index001 = index001 + 1) {
            arg = (vector001.theArray)[index001];
            Proposition.simulateAndOptimizeQuery(((Proposition)(arg)));
          }
        }
      }
      else if (kind == Logic.KWD_OR) {
        { Stella_Object arg = null;
          Vector vector002 = arguments;
          int index002 = 0;
          int length002 = vector002.length();

          for (;index002 < length002; index002 = index002 + 1) {
            arg = (vector002.theArray)[index002];
            { int choicepointunbindingoffset = Logic.simulateCreateChoicePoint();

              Proposition.simulateAndOptimizeQuery(((Proposition)(arg)));
              PatternRecord.unbindVariablesBeginningAt(((QueryIterator)(Logic.$QUERYITERATOR$.get())).currentPatternRecord, choicepointunbindingoffset);
            }
          }
        }
      }
      else if (kind == Logic.KWD_NOT) {
        { boolean oldreversepolarityP = ((Boolean)(Logic.$REVERSEPOLARITYp$.get())).booleanValue();

          { Object old$ReversepolarityP$000 = Logic.$REVERSEPOLARITYp$.get();

            try {
              Native.setBooleanSpecial(Logic.$REVERSEPOLARITYp$, !oldreversepolarityP);
              if (((Boolean)(Logic.$REVERSEPOLARITYp$.get())).booleanValue()) {
                Proposition.warnOfUnboundVariableArgument(proposition);
              }
              Proposition.simulateAndOptimizeQuery(((Proposition)((arguments.theArray)[0])));

            } finally {
              Logic.$REVERSEPOLARITYp$.set(old$ReversepolarityP$000);
            }
          }
        }
      }
      else if (kind == Logic.KWD_IMPLIES) {
        Proposition.warnOfUnboundVariableArgument(proposition);
        { Stella_Object arg = null;
          Vector vector003 = arguments;
          int index003 = 0;
          int length003 = vector003.length();

          for (;index003 < length003; index003 = index003 + 1) {
            arg = (vector003.theArray)[index003];
            Logic.simulateAndOptimizeArgument(arg);
          }
        }
      }
      else if (kind == Logic.KWD_EXISTS) {
        Proposition.simulateAndOptimizeQuery(((Proposition)((arguments.theArray)[0])));
      }
      else if (kind == Logic.KWD_FORALL) {
        { int choicepointunbindingoffset = Logic.simulateCreateChoicePoint();

          { Stella_Object arg = null;
            Vector vector004 = arguments;
            int index004 = 0;
            int length004 = vector004.length();

            for (;index004 < length004; index004 = index004 + 1) {
              arg = (vector004.theArray)[index004];
              Logic.simulateAndOptimizeArgument(arg);
            }
          }
          PatternRecord.unbindVariablesBeginningAt(((QueryIterator)(Logic.$QUERYITERATOR$.get())).currentPatternRecord, choicepointunbindingoffset);
        }
      }
      else {
      }
    }
  }