问题：是否可以在z3中控制模型返回值的某种偏好？ 示例：给定以下命题逻辑公式,有2种可能的模型. > a：是的,b：是的,c：假(首选)> a：是的,b：假,c：真(仍然有效,只是“第二选择”) 我想通过布尔…