不要为符号指定具体值

Question

我使用Z3来解决一些约束。

我发明了一个表达式“x^m@mx where x noteq T”。有人提供“S^a”。

我们知道“x^m@mx where x noteq T”可以以“S^a”开头，条件是“x=S,a=m, x noteeq T”。

由于此条件是可满足的，因此通过应用该条件，“x^m@mx where x noteeq T”将计算为“S^a@aS”。

所以，我想用Z3来检查条件是否满足。

var ctx = new Context();

EnumSort domain = ctx.MkEnumSort("domain", new string[] { "S", "T"});

var x = ctx.MkConst("x", domain);
var m = ctx.MkConst("m", domain);
var a = ctx.MkConst("a", domain);

var solver = ctx.MkSolver();
solver.Add(ctx.MkEq(x, domain.Const(0))); // x=S
solver.Add(ctx.MkEq(a, m)); // a=m
solver.Add(ctx.MkNot(ctx.MkEq(x, domain.Const(1)))); // x noteq T

if (solver.Check() == Status.SATISFIABLE)
{
    Console.WriteLine(solver.Model);
}
else
    Console.WriteLine("Not satisfiable");

模型为m=S，a=S，x=S。这是错误的，因为我的表情会变成“S^S@SS”

我想将

a

保留为未分配状态，因为以后的用户可以为

a

提供具体值。

那么如何阻止 Z3 给

a

赋值呢？

向我展示Python代码就可以了。

Answer 1

您的问题相当令人困惑：您到底想满足哪些约束？但是，一般来说，SMT 求解器不计算符号模型。也就是说，当他们确定

sat

时，就会对所有变量进行赋值。 （请注意，如果没有对变量强制执行特定选择，那么它们将采用可能的值之一。）

因此，如果您不希望

a

接收值，请不要将其作为系统的参数：

from z3 import *

domain, (S, T) = EnumSort('domain', ('S', 'T'))

x = Const('x', domain)
m = Const('m', domain)

s = Solver()
s.add(x == S)
s.add(x != T)

if s.check() == sat:
    print(s.model())
else:
    print("Unsat")

当然，上面的内容毫无意义：如果你有

s.add(x == S)

，那么

s.add(x != T)

就无关紧要了，因为

x == S

自动暗示了枚举类型的

x != T

。