z3

Extract 、難しいですよね。リストのスライスっぽく使える関数を用意しました

def extract_as_list(x, l=None, r=None):
    """
    splice [l, r)

    011110011.....1011
    ^^^^^^^^^         ^
    012345678.........size
    """
    size = x.size()
    if l is None:
        l = 0
    if r is None:
        r = size
    l = (size - l - 1) % size
    r = (size - r) % size
    return Extract(l, r, x)

fibonacci数列を解く

from z3 import Solver, Context, RecFunction, RecAddDefinition, IntSort, Int, If, simplify

ctx = Context()
f = RecFunction("f", IntSort(ctx), IntSort(ctx))
x = Int("x", ctx)
RecAddDefinition(f, x, If(x <= 2, 1, f(x-1) + f(x-2)))

solver = Solver(ctx=ctx)
solver.add(f(x) == 10946)

print(solver.check())
print(solver.model())

RecFunctionを使って再帰的な式を解く例

from z3 import Solver, Context, RecFunction, RecAddDefinition, IntSort, Int, If, simplify

ctx = Context()
f = RecFunction("f", IntSort(ctx), IntSort(ctx))
x = Int("x", ctx)
RecAddDefinition(f, x, If(x <= 2, 1, f(x-1) + f(x-2)))

solver = Solver(ctx=ctx)
solver.add(f(x) == 10946)

print(solver.check())
print(solver.model())