Z3 FiniteDomain 似乎不适用于影响答案

【问题标题】：Z3 FiniteDomain doesn't seem to work with implicationsZ3 FiniteDomain 似乎不适用于影响
【发布时间】：2020-11-30 22:43:51
【问题描述】：

这是一个 Z3 程序，它创建两个变量 X 和 Y，它们不能相等，并且域的大小为 2：

var solver = ctx.MkSolver();

// Section A
var T = ctx.MkFiniteDomainSort("T", 2);
var a = ctx.MkNumeral(0, T);
var b = ctx.MkNumeral(1, T);
var x = ctx.MkConst("x", T);
var y = ctx.MkConst("y", T);

// Section B
//var a = ctx.MkInt(0);
//var b = ctx.MkInt(1);
//var x = ctx.MkIntConst("x");
//var y = ctx.MkIntConst("y");
//solver.Add(ctx.MkLe(a, x), ctx.MkLe(x, b));
//solver.Add(ctx.MkLe(a, y), ctx.MkLe(y, b));

// Section C
//solver.Assert(!ctx.MkEq(x, y));

// Section D
solver.Assert(ctx.MkImplies(ctx.MkEq(x, a), ctx.MkEq(y, b)));
solver.Assert(ctx.MkImplies(ctx.MkEq(x, b), ctx.MkEq(y, a)));
solver.Assert(ctx.MkImplies(ctx.MkEq(y, a), ctx.MkEq(x, b)));
solver.Assert(ctx.MkImplies(ctx.MkEq(y, b), ctx.MkEq(x, a)));

// Section E
//solver.Assert(ctx.MkEq(x, a));

var status = solver.Check();
Console.WriteLine(status);
Console.WriteLine(solver.Model);
Console.WriteLine(solver.Model.Eval(ctx.MkEq(x, a)));
Console.WriteLine(solver.Model.Eval(ctx.MkEq(y, b)));

// Should always be true, but doesn't work when only sections A and D are uncommented?
Console.WriteLine(solver.Model.Eval(ctx.MkImplies(ctx.MkEq(x, a), ctx.MkEq(y, b))));

我得到输出。

SATISFIABLE
(define-fun y () T
  0)
(define-fun x () T
  0)
true
false
false

这个模型显然不满足约束。我明确评估了第一个约束以进行仔细检查，实际上它是错误的。

如果我使用整数（B 部分而不是 A 部分）或添加额外的约束（C 和 E 部分），则不会出现同样的问题。

我错过了什么？我想使用 FiniteDomain，因为它比为整数添加边界更方便，但它的行为似乎完全不同。

【问题讨论】：

这看起来确实很奇怪。请在github.com/Z3Prover/z3/issues 报告，并根据您的发现更新此问题！
如果ctx.MkNumeral 实际上没有实例化排序FiniteDomain 的值，而是使用其他类型的值，则可以解释这一点。一些源代码 cmets 建议使用 Context.FromInt 创建特定的有限域值。
Patrick：这也是我最初的想法，但在这些情况下，z3 通常会引发排序错误。（我使用 Python 接口复制了相同的内容，它的行为也很奇怪，就像发布的 OP 一样。）我想知道是否有一些潜在的假设是有限域只能与定点引擎一起使用（即喇叭子句)，但如果是这种情况，z3 仍应吐出合理的错误消息。好奇。
@alias 有意义
我已提交github.com/Z3Prover/z3/issues/4842。

标签： z3 sat

【解决方案1】：

This GitHub issue 解释说FiniteDomain 仅适用于 Datalog 引擎，在其他用途中已损坏。

在 Z3 的其他引擎中使用枚举是正确的方法。

【讨论】：