Model :: ConstInterp和Model :: Eval有什么区别？

我一直在使用ConstInterp来获取expr中的常量字面值。Model :: ConstInterp和Model :: Eval有什么区别？

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)

但是相同的代码评估和演示，而不是ConstInterp的罚款。我错误地使用了ConstInterp吗？

来源

2013-03-20 S.N.

对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。这种行为可以通过的第二参数设置为true，从而使模型完成，即可以改变，

s.Model.Eval(x, true)

将返回false。

作为替代方案，数组s.Model.ConstDecls包含常数的所有函数声明，这些常数在模型中有解释。不在这个集合中的常量没有解释，并且可以被假定为'不关心'，即任何值都可以被分配给它们。

来源

2013-03-26 15:59:27

Model :: ConstInterp和Model :: Eval有什么区别？

回答

相关问题