Z3 中的变量选择
Variable selection in Z3
有没有什么办法可以找到sat_solver.cpp(solver::next_var)或smt_case_split_queue.cpp( next_case_split(bool_var & next, lbool & phase))?我知道这并不简单，但是有人可以给我一些提示吗？
提前谢谢你。
是的，这是可能的，但可能需要大量工作。该公式在到达 SAT 求解器之前会经历多次转换。它们每个都有自己的映射（如果它们 introduce/remove 变量），因此获取最后完成的映射可能无法让您到达想要的位置。
您要查找的映射很可能是 atom2bool_var, but those Boolean variables are (most likely) introduced in the bit-blaster, which has its own model converter that translates those back to bit-vector variables as demonstrated in bit_blaster_model_converter.cpp。
有没有什么办法可以找到sat_solver.cpp(solver::next_var)或smt_case_split_queue.cpp( next_case_split(bool_var & next, lbool & phase))?我知道这并不简单，但是有人可以给我一些提示吗？
提前谢谢你。
是的，这是可能的，但可能需要大量工作。该公式在到达 SAT 求解器之前会经历多次转换。它们每个都有自己的映射（如果它们 introduce/remove 变量），因此获取最后完成的映射可能无法让您到达想要的位置。
您要查找的映射很可能是 atom2bool_var, but those Boolean variables are (most likely) introduced in the bit-blaster, which has its own model converter that translates those back to bit-vector variables as demonstrated in bit_blaster_model_converter.cpp。