11月24日：技术报告提交，截止时间17:00 11月25日-11月28日：初赛评审 11月29日：作品上传服务器，关闭参赛队服务器访问通道，截止时间17:00 11月30日-12月7日：复赛技术评审 12月8日-12月10日：技术验收成绩公示 12月中下旬：竞赛决赛（待通知）
单目运算符：
LOG NEG (!×) //逻辑非
BIT NEG (~x) //按位非
MINUS (-) //负号
双目运算符：
ADD (a + b)
SUB (a - b)
MUL (a * b)
DIV (a / b)
LOG_AND (a && b) //逻辑与
LOG_OR (a || b)//逻辑或
EQ (a == b)
NEQ (a != b)
LT (a < b)
LTE (a <= b)
GT (a > b)
GTE (a >= b)
BIT_AND (a & b) //按位与
BIT_OR (a | b)//按位或
BIT_XOR (a^b)//按位异或
RSHIFT (a >> b)
LSHIFT (a << b)
IMPLY (a -> b) // 等同于: (!a) || b
注： 除乘法和除法操作外，其他操作基本已经实现。
变量和常量位宽限制在64位以下，且都为 unsigned。
由于同一个约束表达式内可能有不同位宽的变量和常量，所以表达式需要做隐式类型转换，具体规则可参照IEEE Std 1800™-2017, IEEE Standard for SystemVerilog— Unified Hardware Design, Specification, and Verification Language， 11.6 Expression bit lengths.
每个测试题要求生成1000组随机解，这些解需要满足均匀概率分布。随机解按照json格式输出到文件。
思路： 假设经过统计有n条可满足路径经过BDD结点u，其中走u左分支的路径数为x，则走u右分支的路径数为n-x。 故在采样时，在u处走左分支的概率为x/n，走右分支的概率为(n-x)/n。
提交的执行脚本或文件需要支持参数 -seed ，比如 -seed 123456
不加-seed直接执行时，默认seed为0
这个seed作为随机种子，用于生成伪随机序列。在求解过程中需要用随机数时，要从该随机序列提取随机数。评审时，我们可以指定不同的seed，用于检查结果的随机性。
- simple_n5_m8_b8-16_t0.0311
- simple_n10_m10_b4-32_t0.051
- simple_n10_m10_b4-32_t0.053
- simple_n10_m10_b4-32_t0.0516
- simple_n10_m10_b4-32_t0.0518
- simple_n10_m15_b32-64_t0.8
- simple_n20_m20_b4-64_t1.6
- simple_n20_m20_b16-32_t13.7
- simple_n50_m50_b4-8_t4.3
- simple_n150_m100_b4-16_t0.3 合取时间过长
- medium_n20_m20_b4-64_t32.8
- medium_n20_m20_b4-64_t39.2
- medium_n20_m20_b4-64_t43.1
- medium_n20_m20_b16-32_t39.7
- medium_n25_m25_b4-32_t51.3
- medium_n25_m25_b4-32_t66.2 结点数多（297438个），统计时间长
- medium_n30_m30_b4-32_t21.3
- medium_n30_m30_b4-32_t65.9
- medium_n35_m35_b4-16_t34.6
- medium_n50_m50_b4-8_t31.1
- complex_n25_m25_b4-32_t109.8
- complex_n25_m25_b4-32_t168.7
- complex_n25_m25_b4-32_t183.9
- complex_n30_m30_b4-32_t132.4
- complex_n30_m30_b4-32_t149.9 结点数多（138044个），统计时间长
- complex_n35_m35_b4-16_t93.2
- complex_n35_m35_b4-16_t113.9
- complex_n40_m40_b4-8_t85.7
- complex_n40_m40_b4-8_t102.9
- complex_n50_m50_b4-16_t99.0
DO： 解决了常量问题
TODO： 完成逻辑左移和右移操作
DO： 基本实现了除乘除外的其他运算
TODO： 找到尽可能高效的方法实现乘法和除法运算
DO： 实现了变量乘常数的操作，以及完成了通过遍历BDD验证正确性的测试代码。
TODO： 完成乘数为变量的乘法操作和除法操作。
DO： 完成了乘法和除法操作
TODO： 检验程序正确性，调整代码
DO： 完善了代码的格式，提高了代码的复用性，尝试将约束合取在一起
TODO： 合取之后进行输出，可满足路径过多，爆内存
DO： 尝试测试给定文件，但是由于变量的重复定义导致错误，代码需要重构
TODO： 重构代码，解决问题，再次验证给定测试文件
DO： 修改代码，运行测试用例成功，但是尚未验证结果的正确性；登录服务器修改密码。
TODO： 完成输出格式的转换（二进制位向量转十六进制），验证赛题给出的部分解是否全部包含在输出文件中。
DO： 测试给定文件result.json，simple下的第一个测试文件（n5_m8_b8-16_t0.0311）全部可以满足，第二个测试文件（n10_m10_b4-32_t0.051）求解第八个约束，再进行合取时时间过长。
TODO： 继续验证其他测试数据，修改优化代码。
DO: 修改测试函数，提高复用性个和可读性；完善逻辑右移和逻辑左移的代码，使其右操作数可以为变量；数据规模增大，程序运行时间过长，可能需要优化算法。
TODO: 尝试解决随机采样问题
DO: 使用CUDD提供的变量排序优化，约束合取能够在合理时间内完成；测试代码，发现问题，取反操作在某些情况下需要先进行位扩展再进行取反。
TODO: 解决BUG，根据KCBox考虑如何进行采样。
DO： 位扩展问题解决了一部分。解决思路，即统一同一约束中的各个变量位宽为最大变量位宽。这种解决方法有较大问题，因为某些自决定位宽的运算符（逻辑运算符）会隔离位宽的统一。
TODO： 目前想到的方法，在计算约束前先遍历一遍约束树，统计各个运算符所在的子表达式中的最大位宽。
DO： 位扩展基本解决，测试文件全部通过，但是不能保证完全没有BUG；编写采样代码demo。
TODO： 检查代码是否存在其他BUG，完成采样代码，优化变量排序。
DO： 基本实现了采样代码，并且将采样结果输出到了json文件
TODO： 根据直播答疑结果可能要修改采样过程；选择较优的变量排序方法进行优化；优化代码，降低耦合，提高可读性。
DO： 彻底解决了位宽对齐问题
TODO： 优化代码；按照赛题要求提供执行接口和操作命令（随机数种子接口、输入输出文件路径等）。
DO： 解决了采样代码的算法BUG，提供了可执行文件的参数接口。
TODO： 验证reslut文件的正确性
DO： 代码基本完成，模型数过多，c++内置数据类型存不下，改用string存储；BDD采样时，结点唯一存在的表示是其索引和左右指针，故进行模型计算时不要重复，也不要漏掉。
TODO： 编写设计报告；将程序部署到服务器
DO： 修改采样代码，目前全部测试样例都可以得到满分
TODO： 编写设计文档；优化代码；部署到服务器
DO: 初步完成设计文档；程序已经部署到服务器；更新了采样部分的代码（展开归约后隐藏的路径）；编写了运行程序和测试程序的脚本文件
TODO： 进一步完成设计文档；优化程序