题解作者：ksqsf
出题人、验题人、文案设计等：见 Hackergame 2021 幕后工作人员。
-
题目分类：math
-
题目分值：Co-Login（250）+ Co-UnitTest（250）
从过去到未来、从代码到可执行文件、从输入到输出、从人类到计算机、从不变式到测试样例，这样的活动我们称之为 Program（编程）。熟悉范畴论的你听说了这一点，立刻意识到，那么，也应该有 Co-Program！
你想成为世界上第一名 Co-Programmer，从未来向过去编程。你想到，早期有 36 位的计算机。那么，在 36 位计算机上编程是一种怎样的体验？抱着对这个问题的好奇心，你开始了 36 位计算机上的 Co-Program。
Co-Login
你找到了一台古老的 36 位计算机，但是必须有密码（flag）才能登录。幸运的是这台计算机有一个奇怪的密码恢复机制：连续输出 100 个 36 位无符号整数的运算表达式（加、减、乘、除、模、负数），每个表达式中可能含有变量，和这个表达式预期的运算结果。只要你可以在 2 分钟一口气连续 co-evaluate 出至少 90 个相应的变量赋值，就可以重置密码！作为 co-programmer，这应该难不倒你。
注意：并不会针对每个表达式反馈答案。只有在完成 100 轮回答后会给出一个总的判定结果。
你可以通过 nc 202.38.93.111 10700 来连接，也可以使用网页终端。
Co-UnitTest
成功重置了密码后，你可以 Co-Program 一个真正的程序了！通常来说，编写计算器的过程如下。
- 编写一个计算器。
- 随便运行一下，得出结果，手动验证，把验证过的结果作为单元测试。
作为一个真正的 Co-Programmer，你打算倒着来：根据输入输出倒推相应的算术表达式（仅含有自由变量 x 和 y，不含任何整数常数）。
你需要写一个使用了 x 和 y 的表达式（可以使用 if，但不可以使用任何整数常数）满足上述约束。在成功解决 10 组问题中的 7 组后，即可成为真正的 Co-Programmer！但是要抓紧时间，每组只有 30 秒。
你可以通过 nc 202.38.93.111 10800 来连接，也可以使用网页终端。
有关 Co-Programming-Language 的信息
所有整数均为 36 位无符号数。
可以使用的整数表达式的运算有：相反数 -、加法 +、减法 -、乘法 *、除法 /、取模 %。约定：除数为 0 时，除法结果为 2^36-1，求模结果为被除数。
还有一个整数类型的表达式：if(boolExpr,intExpr,intExpr)，当 boolExpr 求值为真时，结果是第二个参数，否则是第三个参数。（提示：Co-Login 中可以不考虑该运算。）
可以使用的布尔表达式有：true, false, intExpr<=intExpr, intExpr=intExpr, !boolExpr, boolExpr&&boolExpr, boolExpr||boolExpr。
如果你不知道
nc是什么，或者在使用上面的命令时遇到了困难，可以参考我们编写的 萌新入门手册：如何使用 nc/ncat？
这里给出本题的 Co-Question。这两道题目可以算是一些常用求解器的普及（？）。如果你点开了这一页，请至少记住 Z3——非常实用！
flag{z3isgood!-...}, 懒人解法的求解脚本
可以猜一组值。如果人品够好的话，是有可能猜对 90 组题的。
不就是 2^(36n) 个值嘛，买个好点的电脑穷举一下不就行了？
简单来说：直接使用 SMT 求解器，如 Z3。只需要写一个解析器把算式翻译成 SMT 表达式可以处理的格式，然后和 nc 对接即可。
不熟悉 SMT 求解器？下面是一个简单介绍：
所谓的 SMT 求解器解决的大体上是这样的问题：输入一些约束条件，求解器自动根据这些约束找出一组满足的变量赋值。以 Z3Py 为例：
from z3 import *
x, y, z = Ints('x y z')
s = Solver()
s.add(x == 100 * y + z)
s.add(y > x)
s.add(x > z)
print(s.check())
print(s.model())上面这段代码会打印出：
sat
[y = 1, z = -100, x = 0]
非常幸运的是，SMT 求解器都支持位向量（bit vector）！所以解出这道题只需要写一个脚本与 nc 对接，然后不断地自动求解即可。
最后，SMT 求解器的使用是非常值得掌握的技能，而且学起来也不难！强烈推荐学习！
这道题最不典型之处是 36 位整数。但仔细一想可以发现，每个表达式里自由变量数是有限的（不妨设为 n ）。那么，每个表达式可以看作输入 36n 个布尔值的运算。然后只需要根据算式列出这些布尔值的约束方程，最后解这个方程即可！
PS：实际上 SMT 求解器就是这么做的，在 desugar 掉上层 theory 后把求解交给 SAT 求解器（只处理布尔值）。
这是一道典型的 Program Synthesis 的题目——根据约束生成代码。（目前你看到的版本是使用了 5 组输入输出来约束题目，更早期的一个版本还有更复杂的约束，不过那样基本就只能用求解器做了，反而没什么意思了……？）
flag{dIdy0uUseCvC5?-...}, 懒人解法的求解脚本
可以猜一个表达式。题目都是完全随机生成的，所以人品够好的话是有可能猜对 7 题的。
不就是很多个表达式嘛，买个好点的电脑穷举一下不就行了？
假如你知道这道题是 Program Synthesis，就不用花时间想解法了，直接找一个求解器就行。这里我找到的是 CVC5。和上面一样，将约束翻译成 CVC5 可以识别的 SyGuS 格式，即可解决。
另一个可行的想法是利用 if 分支。先观察一组约束：
x=1, y=2, ans=3
我们可以针对这组约束给出一个满足的表达式：
ans=x+y
接着再看另一组约束：
x=2, y=1, ans=1
又可以针对这组约束给出一个满足的表达式：
ans=x-y
如何把这两个答案合起来呢？这时可以利用 if 区分这两组输入：
if(x>y,x-y,x+y)
只需把这个想法扩展到 5 组约束即可。这种做法的难点显然在于怎么区分不同的分支，只要能快速找出分支条件，自然可以做出来。当然，只要知道有现成的 Synthesizer，就可以直接借助于这些工具的力量把这些难点搞定了。
如果可以用常数，对约束 f(x[i], y[i]) = z[i] 可以随意构造出下面这样的解（这里换行了，实际上不能换行）：
if(x=x[0]&&y=y[0],
z[0],
...
if(x=x[3]&&y=y[3],
z[3],
z[4]))
于是想办法凑常数即可。观察到 （x!=0 时）:
x-x=0
x/x=1
(x/x)+(x/x)=2
(x/x)+(x/x)+(x/x)=3
(x/x)+(x/x)+(x/x)+(x/x)+(x/x)=5
于是可以先构造出质数表，然后根据利用整数的唯一分解就可以表示出所有的常数，最后构造出最简单的平凡解就搞定了。（但是实际上 nc 有输入长度限制，所以能不能做出来完全取决于常数好不好凑。）
题目约定除数为 0 时，除法结果为 0xfffffffff，求模结果为被除数，是因为 SMT 求解器基本都是这样规定的。所以不需要手动再进行额外处理了。