1

我一直在使用 ConstInterp 来获取 expr 中常量文字的值。

model.ConstInterp(lit)

但是我遇到了一个奇怪的错误

... <body of some loop>
let x = model.ConstInterp(lit)
if solver.Check() == Status.SATISFIABLE
then model.ConstInterp(lit)

第二次调用 ConstInterp 产生错误

Unhandled Exception: Microsoft.Z3.Z3Exception: invalid argument
   at Microsoft.Z3.Native.Z3_model_get_const_interp(IntPtr a0,IntPtr a1,IntPtr a2)
   at Microsoft.Z3.Model.ConstInterp(FuncDecl f)
   at Microsoft.Z3.Model.ConstInterp(Expr a)

但是，使用 Eval 而不是 ConstInterp 的相同代码很好。我是否错误地使用了 ConstInterp？

4

1 回答 1

1

第一次调用 model.ConstInterp() 使用在之前调用 Check() 期间构建的模型，因此它可能包含不同的常量解释，但这只是这里的次要问题。

并不要求所有的常数在每个模型中都有一个解释，例如，当一个常数的赋值不需要满足所有的约束时，它可以不被赋值（因此在模型中缺失）。例如，考虑以下程序：

Solver s = ctx.MkSolver();
s.Add(ctx.MkOr(
    ctx.MkEq(x, ctx.MkTrue()),
    ctx.MkEq(x, ctx.MkFalse()))); // Assert x = false OR x = true
s.Add(ctx.MkEq(y, ctx.MkTrue())); // Assert y = false
s.Check(); // Returns Status.SATISFIABLE

这个程序没有约束x，但它确实有约束y。因此，模型将不包含值，x并将s.Model.ConstInterp(x)抛出一个断言。调用s.Model.Eval(x)不会抛出断言，但它也不会评估x；在这种情况下，我们得到s.Model.Eval(x) == x. 可以通过将第二个参数 of 设置Eval()为 true 来更改此行为，从而启用模型完成，即

s.Model.Eval(x, true)

将返回false。

作为替代方案，该数组s.Model.ConstDecls包含所有在模型中具有解释的常量的函数声明。不在该集合中的常量没有解释，可以假定为“无关”，即可以为它们分配任何值。

于 2013-03-26T15:59:27.453 回答