量词中的非零向量 [英] Nonzero vector in quantifier

问题描述

我想验证以下形式的公式:

I want to verify a formula of the form:

Exists p . ForAll x != 0 . f(x, p) > 0

一个实现(不起作用)如下:

An implementation (that isn't working) is the following:

def f0(x0, x1, x, y):
    return x1 ** 2 * y + x0 ** 2 * x

s = Solver()
x0, x1 = Reals('x0 x1')
p0, p1 = Reals('p0 p1')

s.add(Exists([p0, p1], 
                ForAll([x0, x1], 
                          f0(x0, x1, p0, p1) > 0
                      )
            ))
#s.add(Or(x0 != 0, x1 != 0))

while s.check() == sat:
    m = s.model()
    m.evaluate(x0, model_completion=True)
    m.evaluate(x1, model_completion=True)
    m.evaluate(p0, model_completion=True)
    m.evaluate(p1, model_completion=True)
    print m
    s.add(Or(x0 != m[x0], x1 != m[x1])) 

公式不满足.

当 f0() >= 0 时，唯一的输出是 (0, 0).

With f0() >= 0, the only output is (0, 0).

我想要 f0() >0 并约束 (x0, x1) != (0, 0).

我期望的是:p0, p1 = 1, 1 或 2, 2 例如，但我不知道如何删除 0, 0 来自 x0, x1 的可能值.

Something I'd expect is: p0, p1 = 1, 1 or 2, 2 for instance, but I don't know how to remove 0, 0 from the possible values for x0, x1.

推荐答案

跟进 Levent 的回复.在第一次检查期间，Z3 使用与量词配合使用的自定义决策程序.在增量模式下，它回退到不是决策过程的东西.要强制使用一次性求解器，请尝试以下操作:

Following up on Levent's reply. During the first check, Z3 uses a custom decision procedure that works with the quantifiers. In incremental mode it falls back to something that isn't a decision procedure. To force the one-shot solver try the following:

from z3 import *

def f0(x0, x1, x, y):
    return x1 * x1 * y + x0 * x0 * x

p0, p1 = Reals('p0 p1')

x0, x1 = Reals('x0 x1')
fmls = [ForAll([x0, x1], Implies(Or(x0 != 0, x1 != 0), f0(x0, x1, p0, p1) > 0))]

while True:
    s = Solver()
    s.add(fmls)
    res = s.check()
    print res
    if res == sat:
        m = s.model()
        print m
        fmls += [Or(p0 != m[p0], p1 != m[p1])]
    else:
       print "giving up"
       break

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