Solver()命令创建一个通用求解器。我们可以通过add函数添加约束条件。我们称之为声明约束条件。check()函数解决声明的约束条件,sat结果表示找到某个合适的解,unsat结果表示没有解。这时候我们称约束系统无解。最后,求解器可能无法解决约束系统并返回未知作为结果。
对于上面的题目我们首先定义x1,x2,x3,x4四个int变量,然后添加逆向中的约束条件,最后进行求解。Z3会在找到合适解的时候返回sat。我们认为Z3能够满足这些约束条件并得到解决方案。该解决方案被看做一组解决约束条件的模型。模型能够使求解器中的每个约束条件都成立。最后我们遍历model中的解。
得到x1,x2,x3,x4的解后,我们将其代入逆向题中,得出v1,v2,v7,v8,v9,v9,v10,v11,v12的值,然后进行下一步的求解: