@@ -0,0 +1,1687 @@
+/*%0A * Copyright 2013 Charles University in Prague%0A * Copyright 2013 Vojtech Horky%0A * %0A * Licensed under the Apache License, Version 2.0 (the %22License%22);%0A * you may not use this file except in compliance with the License.%0A * You may obtain a copy of the License at%0A *%0A *     http://www.apache.org/licenses/LICENSE-2.0%0A *%0A * Unless required by applicable law or agreed to in writing, software%0A * distributed under the License is distributed on an %22AS IS%22 BASIS,%0A * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.%0A * See the License for the specific language governing permissions and%0A * limitations under the License.%0A */%0Apackage cz.cuni.mff.d3s.spl.core.impl.formula;%0A%0Aimport cz.cuni.mff.d3s.spl.core.Formula;%0Aimport cz.cuni.mff.d3s.spl.core.Result;%0A%0Apublic class LogicImply extends LogicOp %7B%0A%0A%09public LogicImply(Formula left, Formula right) %7B%0A%09%09super(left, right);%0A%09%7D%0A%0A%09/*%0A%09 * We are using Kleene three-value logic.%0A%09 */%0A%09@Override%0A%09public Result evaluate() %7B%0A%09%09Result leftResult = left.evaluate();%0A%09%09%0A%09%09/*%0A%09%09 * If the left one is FALSE, we do not need%0A%09%09 * to evaluate the right one.%0A%09%09 */%0A%09%09if (leftResult == Result.FALSE) %7B%0A%09%09%09return Result.TRUE;%0A%09%09%7D%0A%09%09%0A%09%09Result rightResult = right.evaluate();%0A%09%09%0A%09%09/*%0A%09%09 * If left is TRUE, the result solely depends on the%0A%09%09 * right operand.%0A%09%09 */%0A%09%09if (leftResult == Result.TRUE) %7B%0A%09%09%09return rightResult;%0A%09%09%7D%0A%09%09%0A%09%09/*%0A%09%09 * Last option - left is UNKNOWN. Final result can be TRUE%0A%09%09 * only if right operand is TRUE. Otherwise, the UNKNOWN%0A%09%09 * takes over.%0A%09%09 */%0A%09%09assert leftResult == Result.CANNOT_COMPUTE;%0A%09%09%0A%09%09if (rightResult == Result.TRUE) %7B%0A%09%09%09return Result.TRUE;%0A%09%09%7D else %7B%0A%09%09%09return Result.CANNOT_COMPUTE;%0A%09%09%7D%0A%09%7D%0A%0A%7D%0A

Add LogicImply class