在 Z3 Java api 中创建对 EnumSorts 的约束答案

【问题标题】：Creating constraints over EnumSorts in Z3 Java api在 Z3 Java api 中创建对 EnumSorts 的约束
【发布时间】：2022-01-22 06:46:24
【问题描述】：

我被困住了，需要你的帮助（我查阅了文档并查看了 Z3 github repo 中的主示例，但找不到我想做的示例）。

假设我想要一个包含所有 RGB（即红色、绿色、蓝色）颜色的枚举，并且我想对这个枚举施加约束，无论枚举是否包含任何特定颜色。

以下约束应评估为 Sat：enumRgb contains "red" && enumRgb contain "green"

此约束应评估为 UnSat：enumRgb 包含“粉红色”。

在代码中（它不完整，因为我被卡住了）它看起来像这样：

public Expr addEnumExpr() { 
  EnumSort rgbEnum = myCtx.mkEnumSort(myCtx.mkSymbol("rgbEnum"), myCtx.mkSymbol("red"), myCtx.mkSymbol("green"), myCtx.mkSymbol("blue")); 
  Symbol colorPink = myCtx.mkSymbol("pink"); 
  Expr enumExpr = myCtx.mkConst("enumExpr", rgbEnum); 
  return myCtx.mkEq(colorPink, enumExpr); 
}

注意：myCtx 是一个保存 Context 的全局变量。

所以我遇到的具体问题：

由于类型不兼容（colorPink 是符号），无法创建 equals 约束
为了检查枚举中是否包含某种颜色，equals 表达式是否正确？

【问题讨论】：

你已经问过这个问题并在这里得到了答案：stackoverflow.com/questions/70157458/…
没有。它不是。我问如何在枚举上创建一个特定的约束。一个简单的例子实际上会更有帮助
SMTLib 是一种类型化语言。这意味着您不能创建任何具有值pink 的枚举值。这就像问"hello" 是否是一个数字。在类型化系统中，这永远不会发生。
谢谢。这个答案实际上帮助了我。对不起，如果我原来的问题是愚蠢的或什么的
不用担心。当您得到答案并且您不接受/投票时，很难判断您是否还有其他问题或其他问题是否令人困惑。这就是堆栈溢出通常的工作方式。见这里：stackoverflow.com/help/someone-answers

标签： java z3 smt

【解决方案1】：

查看Z3Py tutorial，搜索“颜色”:-)

请注意，您不能为“pink”创建排序为rgbEnum 的表达式，因为结果显然不是排序为rgbEnum 的表达式。但是，您可以创建一个名为“pink”的常量/变量rgbEnum，例如Expr pink = myCtx.mkConst("pink", rgbEnum);，但永远不会为该常量分配任何不在枚举中的值。

【讨论】：

我理解它的方式是，如果我有一组值（即枚举 rgbColor）并且我想测试其他随机值（即其他颜色，例如“粉红色”）是否它们是该集合的一部分，那么 enumSort 不需要写入类型，因为我不能只询问枚举是否某个符号（例如“粉红色”）是其中的一部分。我理解正确吗？也感谢您的回答。
是的，没错。您需要一个包含所有颜色的类型/排序，然后才能对它们的子集进行陈述。