• 検索結果がありません。

定義モジュール

# definitions.py

# 論理式記述を行うために必要となる補助的な関数や述語の定義週

# 日付けに関しては，1年12月，1月30日 と簡単化

from z3 import *

from essentials import * d1,d2,d3=Ints(’d1 d2 d3’) d=Int(’d’)

### OR,AND,NOT,IF:論理演算子Or,And,Not,Ifの高階化 ###

# 主に，日付けパラメータd(日)，m(月)に関して高階化し，記述のコンパクト化を計る.

# 法文の文章表現との対応が付けやすい反面，日付けパラメータが隠れることによる

# 理解性の低下の問題もある．内容的には，

# OR(p,q,..,r)(d)==Or(p(d),q(d),..,r(d))

# AND(p,q,..,r)(d)==And(p(d),q(d),..,r(d))

# NOT(p)(d)==Not(p(d))

# IF(p,q,r)(d)==If(p(d),q(d),r(d))

from functools import reduce OR=(lambda *args:(lambda d:

reduce(Or,[x(d) for x in args],False))) AND=(lambda *args:(lambda d:

reduce(And,[x(d) for x in args],True))) NOT=lambda f:(lambda d:Not(f(d)))

IF=lambda p,q,r:lambda d:If(p(d),q(d),r(d)) FALSE=lambda d:False

TRUE=lambda d:True

### 日付けのための述語，関数 ###

# 1900年1月1日を起点とした日数，月数で日，月を表現

# 以下，1<=d=<30, 1<=m=<12

通日=lambda y,m,d:(y-1900)*360+(m-1)*30+d-1 # 西暦y年、m月、d日の通日

属月=lambda d:d/30 # 通日dの属する月 偶数月=lambda m:m%2==0

前月=lambda f:lambda m:EXists(d,And(f(d),属月(d)==m+1))

# 前月(f):fが成立する日の前の月に対してのみTrue

# f:日->Bool, 前月(f);月->Bool

# 日の区間，月の区間，当日，当月

# 以下，x,x1,x2:(year,month,day) DD=(lambda x1,x2:lambda d:

And(通日(x1[0],x1[1],x1[2])<=d,d<=通日(x2[0],x2[1],x2[2])))

# DD((1977,4,1),(1998,9,30))==lambda d:And(通日(1977,4,1)<=d,d<=通日(1996,9,30)) MM=(lambda x1,x2:lambda m:

And(通月(x1[0],x1[1])<=m,m<=通月(x2[0],x2[1])))

# MM((1955,5),(1977,3))==lambda m:And(通月(1955,5)=<m,m=<通月(1977,3)) D=lambda x:lambda d:d==通日(x[0],x[1],x[2])

M=lambda x:lambda m:m==通月(x[0],x[1])

# 年齢汎用：誕生日が西暦(y,m,d)である人の通日ddにおける年齢

年齢汎用=lambda y,m,d:lambda dd,age:age==(dd-通日(y,m,d)+1)/360 年齢が達する日=(lambda y:(lambda d:And(年齢(d-1,y-1),年齢(d,y))))

# 年齢は年金原簿honnin_xxで定義されている．

# 年号

昭和=lambda y:y+1925 平成=lambda y:y+1988 令和=lambda y:y+2018

### 充足リスト ###

# i=0〜m-1のなかで条件f(i)を満たすiからなるリスト def 充足リスト(f,m):

v=[]

i,i0=Ints(’i i0’) p=f(i)

for n in range(0,m):

s=Solver() s.add(p)

if s.check()==sat:

i0=s.model()[i]

v=v+[i0]

p=And(p,i!=i0) else:

break return v

# p=lambda i:And(10<i,i<15)

# print(充足リスト(p,20))

# [11, 12, 13, 14]

#### 月数 ####

# i=0〜499のなかで条件f(i)を満たすiの個数

# 被保険者の資格に必要な480月（40年間）をカバー def 月数(f):

m=500 v=0

i,i0=Ints(’i i0’) p=f(i)

for n in range(0,m):

s=Solver() s.add(p)

if s.check()==sat:

i0=s.model()[i]

v=v+1

p=And(p,i!=i0) else:

break return v

# p=lambda i:And(10<i,i<15)

# print(月数(p))

# 4

### 期間，期間2，期間3 ###

# 以下で，f,g,h:日->{True,False}

# 期間の端点を算入する仕方により3種類がある．

## 期間 ##

