Main.java

package net.ivorius.proplogic;

import com.google.common.base.Function;
import net.ivorius.algebra.Algebra;
import net.ivorius.algebra.BoolAlgebra;

import javax.annotation.Nullable;

import java.text.ParseException;
import java.util.*;
import java.util.stream.Collectors;

import static net.ivorius.algebra.BoolAlgebra.*;

public class Main {

    private static void error(String x)
    {
        System.out.println(x);
        System.exit(1);
    }

    public static void main(String[] args) {

        if (args.length < 1)
            error("Need a function and an input!");

        String func = args[0];

        // Copied from my own Open Source projects. Yes, this is my work.
        Algebra<Boolean> algebra = new Algebra<>(
                parentheses("(", ")"),
                BoolAlgebra.equals("<=>"),
                implies("=>"),
                or("v"),
                and("^"),
                not("~")
        );

        try
        {
            String inp = Arrays.asList(args).subList(1, args.length).stream().collect(Collectors.joining(" "));

            switch (func)
            {
                case "help":
                    System.out.println("Commands:\nhelp, operators, parse X, tautology X, unsatisfiable X, satisfiable X, entails X,Y");
                    break;
                case "operators":
                    System.out.println("Parentheses: (X)\nEquals: X <=> Y\nImplies: X => Y\nOR: X v Y\nAND:X ^ Y\nNOT: ~X");
                    break;
                case "parse":
                    System.out.println(algebra.parse(inp).toString(String::toString));
                    break;
                case "tautology":
                    printResult(isTautology(algebra.parse(inp)));
                    break;
                case "unsatisfiable":
                    printResult(isUnsatisfiable(algebra.parse(inp)));
                    break;
                case "satisfiable":
                    printResult(!isUnsatisfiable(algebra.parse(inp)));
                    break;
                case "entails":
                    int commaIndex = inp.indexOf(",");
                    if (commaIndex < 0) error("No comma found!");
                    printResult(entails(algebra.parse(inp.substring(0, commaIndex)), algebra.parse(inp.substring(commaIndex + 1))));
                    break;
                default:
                    error("Invalid function!");
            }
        }
        catch (ParseException e)
        {
            error("Could not parse!");
        }
    }

    private static void printResult(boolean result)
    {
        System.out.println(result ? "True" : "False");
    }

    private static boolean entails(Algebra.Expression<Boolean> left, Algebra.Expression<Boolean> right)
    {
        return isTautology(new Algebra.Operation<>(implies("=>"), left, right));
    }

    public static boolean isTautology(Algebra.Expression<Boolean> expression)
    {
        return allResults(expression).stream().allMatch(Boolean::booleanValue);
    }

    public static boolean isUnsatisfiable(Algebra.Expression<Boolean> expression)
    {
        return allResults(expression).stream().noneMatch(Boolean::booleanValue);
    }

    public static List<Boolean> allResults(Algebra.Expression<Boolean> expression)
    {
        List<Boolean> result = new ArrayList<>();

        for (long i = 0; ; i++)
        {
            IterativeEvaluator evaluator = new IterativeEvaluator(i);
            result.add(expression.evaluate(evaluator));
            if (evaluator.wasFinal())
                break;
        }

        return result;
    }

    /**
     * Don't try this at home, kids.
     */
    public static class IterativeEvaluator implements Function<String, Boolean>
    {
        public final Map<String, Boolean> values = new HashMap<>();
        public long iteration;

        public IterativeEvaluator(long iteration)
        {
            this.iteration = iteration;
        }

        @Nullable
        @Override
        public Boolean apply(String input)
        {
            switch (input)
            {
                case "False":
                    return false;
                case "True":
                    return true;
            }

            if (!values.containsKey(input))
                values.put(input, ((iteration >> values.size()) & 1) == 1);

            return values.get(input);
        }

        public boolean wasFinal()
        {
            return values.values().stream().allMatch(Boolean::booleanValue);
        }
    }
}