589 lines
16 KiB
Kotlin
589 lines
16 KiB
Kotlin
package prolog.builtins
|
|
|
|
import org.junit.jupiter.api.Assertions.*
|
|
import org.junit.jupiter.api.Test
|
|
import org.junit.jupiter.api.assertThrows
|
|
import prolog.Substitutions
|
|
import prolog.ast.arithmetic.Float
|
|
import prolog.ast.arithmetic.Integer
|
|
import prolog.ast.terms.Variable
|
|
import prolog.logic.equivalent
|
|
|
|
class ArithmeticOperatorsTests {
|
|
@Test
|
|
fun `1 evaluates to 1`() {
|
|
val op1 = EvaluatesTo(
|
|
Integer(1),
|
|
Integer(1)
|
|
)
|
|
|
|
var result = op1.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "1 should be equal to 1")
|
|
assertTrue(result[0].isSuccess, "1 should be equal to 1")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "1 should not be rebound")
|
|
|
|
val op2 = EvaluatesToDifferent(
|
|
Integer(1),
|
|
Integer(1)
|
|
)
|
|
|
|
result = op2.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(0, result.size, "1 should not be different from 1")
|
|
}
|
|
|
|
@Test
|
|
fun `1 does not evaluate to 2`() {
|
|
val op1 = EvaluatesTo(
|
|
Integer(1),
|
|
Integer(2)
|
|
)
|
|
|
|
var result = op1.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(0, result.size, "1 should not be equal to 2")
|
|
|
|
val op2 = EvaluatesToDifferent(
|
|
Integer(1),
|
|
Integer(2)
|
|
)
|
|
|
|
result = op2.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "1 should be different from 2")
|
|
assertTrue(result[0].isSuccess, "1 should be different from 2")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "1 should not be rebound")
|
|
}
|
|
|
|
@Test
|
|
fun `2 + 3 evaluates to 5`() {
|
|
val op = EvaluatesTo(
|
|
Add(Integer(2), Integer(3)),
|
|
Integer(5)
|
|
)
|
|
|
|
var result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "2 + 3 should be equal to 5")
|
|
assertTrue(result[0].isSuccess, "2 + 3 should be equal to 5")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "2 + 3 should not be rebound")
|
|
|
|
val op2 = EvaluatesToDifferent(
|
|
Add(Integer(2), Integer(3)),
|
|
Integer(5)
|
|
)
|
|
|
|
result = op2.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(0, result.size, "2 + 3 should not be different from 5")
|
|
}
|
|
|
|
@Test
|
|
fun `2 + 3 evaluates to 4 + 1`() {
|
|
val op = EvaluatesTo(
|
|
Add(Integer(2), Integer(3)),
|
|
Add(Integer(4), Integer(1))
|
|
)
|
|
|
|
var result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "2 + 3 should be equal to 4 + 1")
|
|
assertTrue(result[0].isSuccess, "2 + 3 should be equal to 4 + 1")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "2 + 3 should not be rebound")
|
|
|
|
val op2 = EvaluatesToDifferent(
|
|
Add(Integer(2), Integer(3)),
|
|
Add(Integer(4), Integer(1))
|
|
)
|
|
|
|
result = op2.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(0, result.size, "2 + 3 should not be different from 4 + 1")
|
|
}
|
|
|
|
@Test
|
|
fun `1 evaluates to variable not sufficiently instantiated`() {
|
|
val op = EvaluatesTo(
|
|
Integer(1),
|
|
Variable("X")
|
|
)
|
|
|
|
var result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "One exception should be thrown")
|
|
assertTrue(result[0].isFailure, "One exception should be thrown")
|
|
var exceptions = result[0].exceptionOrNull()
|
|
assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
|
|
|
|
val op2 = EvaluatesToDifferent(
|
|
Integer(1),
|
|
Variable("X")
|
|
)
|
|
|
|
result = op2.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "One exception should be thrown")
|
|
assertTrue(result[0].isFailure, "One exception should be thrown")
|
|
exceptions = result[0].exceptionOrNull()
|
|
assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
|
|
}
|
|
|
|
@Test
|
|
fun `(1 + var) evaluates to 1 not sufficiently instantiated`() {
|
|
val op = EvaluatesTo(
|
|
Add(Integer(1), Variable("X")),
|
|
Integer(1)
|
|
)
|
|
|
|
assertThrows<IllegalArgumentException> { op.satisfy(emptyMap()) }
|
|
|
|
val op2 = EvaluatesToDifferent(
|
|
Add(Integer(1), Variable("X")),
|
|
Integer(1)
|
|
)
|
|
|
|
assertThrows<IllegalArgumentException> { op2.satisfy(emptyMap()) }
|
|
}
|
|
|
|
@Test
|
|
fun `1 is 1`() {
|
|
val op = Is(
|
|
Integer(1),
|
|
Integer(1)
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap())
|
|
|
|
assertTrue(result.any(), "1 should be equal to 1")
|
|
}
|
|
|
|
@Test
|
|
fun `1 is not 2`() {
|
|
val op = Is(
|
|
Integer(1),
|
|
Integer(2)
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertTrue(result.isEmpty(), "1 should not be equal to 2")
|
|
}
|
|
|
|
@Test
|
|
fun `bound-to-1-var is 1`() {
|
|
val t1 = Variable("X")
|
|
val op = Is(
|
|
t1,
|
|
Integer(1)
|
|
)
|
|
|
|
val result = op.satisfy(mapOf(t1 to Integer(1))).toList()
|
|
|
|
assertEquals(1, result.size, "X should be equal to 1")
|
|
assertTrue(result.first().isSuccess, "X should be equal to 1")
|
|
assertTrue(result.first().getOrNull()!!.isEmpty(), "X should not be rebound")
|
|
}
|
|
|
|
@Test
|
|
fun `bound-to-2-var is not 1`() {
|
|
val t1 = Variable("X")
|
|
val op = Is(
|
|
t1,
|
|
Integer(1)
|
|
)
|
|
|
|
val result = op.satisfy(mapOf(t1 to Integer(2)))
|
|
|
|
assertFalse(result.any(), "X should not be equal to 1")
|
|
}
|
|
|
|
@Test
|
|
fun `variable is 1`() {
|
|
val op = Is(
|
|
Variable("X"),
|
|
Integer(1)
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertFalse(result.isEmpty(), "X should be equal to 1")
|
|
assertTrue(result.first().isSuccess, "X should be equal to 1")
|
|
assertEquals(1, result[0].getOrNull()!!.size, "X should be rebound")
|
|
assertTrue(equivalent(Integer(1), result[0].getOrNull()!![Variable("X")]!!, emptyMap()), "X should be equal to 1")
|
|
}
|
|
|
|
@Test
|
|
fun `variable is 1 + 2`() {
|
|
val op = Is(
|
|
Variable("X"),
|
|
Add(Integer(1), Integer(2))
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertFalse(result.isEmpty(), "X should be equal to 3")
|
|
assertTrue(result.first().isSuccess, "X should be equal to 3")
|
|
|
|
val subs = result[0].getOrNull()!!
|
|
|
|
assertEquals(1, subs.size, "X should be rebound")
|
|
assertTrue(
|
|
equivalent(Integer(3), subs[Variable("X")]!!, emptyMap()),
|
|
"X should be equal to 3"
|
|
)
|
|
}
|
|
|
|
@Test
|
|
fun `var is var should throw`() {
|
|
val op = Is(
|
|
Variable("X"),
|
|
Variable("Y")
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "One exception should be thrown")
|
|
assertTrue(result[0].isFailure, "One exception should be thrown")
|
|
val exceptions = result[0].exceptionOrNull()
|
|
assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
|
|
}
|
|
|
|
@Test
|
|
fun `1 is var should throw`() {
|
|
val op = Is(
|
|
Integer(1),
|
|
Variable("X")
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "One exception should be thrown")
|
|
assertTrue(result[0].isFailure, "One exception should be thrown")
|
|
val exceptions = result[0].exceptionOrNull()
|
|
assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
|
|
}
|
|
|
|
/**
|
|
* ?- X = 1, Y = 1 + 2, X is Y.
|
|
* false.
|
|
*/
|
|
@Test
|
|
fun `var is bound-to-sum-var`() {
|
|
val t1 = Variable("X")
|
|
val t2 = Variable("Y")
|
|
|
|
val op = Is(t1, t2)
|
|
val map: Substitutions = mapOf(t1 to Integer(1), t2 to Add(Integer(1), Integer(2)))
|
|
|
|
val result = op.satisfy(map).toList()
|
|
|
|
assertEquals(0, result.size, "X should not be equal to Y")
|
|
}
|
|
|
|
@Test
|
|
fun `var is mul`() {
|
|
val op = Is(
|
|
Variable("X"),
|
|
Multiply(Integer(2), Integer(3))
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "X should be equal to 6")
|
|
assertTrue(result[0].isSuccess, "X should be equal to 6")
|
|
val subs = result[0].getOrNull()!!
|
|
assertEquals(1, subs.size, "X should be rebound")
|
|
assertTrue(
|
|
equivalent(Integer(6), subs[Variable("X")]!!, emptyMap()),
|
|
"X should be equal to 6"
|
|
)
|
|
}
|
|
|
|
@Test
|
|
fun `bound-var is mul`() {
|
|
val t1 = Variable("X")
|
|
|
|
val op = Is(
|
|
t1,
|
|
Multiply(Integer(2), Integer(3))
|
|
)
|
|
val map: Substitutions = mapOf(t1 to Integer(6))
|
|
|
|
val result = op.satisfy(map).toList()
|
|
|
|
assertEquals(1, result.size, "X should be equal to 6")
|
|
assertTrue(result[0].isSuccess, "X should be equal to 6")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "X should not be rebound")
|
|
}
|
|
|
|
@Test
|
|
fun `var is bound-to-mul`() {
|
|
val t1 = Variable("X")
|
|
val t2 = Variable("Y")
|
|
|
|
val op = Is(t1, t2)
|
|
val map: Substitutions = mapOf(t1 to Integer(6), t2 to Multiply(Integer(2), Integer(3)))
|
|
|
|
val result = op.satisfy(map).toList()
|
|
|
|
assertEquals(1, result.size, "X should be equal to Y")
|
|
assertTrue(result[0].isSuccess, "X should be equal to Y")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "X should not be rebound")
|
|
}
|
|
|
|
@Test
|
|
fun `2 is 4 div 2`() {
|
|
val op = Is(
|
|
Integer(2),
|
|
Divide(Integer(4), Integer(2))
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "2 should be equal to 4 / 2")
|
|
assertTrue(result[0].isSuccess, "2 should be equal to 4 / 2")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "2 should not be rebound")
|
|
}
|
|
|
|
@Test
|
|
fun `4 div 2 is var`() {
|
|
val op = Is(
|
|
Variable("X"),
|
|
Divide(Integer(4), Integer(2))
|
|
)
|
|
|
|
val result = op.satisfy(emptyMap()).toList()
|
|
|
|
assertEquals(1, result.size, "X should be equal to 2")
|
|
assertTrue(result[0].isSuccess, "X should be equal to 2")
|
|
val subs = result[0].getOrNull()!!
|
|
assertEquals(1, subs.size, "X should be rebound")
|
|
assertTrue(
|
|
equivalent(Integer(2), subs[Variable("X")]!!, emptyMap()),
|
|
"X should be equal to 2"
|
|
)
|
|
}
|
|
|
|
@Test
|
|
fun `bound-var is 4 div 2`() {
|
|
val t1 = Variable("X")
|
|
|
|
val op = Is(
|
|
t1,
|
|
Divide(Integer(4), Integer(2))
|
|
)
|
|
val map: Substitutions = mapOf(t1 to Integer(2))
|
|
|
|
val result = op.satisfy(map).toList()
|
|
|
|
assertEquals(1, result.size, "X should be equal to 2")
|
|
assertTrue(result[0].isSuccess, "X should be equal to 2")
|
|
val subs = result[0].getOrNull()!!
|
|
assertTrue(subs.isEmpty(), "X should not be rebound")
|
|
}
|
|
|
|
/**
|
|
* ?- between(1, 2, X), Y is 1 + X.
|
|
* X = 1, Y = 2 ;
|
|
* X = 2, Y = 3 .
|
|
*/
|
|
@Test
|
|
fun `between 1 and 2 plus 1 to get 2 and 3`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(2)
|
|
val t3 = Variable("X")
|
|
val t4 = Variable("Y")
|
|
|
|
val op = Conjunction(
|
|
Between(t1, t2, t3),
|
|
Is(t4, Add(Integer(1), t3))
|
|
)
|
|
}
|
|
|
|
@Test
|
|
fun `negate 1 to get -1`() {
|
|
val t1 = Integer(1)
|
|
|
|
val result = Negate(t1).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(-1), result.to, "negate(1) should be equal to -1")
|
|
}
|
|
|
|
@Test
|
|
fun `negate 0 to get 0`() {
|
|
val t1 = Integer(0)
|
|
|
|
val result = Negate(t1).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(0), result.to, "negate(0) should be equal to 0")
|
|
}
|
|
|
|
@Test
|
|
fun `negate -1 to get 1`() {
|
|
val t1 = Integer(-1)
|
|
|
|
val result = Negate(t1).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(1), result.to, "negate(-1) should be equal to 1")
|
|
}
|
|
|
|
@Test
|
|
fun `negate bound-to-1-var to get -1`() {
|
|
val t1 = Variable("X")
|
|
|
|
val map: Substitutions = mapOf(t1 to Integer(1))
|
|
|
|
val result = Negate(t1).simplify(map)
|
|
|
|
assertEquals(Integer(-1), result.to, "negate(1) should be equal to -1")
|
|
}
|
|
|
|
@Test
|
|
fun `negate 1 + 3 to get -4`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(3)
|
|
|
|
val result = Negate(Add(t1, t2)).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(-4), result.to, "negate(1 + 3) should be equal to -4")
|
|
}
|
|
|
|
@Test
|
|
fun `Add 1 and 2 to get 3`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(2)
|
|
|
|
val result = Add(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(3), result.to, "1 + 2 should be equal to 3")
|
|
}
|
|
|
|
@Test
|
|
fun `Add 1 and bound-to-2-var to get 3`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Variable("X")
|
|
|
|
val subs: Substitutions = mapOf(t2 to Integer(2))
|
|
val result = Add(t1, t2).simplify(subs)
|
|
|
|
assertEquals(Integer(3), result.to, "1 + 2 should be equal to 3")
|
|
}
|
|
|
|
@Test
|
|
fun `Subtract 1 and 2 to get -1`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(2)
|
|
|
|
val result = Subtract(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(-1), result.to, "1 - 2 should be equal to -1")
|
|
}
|
|
|
|
@Test
|
|
fun `Subtract 3 and 1 to get 2`() {
|
|
val t1 = Integer(3)
|
|
val t2 = Integer(1)
|
|
|
|
val result = Subtract(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(2), result.to, "3 - 1 should be equal to 2")
|
|
}
|
|
|
|
@Test
|
|
fun `Multiply 0 and 0 to get 0`() {
|
|
val t1 = Integer(0)
|
|
val t2 = Integer(0)
|
|
|
|
val result = Multiply(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(0), result.to, "0 * 0 should be equal to 0")
|
|
}
|
|
|
|
@Test
|
|
fun `Multiply 1 and 0 to get 0`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(0)
|
|
|
|
val result = Multiply(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(0), result.to, "1 * 0 should be equal to 0")
|
|
}
|
|
|
|
@Test
|
|
fun `Multiply 0 and 1 to get 0`() {
|
|
val t1 = Integer(0)
|
|
val t2 = Integer(1)
|
|
|
|
val result = Multiply(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(0), result.to, "0 * 1 should be equal to 0")
|
|
}
|
|
|
|
@Test
|
|
fun `Multiply 3 and 1 to get 3`() {
|
|
val t1 = Integer(3)
|
|
val t2 = Integer(1)
|
|
|
|
val result = Multiply(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(3), result.to, "3 * 1 should be equal to 3")
|
|
}
|
|
|
|
@Test
|
|
fun `Multiply 2 and 3 to get 6`() {
|
|
val t1 = Integer(2)
|
|
val t2 = Integer(3)
|
|
|
|
val result = Multiply(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(6), result.to, "2 * 3 should be equal to 6")
|
|
}
|
|
|
|
@Test
|
|
fun `Divide 1 and 1 to get 1`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(1)
|
|
|
|
val result = Divide(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(1), result.to, "1 / 1 should be equal to 1")
|
|
}
|
|
|
|
@Test
|
|
fun `Divide 2 and 2 to get 1`() {
|
|
val t1 = Integer(2)
|
|
val t2 = Integer(2)
|
|
|
|
val result = Divide(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(1), result.to, "2 / 2 should be equal to 1")
|
|
}
|
|
|
|
@Test
|
|
fun `Divide 12 and 3 to get 4`() {
|
|
val t1 = Integer(12)
|
|
val t2 = Integer(3)
|
|
|
|
val result = Divide(t1, t2).simplify(emptyMap())
|
|
|
|
assertEquals(Integer(4), result.to, "12 / 3 should be equal to 4")
|
|
}
|
|
|
|
@Test
|
|
fun `Divide 1 and 2 to get float`() {
|
|
val t1 = Integer(1)
|
|
val t2 = Integer(2)
|
|
|
|
val result = Divide(t1, t2).simplify(emptyMap())
|
|
|
|
assertTrue(equivalent(result.to, Float(0.5f), emptyMap()), "1 / 2 should be equal to 0.5")
|
|
}
|
|
}
|