# 条件fを最初に満たす日d1の翌月から，条件gを最初に満たす日d2の属月まで月の集合．

# このようなf,gの対が複数ある場合は，それらの期間を合算したもの.

# ...f...g....f...g...

# - - = =

# f,gが同じ月に起きるときには，その月は含まれない．

期間=(lambda f,g:(lambda m:

Exists(d1,

And(f(d1),属月(d1)+1<=m, ForAll(d2,

Implies(And(g(d2),d1<=d2), m<=属月(d2)))))))

# f=lambda d:Or(d==100,d==300)

# g=lambda d:Or(d==200,d==400)

# print(充足リスト(期間(f,g),20))

# # [4, 5, 6, 11, 12, 13]

# print(time.time()-start) # 73 msec

## 期間2 ##

# 条件fを最初に満たす日d1の属月から，条件gを最初に満たす日d2の前月まで月の集合．

# このようなf,gの対が複数ある場合は，それらの期間を合算したもの．

# ...f...g....f...g...

# - - = =

# f,gが同じ月に起きるときには、その月は含まれる。

期間2=(lambda f,g:(lambda m:

Exists(d1,

And(f(d1),属月(d1)<=m, Or(ForAll(d2,

Implies(And(g(d2),d1<=d2), m<=属月(d2)-1)), And(属月(d1)==m,

Exists(d2,And(g(d2),属月(d2)==m))))))))

# f=lambda d:Or(d==100,d==300, d==500, d==530, d==532)

# g=lambda d:Or(d==200,d==400, d==500, d==531, d==533)

# print(充足リスト(期間2(f,g),20))

# #[3, 4, 5, 10, 11, 12, 16,17]

## 期間3 ##

# fが成立する日の属月の前の月から、fが成立しなくなる日の属月までの月の集合

# このような期間が複数ある場合は、それらを合算したもの

期間3=(lambda f:(lambda m:

Exists(d1,

And(f(d1),属月(d1)-1<=m, ForAll(d2,

Implies(And(Not(f(d2)),d1<=d2), m<=属月(d2)))))))

# f=(lambda d:Or(And(100<=d,d<=200),And(300<=d,d<=400)))

# print(充足リスト(期間3(f),20))

# [2, 3, 4, 5, 6, 9, 10, 11, 12, 13]

### 事由の成立関係 ###

# 月mのうちで，条件fが成立する日dがあり，その後g,hが成立する日はない．

月内で最後に成立=(lambda f,g,h:(lambda m:

Exists(d,

And(m==属月(d), f(d),

ForAll(d1,

Implies(And(d<=d1,m==属月(d1)), Not(Or(g(d1),h(d1)))))))))

前に成立=(lambda f,g:

Exists([d1,d2],And(f(d1),g(d2),d1<d2))) 以前に成立=(lambda f,g:

Exists([d1,d2],And(f(d1),g(d2),d1<=d2))) 同日に成立=(lambda f,g:

間で成立=(lambda f,g,h:

Exists([d1,d2,d3],And(f(d1),g(d2),h(d3),d1<d2,d2<=d3)))

# 前日不成立，当日成立

成立に至る=(lambda f:(lambda d: And(Not(f(d-1)),f(d))))

# definitions_date.py

# 論理式記述を行うために必要となる補助的な関数や述語の定義週

# 西暦による日付けに対応している．

# definition.py に比べると (y,m,d)<=>通日 の計算が複雑になるために

# 属月，期間などを計算するコストが大きくなる．これを解決するために，

# 充足リスト，月数，期間などのアルゴリズムが工夫されている．

from z3 import *

#### z3変数 ####

# "_"で始まるものは，ForAll,Existsの束縛変数用，Python処理系でForAll,EXists

# の束縛変数を特別扱いしないので，名前の衝突を防ぐため．

d,d1,d2,d3=Ints(’d d1 d2 d3’)

m,m1,m2,n,n1,mjd=Ints(’m m1 m2 n n1 mjd’) x,x1,x2,y,y1,y2=Ints(’x x1 x2 y y1 y2’) a,a1,a2,b,b1,b2=Ints(’a a1 a2 b b1 b2’) _d,_d1,_d2,_d3=Ints(’_d _d1 _d2 _d3’) _a,_a1,_a2,_a3_=Ints(’_a _a1 _a2 _a3’) _b,_b1,_b2,_b3=Ints(’_b _b1 _b2 _b3’)

_m,_m1,_m2,_n,_n1,_mjd=Ints(’_m _m1 _m2 _n _n1 _mjd’) _x,_x1,_x2,_y,_y1,_y2=Ints(’_x _x1 _x2 _y _y1 _y2’)

### OR,AND,NOT,IF:論理演算子Or,And,Not,Ifの高階化 ###

# 主に，日付けパラメータd(日)，m(月)に関して高階化し，記述のコンパクト化を計る.

# 法文の文章表現との対応が付けやすい反面，日付けパラメータが隠れることによる

# 理解性の低下の問題もある．内容的には，

# OR(p,q,..,r)(d)==Or(p(d),q(d),..,r(d))

# AND(p,q,..,r)(d)==And(p(d),q(d),..,r(d))

# NOT(p)(d)==Not(p(d))

# IF(p,q,r)(d)==If(p(d),q(d),r(d))

from functools import reduce OR=(lambda *args:(lambda d:

reduce(Or,[x(d) for x in args],False)))

reduce(And,[x(d) for x in args],True))) NOT=lambda f:(lambda d:Not(f(d)))

IF=lambda p,q,r:lambda d:If(p(d),q(d),r(d)) FALSE=lambda d:False

TRUE=lambda d:True

#### 日付けのための述語，関数 ####

# 通日： 西暦年，月，日＝＞ユリウス通日，関数

# Year：ユリウス通日＝＞西暦年，述語

# Month: ユリウス通日＝＞月，述語

# 属月：ユリウス通日＝＞ユリウス通月，述語

#    期間など属月を利用しているものも対応

# 年齢: 誕生日＝＞通日＝＞年齢，述語

# 昭和，平成，令和：和暦年＝＞西暦年

def 通日(y,m,d):

y1=If(m<=2,y-1,y) m1=If(m<=2,m+12,m) d1=36525*y1/100 d2=y1/400

d3=y1/100

m2=3059*(m1-2)/100

mjd=d1+d2-d3+m2+d-678912 return mjd

Year=(lambda mjd,y: # mjd => 西暦年 Exists([_a,_a1,_a2,_b,_b1,_m1,_n,_y1],

And(

_n==mjd+678881,

_a2==(4*(_n+1)/146097+1), _a1==(3*_a2/4),

_a==4*_n+3+4*_a1, _b1==((_a%1461)/4), _b==5*_b1+2,

_y1==(_a/1461),

_m1==(_b/153+3),

y==If(_m1>=13,_y1+1,_y1))))

Month=(lambda mjd,m: # mjd => 西暦月 Exists([_a,_a1,_a2,_b,_b1,_m1,_n],

And(

_n==mjd+678881,

_a2==(4*(_n+1)/146097+1), _a1==(3*_a2/4),

_a==4*_n+3+4*_a1, _b1==((_a%1461)/4), _b==5*_b1+2,

_m1==(_b/153+3),

m==If(_m1>=13,_m1-12,_m1))))

Day=(lambda mjd,d: # mjd => 西暦 日 Exists([_a,_a1,_a2,_b,_b1,_n],

And(

_n==mjd+678881,

_a2==(4*(_n+1)/146097+1), _a1==(3*_a2/4),

_a==4*_n+3+4*_a1, _b1==((_a%1461)/4), _b==5*_b1+2,

d==(_b%153)/5+1)))

def mjd2ymd(mjd): # 通日 => (年、月、日) s=Solver()

s.add(Year(mjd,y),Month(mjd,m),Day(mjd,d),0<m,m<13,0<d,d<32,y>0) s.check()

y1=s.model()[y]

m1=s.model()[m]

d1=s.model()[d]

return (y1,m1,d1)

# ユリウス起点1858.11.17から西暦y年m月1日までの月数

def mjm2ym(mjm): # 通月 => (年、月) m=(mjm+10)%12+1

y=(mjm-m+11)//12+1858 return (y,m)

属月=(lambda d,m: #通日dを含む通月mに対してTrue Exists([_y,_m],

And(Year(d,_y), Month(d,_m),

m==(_y-1858)*12+_m-11)))

# d=>m は高速 solve(属月(300,m)) 68mse

# m=>d は非常に遅い solve(属月(d,30)) 1.5sec/回

偶数月=lambda m:m%2==1 # m:通月，通月は１８５８年１１月が起点 前月=lambda f:lambda m:EXists(d,And(f(d),属月(d)==m+1))

# 日の区間，月の区間，当日，当月

# 以下，x,x1,x2: (年,月,日) DD=(lambda x1,x2:lambda d:

And(通日(x1[0],x1[1],x1[2])<=d,d<=通日(x2[0],x2[1],x2[2])))

# DD((1977,4,1),(1998,9,30))==lambda d:And(通日(1977,4,1)<=d,d<=通日(1996,9,30)) MM=(lambda x1,x2:lambda m:

And(通月(x1[0],x1[1])<=m,m<=通月(x2[0],x2[1])))

# MM((1955,5),(1977,3))==lambda m:And(通月(1955,5)=<m,m=<通月(1977,3)) D=lambda x:lambda d:d==通日(x[0],x[1],x[2])

M=lambda x:lambda m:m==通月(x[0],x[1])

# 年齢汎用：誕生日が西暦(y,m,d)である人の通日ddにおける年齢 年齢汎用=(lambda yBirth,mBirth,dBirth:lambda d,age:

Exists([_y,_a1,_mjd], And(Year(d,_y),

_a1==_y-yBirth,

_mjd==通日(_y,mBirth,dBirth), age==_a1-If(d<_mjd-1,1,0))))

年齢が達する日=(lambda y:(lambda d:And(年齢(d-1,y-1),年齢(d,y))))

# 年齢は年金原簿honnin_xxで定義されている．

# 年号

昭和=lambda y:y+1925 平成=lambda y:y+1988 令和=lambda y:y+2018

#### 充足リスト ####

# i=0〜m-1のなかで条件f(i)を満たす相異なる最大m個のiからなるリスト

def 充足リスト(f,m):

v=[]

i,i0=Ints(’i i0’) p=f(i)

for n in range(0,m):

s=Solver() s.add(p)

if s.check()==sat:

i0=s.model()[i]

v=v+[i0.as_long()]

p=And(p,i!=i0) else:

break return sorted(v)

# p=lambda i:And(10<i,i<15)

# print(充足リスト(p,20))

# [11, 12, 13, 14] 45msec

#### 月数 ####

# 月数(h)

# hは月に関する述語、hが成立する月の数

# hが成立〜不成立のサイクルの回数がｍ回以内で、成立する月数の総数

def 月数(f):

f1=成立に至る(f) f2=成立に至る(NOT(f)) n=0

Lf1=充足リスト(f1,k) Lf2=充足リスト(f2,k) while Lf1!=[]:

n=n+Lf2[0]-Lf1[0]

Lf1=Lf1[1:]

Lf2=Lf2[1:]

return n

# リスト(f)

# 述語f(m)を満たすmからなるリストを計算

# fの成立から不成立までの区間を最大100区間まで探索

# 区間の検出に充足リスト関数を利用

# 直接的に充足リストを用いるより高速

def リスト(f):

k=100

f1=成立に至る(f) f2=成立に至る(NOT(f)) L=[]

Lf1=充足リスト(f1,k) Lf2=充足リスト(f2,k) while Lf1!=[]:

L=L+[m for m in range(Lf1[0],Lf2[0])]

Lf1=Lf1[1:]

Lf2=Lf2[1:]

return L

#### 期間 ####

# 以下で，f,g,h:日->{True,False}

# 条件fを最初に満たす日d1の翌月から，条件gを最初に満たす日d2の属月まで月の集合．

# このようなf,gの対が複数ある場合は，それらの期間を合算したもの.

# ...f...g....f...g...

# - - = =

# f,gが同じ月に起きるときには，その月は含まれない．

def 期間(f,g):

def term(m):

k=100 p=False

Lf=充足リスト(f,k) Lg=充足リスト(g,k) while Lf!=[]:

s=Solver()

s.add(属月(Lf[0],m1),属月(Lg[0],m2)) s.check()

m11=s.model()[m1]

m22=s.model()[m2]

p=Or(p,If(m11==m22,m==m11,And(m11<m,m<=m22))) Lf=Lf[1:]

Lg=Lg[1:]

return p return term

# f=lambda d:Or(d==通日(2020,8,17),d==通日(2040,8,17))

# g=lambda d:Or(d==通日(2030,10,13),d==通日(2050,10,13))

# solve(期間(f,g)(m)) #[m = 1942]

# print(time.time()-start) #0.32891321182250977

# print(充足リスト(期間(f,g),300)) #[1942~2063,2182~2303]

# print(time.time()-start) #2.871021032333374

#### 期間2 ####

# fが成立に至った日から、gが成立に至った日の前月までの月からなる期間。

