我一直在使用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 ?
对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。此行为可以通过将Eval()的第二个参数设置为true来改变，从而启用模型完成，即
s.Model.Eval(x, true)
将返回false。
作为替代，数组s.Model.ConstDecls包含所有在模型中有解释的常量的函数声明。不在此集合中的常量没有解释，可以假定为"不关心"，即可以为它们赋任何值。