如何解决基于几个约束合成一个布尔表达式
我需要的非常简单,我正在寻找一个工具/库 约束格式如下:
{"vars": {a=2,b=1,c=3},"eval": "False"}
{"vars": {a=1,c=2},"eval": "True"}
{"vars": {a=1,b=2,c=1},"eval": "True"}
然后根据预定义的符号为我合成一个布尔表达式:
Symbols: ["between variables": ['<=','>=','<','>','==','!='],"between expressions": ['and','or']]
对于这个系统,我只需要一个解决方案;例如,一个可以是
a == b or b == c or a == c
我一直在研究 Z3 库功能,但找不到任何有用的东西。如果您知道合适的工具,请告诉我。
解决方法
程序综合是一个非常活跃的研究领域;您将获得的程序质量实际上取决于您要使用的程序模板类型。 SMT 求解器很可能不会为您提供您正在寻找的那种开箱即用的程序,尽管它们会工作。
以下是我对您当前问题进行编码的方式:我将使用未解释的函数并将“测试用例”添加为约束。像这样:
(declare-fun f (Int Int Int) Bool)
(assert (not (f 2 1 3)))
(assert (f 1 1 2))
(assert (f 1 2 1))
(check-sat)
(get-model)
当我运行这个时,z3 说:
sat
(
(define-fun f ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
(ite (and (= x!0 2) (= x!1 1) (= x!2 3)) false
true))
)
如果您阅读输出,您会发现它基本上合成了以下程序:
if (a == 2) && (b == 1) && (c == 3)
then False
else True
这是正确的吗?绝对地。这真的是你想要它做的吗?很可能不是。但是开箱即用,您不会从 SMT 求解器中获得更好的效果。
要使用基于 SMT 的技术合成很酷的程序,请参阅 Emina Torlak 的研究。下面是一篇很好的论文:http://synapse.uwplse.org
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。