Skip to content

Instantly share code, notes, and snippets.

@lectricas
Created July 1, 2022 10:48
Show Gist options
  • Save lectricas/de256203de480e39e436ef35bfec4c49 to your computer and use it in GitHub Desktop.
Save lectricas/de256203de480e39e436ef35bfec4c49 to your computer and use it in GitHub Desktop.
prop solver
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))
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment