Hiroyuki Katsura
Hiroyuki Katsura
Oh, I'm sorry to use such non-released version of z3. But this bug also occurs with z3 4.8.7(commit id: 30e7c225cd510400eacd41d0a83e013b835a8ece, tag: z3-4.8.7).
Thanks! Actually, I have no problem to use z3-4.8.4, and now I'm using this version. I just wanted to inform other people and developers of the existence of that bug....
これ、問題の隣にSolver数を書いたらおおよその難易度が分かって良さそう
複数出力もそうですが、複数入力(配列的)も欲しい…
問題にやや限界を感じる(配列的に与えれば、実質無限の長さの入力が与えられるので、より一般化できて良さそう ここでいう配列的 というのは、同じところから複数の値が順番に出てくるみたいなのをイメージしています 例えば、現状は max を答える問題を作ろうとしてもたかだか10個くらいの入力から最も大きいのをそれぞれ比べていく、みたいなことをせざるをえないので、頭が悪いコードレベル0x73になってしまうのですが、配列的概念を導入すれば、各入力からの道と、それまでで最大の値を保持する回路を作っておけば良いので、実際のプログラミングとほとんど変わらないゲームになると思うんですよね。（実装も個人的にはそれほど難しくなさそうに思える（というか言うなら僕が実装しろやって話ではありそう））
入力を出すタイミング自体は順序を守れば任意で良さそうです(入力表の問題は残りますが)