prop solver

PropSolver.kt

package main.com.company.solver

import kotlin.test.assertFalse
import kotlin.test.assertTrue


class PropositionSolver {
    private var openBranches = 0

    fun solve(test: Prop): Boolean {
        openBranches = 0
        val tree = buildTree(test)
        openBranches = countBranches(tree)
        test(tree)
        return openBranches == 0
    }

    private fun countBranches(root: Node?): Int {
        if (root == null) {
            return 0
        }
        if (root.left == null && root.right == null) {
            return 1
        }
        return countBranches(root.left) + countBranches(root.right)
    }

    private fun test(root: Node?) {
        if (root == null) {
            return
        }

        if (root.prop is Varr) {
            testInternal(root, root.prop.a, !root.positive)
        }
        test(root.left)
        test(root.right)
    }

    private fun testInternal(root: Node?, a: String, positive: Boolean) {
        if (root == null) {
            return
        }
        if (root.prop is Varr && root.prop.a == a && root.positive == positive) {
            openBranches -= countBranches(root)
        } else {
            testInternal(root.left, a, positive)
            testInternal(root.right, a, positive)
        }
    }


    private fun buildTree(prop: Prop): Node {
        val tree = Node(prop, false)
        eval(tree)
        return tree
    }

    private fun eval(root: Node?) {
        if (root == null) {
            return;
        }
        evalSingle(root)
        evalDouble(root)
        eval(root.left)
        eval(root.right)
    }

    private fun evalSingle(node: Node?) {
        if (node == null || node.eval) {
            return
        }
        if (node.positive) {
            when (node.prop) {
                is Varr -> node.eval = true
                is Not -> {
                    val left = Node(node.prop.n, false)
                    addNode(node, left)
                    node.eval = true
                }
                is And -> {
                    val left = Node(node.prop.l)
                    val right = Node(node.prop.r)
                    addNode(node, left)
                    addNode(node, right)
                    node.eval = true;
                }
            }
        } else {
            when (node.prop) {
                is Not -> {
                    val left = Node(node.prop.n)
                    addNode(node, left)
                    node.eval = true;
                }
                is Or -> {
                    val left = Node(node.prop.l, false)
                    val right = Node(node.prop.r, false)
                    addNode(node, left)
                    addNode(node, right)
                    node.eval = true;
                }
                is Arr -> {
                    val left = Node(node.prop.l)
                    val right = Node(node.prop.r, false)
                    addNode(node, left)
                    addNode(node, right)
                    node.eval = true;
                }
            }
        }
        eval(node.left)
        eval(node.right)
    }


    private fun evalDouble(node: Node?) {
        if (node == null || node.eval) {
            return
        }
        if (node.positive) {
            when (node.prop) {
                is Or -> {
                    val left = Node(node.prop.l)
                    val right = Node(node.prop.r)
                    addNode(node, left, right)
                    node.eval = true;
                }
                is Arr -> {
                    val left = Node(node.prop.l, false)
                    val right = Node(node.prop.r)
                    addNode(node, left, right)
                    node.eval = true;
                }
            }
        } else {
            when (node.prop) {
                is And -> {
                    val left = Node(node.prop.l, false)
                    val right = Node(node.prop.r, false)
                    addNode(node, left, right)
                    node.eval = true;
                }
            }
        }
        eval(node.left)
        eval(node.right)
    }

    private fun addNode(where: Node?, whatLeft: Node, whatRight: Node? = null) {
        if (where == null) {
            return
        }
        if (where.left == null) {
            where.left = whatLeft
            where.right = whatRight
        } else {
            addNode(where.left, whatLeft, whatRight)
            addNode(where.right, whatLeft, whatRight)
        }
    }
}

interface Prop

data class Node(
    val prop: Prop,
    val positive: Boolean = true,
    var left: Node? = null,
    var right: Node? = null
) {

    var value = show(prop)

    var eval = false

    fun show(inner: Prop): String {
        return when (inner) {
            is Varr -> inner.a
            is Not -> "!(${show(inner.n)})"
            is Or -> "(${show(inner.l)} \\/ ${show(inner.r)})"
            is And -> "(${show(inner.l)} /\\ ${show(inner.r)})"
            is Arr -> "(${show(inner.l)} --> ${show(inner.r)})"
            else -> throw java.lang.IllegalStateException("can't be")
        }
    }
}

data class Varr(val a: String) : Prop
data class Not(val n: Prop) : Prop
data class Or(val l: Prop, val r: Prop) : Prop
data class And(val l: Prop, val r: Prop) : Prop
data class Arr(val l: Prop, val r: Prop) : Prop

fun main(args: Array<String>) {

    val solver = PropositionSolver()

    val test1 = Arr(Or(Varr("a"), Not(Varr("a"))), Or(Varr("b"), Not(Varr("b"))))
    val test2 = Arr(
        Or(Varr("p"), And(Varr("q"), Varr("r"))),
        And(Or(Varr("p"), Varr("q")), Or(Varr("p"), Varr("r")))
    )
    val test3 = Arr(Or(Varr("a"), Not(Varr("a"))), Or(Varr("b"), Varr("b")))
    val test4 = Arr(
        Or(Varr("p"), Varr("q")),
        Arr(Not(Varr("p")), Varr("q"))
    )
    assertTrue(solver.solve(test1))
    assertTrue(solver.solve(test2))
    assertFalse(solver.solve(test3))
    assertTrue(solver.solve(test4))
}