# このようなペアが複数ある場合はそれらの期間の集合。

# f~gのサイクルがk回（100）以内でリストアップ

def 期間2(f,g):

def term2(m):

k=100 p=False

Lg=充足リスト(g,k) while Lf!=[]:

s=Solver()

s.add(属月(Lf[0],m1),属月(Lg[0],m2)) s.check()

m11=s.model()[m1]

m22=s.model()[m2]

p=Or(p,If(m11==m22,m==m11,And(m11<=m,m<m22))) Lf=Lf[1:]

Lg=Lg[1:]

return p return term2

# print(充足リスト(f,10)) #[59078, 66383]

# print(充足リスト(g,10)) #[62787, 70092]

# print(time.time()-start) #0.06526803970336914

# print(充足リスト(期間2(f,g),300)) #[1941~206,2181~2302]

# print(time.time()-start) #2.6776301860809326

#### 期間3 ####

# fが成立する日の属月の前の月から、gが成立する日の属月までの月の集合

# このような期間が複数ある場合は、それらを合算したもの

成立に至る=(lambda f:(lambda d: And(Not(f(d-1)),f(d))))

# hが成立する日の前月から、hが成立しなくなる日の月までの月の集合

# hの成立〜不成立のサイクルがｋ回以内の範囲で積算

# k=100

def 期間3(h):

h1=成立に至る(h) h2=成立に至る(NOT(h)) def term3(m):

k=100 p=False

Lh1=充足リスト(h1,100) Lh2=充足リスト(h2,100) while Lh1!=[]:

s=Solver()

s.add(属月(Lh1[0],m1),属月(Lh2[0],m2)) s.check()

m11=s.model()[m1]

m22=s.model()[m2]

p=Or(p,And(m11-1<=m,m<=m22)) Lh1=Lh1[1:]

Lh2=Lh2[1:]

return p return term3

# h=(lambda d:Or(And(通日(2020,8,17)<=d,d<=通日(2030,10,13)),

# And(通日(2040,8,17)<=d,d<=通日(2050,10,13))))

# solve(期間3(h)(m)) #[m = 2180]

# 0.3370368480682373 sec

# print(充足リスト(期間3(h),300)) #[1940~2063,2180~2303]

# 2.943574905395508 sec

### 事由の成立関係 ###

# 月mのうちで，条件fが成立する日dがあり，その後g,hが成立する日はない．

def 月内で最後に成立(f,g,h):

f1=lambda d:And(Not(f(d-1)),f(d)) f2=lambda d:And(f(d),Not(f(d+1))) g1=lambda d:And(Not(g(d-1)),g(d)) g2=lambda d:And(g(d),Not(g(d+1))) h1=lambda d:And(Not(h(d-1)),h(d)) h2=lambda d:And(h(d),Not(h(d+1))) def term4(m):

k=100 p=False

Lf1=充足リスト(f1,k) Lf2=充足リスト(f2,k) Lg1=充足リスト(g1,k) Lg2=充足リスト(g2,k) Lh1=充足リスト(h1,k) Lh2=充足リスト(h2,k)

s=Solver()

s.add(属月(Lf1[0],m1),属月(Lf2[0],m2)) s.check()

m11=s.model()[m1].as_long() m22=s.model()[m2].as_long() for d in Lg2+Lh2:

t=Solver()

t.add(属月(d,m11))

if t.check()==sat and Lf1[0]<d:

m11=m11+1 break else:

continue for d in Lg1+Lh1:

r=Solver()

r.add(属月(d,m22),Lf2[0]<d) if r.check()==sat:

m22=m22-1 break else:

continue

p=Or(p,And(m11<=m,m<=m22)) Lf1=Lf1[1:]

Lf2=Lf2[1:]

return p return term4

前に成立=(lambda f,g:

Exists([d1,d2],And(f(d1),g(d2),d1<d2))) 以前に成立=(lambda f,g:

Exists([d1,d2],And(f(d1),g(d2),d1<=d2))) 同日に成立=(lambda f,g:

Exists(d,And(f(d),g(d)))) 間で成立=(lambda f,g,h:

Exists([d1,d2,d3],And(f(d1),g(d2),h(d3),d1<d2,d2<=d3)))

### 前日不成立，当日成立 ###

成立に至る=(lambda f:(lambda d: And(Not(f(d-1)),f(d))))

今ダウンロードする "JAIST Repository: 法令..."

Outline

関連したドキュメント