Z3 中有 UnsignedIntSort 吗? [英] Is there an UnsignedIntSort in Z3?

问题描述

我在求解器中使用函数来模拟离散时间.问题是现在我们使用像 z3.Function('f', IntSort(), IntSort()) 这样的函数，函数的负输入值在这里真的不适用，因为时间从 t 开始=0.当我想证明事情时，这会导致问题，因为求解器找到了根本不应该考虑的负时间解决方案.

I am using functions in my solver to model discrete time. The problem is that right now we use functions like z3.Function('f', IntSort(), IntSort()) and negative input values to the functions is really not applicable here because time starts at t=0. This causes problems when I want to proove things because the solver finds negative time solutions that should not be considered at all.

所以我的问题是:z3 中是否有某种无符号整数排序(UnsignedIntSort)?

So my question is: Is there some kind of unsigned int sort (UnsignedIntSort) in z3?

推荐答案

正如评论中指出的，没有这样的排序；最好的办法是确保所有用途都有 t >= 0 断言.

As pointed out in the comments, there's no such sort; and your best bet is to make sure you have t >= 0 assertions for all uses.

请注意，这在实践中实际上更棘手.您不仅需要对所​​有新鲜"变量进行此断言，而且每当您对这些变量进行任何算术运算以确保结果保留在域内时，都需要进行此断言.也就是说，如果您曾经计算过 t-1，那么您将希望 t >= 1 作为断言出现，假设该表达式的结果用作时间价值本身.

Note that this is actually trickier in practice. Not only you need to make this assertion for all your "fresh" variables, but also whenever you do any arithmetic with such variables to ensure the results remain within the domain. That is, if you ever compute t-1, then you'll want t >= 1 as an assertion appearing, assuming the result of that expression is used as a time value itself.

这会很快变得非常乏味，因此拥有一种机制(重载算术")可以简化生活.但当然，这取决于您如何对约束进行编程，是使用 SMT-Lib，还是通过高级语言使用其中一种 API.

This can get really tedious really quick, so having a mechanism ("overloaded arithmetic") can simplify life. But of course, that depends on exactly how you are programming your constraints, whether you're using SMT-Lib, or one of the APIs via a higher-level language.

这篇关于Z3 中有 UnsignedIntSort 吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！