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())