解决优化问题的一种方法是使用SMT求解器来询问是否存在(坏)解决方案,然后逐步添加更严格的成本约束,直到命题不再可满足为止.例如,在http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/中讨论了这种方法.08_isvlsi_optprob.pdf.
这种方法有效吗？也就是说,当尝试用额外的约束来解决时,解算器会重复使用先前解决方案中的信息吗？
我正在尝试将 z3py 集成到我的应用程序中。有涉及小实数的断言，例如
solver.add(x <= 1e-6)
然后我收到以下错误：
File "~/src/solver/z3.py", line 2001, in __le__
a, b = _coerce_exprs(self, other)
File "~/src/solver/z3.py", line 846, in _coerce_exprs
b = s.cast(b)
File "~/src/solver/z3.py", line 1742, in cast
return RealVal(val, self.ctx)
File "~/src/solver/z3.py", line 2526, in RealVal
return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral
raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
src.solver.z3types.Z3Exception: 'parser error'
虽然断言
solver.add(x <= 1e-4)
似乎没问题。
因此，我猜测 z3 中存在某种精度限制。如果是这样，是否可以选择让第一个断言通过？
谢谢。
我试图证明 Z3（Microsoft 的 SMT 求解器）中的一个归纳事实。我知道 Z3 通常不提供此功能，如Z3 指南（第 8 节：数据类型）中所述，但是当我们限制要证明事实的域时，这似乎是可能的。考虑以下示例：
(declare-fun p (Int) Bool)
(assert (p 0))
(assert (forall ((x Int))
(=>
(and (> x 0) (<= x 20))
(= (p (- x 1)) (p x) ))))
(assert (not (p 20)))
(check-sat)
求解器正确响应unsat，这意味着这(p 20)是有效的。问题是，当我们进一步放松这个约束时（我们20在前面的例子中用大于 20 的任何整数替换），求解器响应unknown。
我觉得这很奇怪，因为 Z3 解决原来的问题并没有花很长时间，但是当我们将上限增加 1 时，它突然变得不可能。我试图向量词添加一个模式，如下所示：
(declare-fun p (Int) Bool)
(assert (p 0))
(assert (forall ((x Int))
(! (=>
(and (> x 0) (<= x …如何使用 Z3 的 Python API 执行量词消除？虽然我检查了教程和 API，但无法做到。
我有一个公式，它有一个存在量词，我希望 Z3 给我一个新公式，这样这个量词就被消除了。我基本上想做与此相同的事情：
但使用 Python 接口。我的公式也是线性算术。
谢谢！
添加：在进行量词消除后，我将用另一个“添加”无量词公式。因此，如果我使用 Tactic，是否可以将子目标（即策略的输出）转换为线性算术表达式？
我试图表达 z3 中一个无界数组的范围之和。例如在 Python 中：
IntArray = ArraySort(IntSort(), IntSort())
sum = Function('sum', IntArray, IntSort())
........
有没有办法完成' sum'的定义？否则，有没有更合理的选择？
谢谢！
假设我有一个BoolExpr的形式
a & (a | b) or a | (a & b)
我想简化它
a
通过调用simplify().它不起作用.
另外,对于像这样的约束
(a | b) & (b | a)
simplify()无法将其转换为最简单的形式
(a|b) or (b|a).
有解决方法吗？
@Nikolaj Bjorner:感谢您的帮助,我还有一个问题:
这是我原来的约束:
Goal: (goal
(or (> (type o) 2) (= (type o) 1))
(or (= (type o) 1) (> (type o) 2)))
这是简化版本(通过ctx-solver-simplified):
(or (= (type o) 1) (not (<= (type o) 2)))
我期待的实际约束是:
(or (= (type o) 1) (> (type o) 2))
而且我不想引入任何否定.我该怎么办？
我试图在 SMT-LIB 中表示时间约束，以检查它们的可满足性。我正在寻找有关我正在采取的方向的反馈。我对 SMT-LIB 比较陌生，我非常感谢输入。
我的限制是关于事件的时间和持续时间。例如，考虑以下自然语言中给出的约束：
约翰从 13:03:41 开始写一篇文章，他花了 20 分钟才完成。
写完之后，他检查了他的电子邮件，这花了他 40 多分钟。
查完邮件后，他给妻子打了电话。
14:00:00后他给妻子打了电话。
很容易看出这组约束是可稳定的，我正在尝试使用 SMT 求解器推断出这一点。
为了对时间和持续时间的概念进行一些封装，我定义了用数组表示它们的新类型。一些宏被定义为用作结构：
(define-sort Time () (Array Int Int))
(define-fun new_time_ns ((hours Int) (minutes Int) (seconds Int) (nanos Int)) Time
(store (store (store (store ((as const (Array Int Int)) 0) 1 hours) 2 minutes) 3 seconds) 4 nanos)
)
(define-sort Duration () (Array Int Int))
(define-fun new_duration_ns ((seconds Int) (nanos Int)) Duration
(store (store ((as const (Array Int Int)) 0) 1 seconds) 2 …我看到很多使用 SBV 库的示例，如下所示：
f :: IO SatResult
f = sat $ do
x <- sInteger "x"
constraint $ x .< 200
对于接受 Haskell Int 的函数，我想在通过 Data.SBV 库传递给 Z3 的约束公式中使用该 Int：
f :: Int -> IO SatResult
f i = sat $ do
x <- sInteger "x"
constraint $ x .< (g i)
where
g = ???
如何从 Haskell Int 转换为 SInteger 或 OrdSymbolic 和 EqSymbolic 的一些适当实例以与 (.<) 和 (.==) 一起使用？
谢谢！
Z3 4.8.1 中的新功能之一是并行求解：
并行模式可用于选定的理论，包括 QF_BV。通过设置 parallel.enable=true Z3 将产生与可用 CPU 内核数量成正比的工作线程数量，以在目标上应用立方体和征服解决方案。
它提到只parallel.enable=true需要设置，但我找不到parallel在代码中结构。
有人可以提供一些示例代码来了解如何实现这个新功能吗？
谢谢
我正在尝试解决数组表达式的模型，其中数组的默认值等于 0。
例如，我试图解决这个例子，但我一直得到未知的结果
(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)
(assert (forall ((x Int)) (= (select arr x) 0)))
(assert (> a 0))
(assert (<= a 10))
(assert (= arr2 (store arr a 1337)))
(assert (> b 0))
(assert (<= b 10))
(assert (= (select arr2 b) 0))
(check-sat)
(get-model)