Relation for n = m * q + r, with 0 <= r < m.

Examples

In this example we test for some n,m pairs that satisfies n = m * 3 + 1.

iex> use Ckini
iex> n = Var.new()
iex> for i <- 2..10 do
...>   r = run(n, divo(n, from_number(i), from_number(3), from_number(1)))
...>   assert [from_number(i*3+1)] == r
...> end

Convert an Elixir integer (>= 0) to a list-encoded numeral representing the number to be used by the relations.

Relation that holds for n > 1.

Relation for n < m.

Examples

iex> use Ckini
iex> n = Var.new()
iex> run(n, leo(n, from_number(3)))
[from_number(0), from_number(1), from_number(2), from_number(3)]

Relation that holds for n = b^q + r.

This relation doesn't spit out complete result yet. More investigation needed.

See https://github.com/shouya/ckini/issues/1.

Relation for n < m.

Examples

iex> use Ckini
iex> n = Var.new()
iex> run(n, lto(n, from_number(3)))
[from_number(0), from_number(1), from_number(2)]

Relation for n - m = k.

See pluso/3.

Relation for n * m = p.

Examples

iex> use Ckini
iex> n = Var.new()
iex> run(n, mulo(from_number(5), from_number(4), n))
[from_number(20)]
iex> m = Var.new()
iex> run({m, n}, mulo(m, n, from_number(12)))
[{from_number(1), from_number(12)},
 {from_number(12), from_number(1)},
 {from_number(2), from_number(6)},
 {from_number(4), from_number(3)},
 {from_number(6), from_number(2)},
 {from_number(3), from_number(4)}]

Relation for n + m = k.

Examples

iex> use Ckini
iex> n = Var.new()
iex> run(n, pluso(from_number(5), from_number(4), n))
[from_number(9)]
iex> m = Var.new()
iex> run({m, n}, pluso(m, n, from_number(3)))
[{from_number(3), from_number(0)},
 {from_number(0), from_number(3)},
 {from_number(1), from_number(2)},
 {from_number(2), from_number(1)}]

Convert a list-encoded numeral back to an Elixir integer.