小编Mil*_*ion的帖子

你能告诉我如何逐步使用求解器Z3吗？而且,当我使用时v.name(),如何才能获得没有命题价值的模型？比如,在调用程序后cout<<v.name()<<m.get_const_interp(v);,我们可以得到模型 x = 3, p = true, y = 4,因为我不需要p = true,可以从模型集中删除吗？