0

我叫魏凡。我尝试使用 Z3py 来检查特定公式的可满足性，如下所示：

from z3 import *
import time 
import sys
import signal

UNIT_TIMEOUT = 300

# ==== time out exception class and handler ====
class Z3TimeoutException(Exception):
    def __int__ (self, value = "Z3 Timeout"):
        self.value = value
    def __str__ (self):
        return repr(self.value)

def Z3TimeoutHandler (signum, frame):
    raise Z3TimeoutException

# ==== a helper for killing Z3 when timing out ====
def TimedZ3Check(z3solver): 
    signal.alarm(UNIT_TIMEOUT)
    z3ret = z3solver.check()
    signal.alarm(0)
    return z3ret

signal.signal(signal.SIGALRM, Z3TimeoutHandler)

# ==== declaration of constants and free variables ====
LBOUND = Q("-89999998976", 1)
UBOUND = Q("89999998976", 1)
aff39 = Real('aff39')
rnvar = Real('rnvar')
models_8_12 = Real('models_8_12')
weights_0_4 = Real('weights_0_4')
weights_4_8 = Real('weights_4_8')
weightedAbscissas_8_12 = Real('weightedAbscissas_8_12')
weights_8_12 = Real('weights_8_12')
models_4_8 = Real('models_4_8')
models_0_4 = Real('models_0_4')
weightedAbscissas_4_8 = Real('weightedAbscissas_4_8')
weightedAbscissas_0_4 = Real('weightedAbscissas_0_4')
aff25 = Real('aff25')
aff0 = Real('aff0')
aff30 = Real('aff30')
aff14 = Real('aff14')
aff19 = Real('aff19')
aff1 = Real('aff1')
aff8 = Real('aff8')
aff29 = Real('aff29')
aff18 = Real('aff18')
aff7 = Real('aff7')
aff38 = Real('aff38')
aff15 = Real('aff15')
aff16 = Real('aff16')
aff2 = Real('aff2')
aff3 = Real('aff3')
aff26 = Real('aff26')
aff27 = Real('aff27')
aff4 = Real('aff4')
aff12 = Real('aff12')
aff6 = Real('aff6')
aff13 = Real('aff13')
aff37 = Real('aff37')
aff17 = Real('aff17')
aff22 = Real('aff22')
aff23 = Real('aff23')
aff20 = Real('aff20')
aff21 = Real('aff21')
aff24 = Real('aff24')
aff36 = Real('aff36')
aff28 = Real('aff28')
aff33 = Real('aff33')
aff34 = Real('aff34')
aff31 = Real('aff31')
aff32 = Real('aff32')
aff35 = Real('aff35')
aff11 = Real('aff11')
aff5 = Real('aff5')
aff10 = Real('aff10')
aff9 = Real('aff9')
const0 = Real('const0')
const1 = Real('const1')
const2 = Real('const2')
objvar = Real('objvar')

# ==== creation of the solver ====
usolver = Tactic('qfnra').solver()

# ==== add constraints ==== 
usolver.add(rnvar == aff39)
usolver.add(Q("-16777217", "16777216") <= models_8_12)
usolver.add(models_8_12 <= Q("16777217", "16777216"))
usolver.add(Q("21990231", "2199023255552") <= weights_0_4)
usolver.add(weights_0_4 <= Q("16777217", "16777216"))
usolver.add(Q("21990231", "2199023255552") <= weights_4_8)
usolver.add(weights_4_8 <= Q("16777217", "16777216"))
usolver.add(Q("21990231", "2199023255552") <= weightedAbscissas_8_12)
usolver.add(weightedAbscissas_8_12 <= Q("16777217", "16777216"))
usolver.add(Q("21990231", "2199023255552") <= weights_8_12)
usolver.add(weights_8_12 <= Q("16777217", "16777216"))
usolver.add(Q("-16777217", "16777216") <= models_4_8)
usolver.add(models_4_8 <= Q("16777217", "16777216"))
usolver.add(Q("-16777217", "16777216") <= models_0_4)
usolver.add(models_0_4 <= Q("16777217", "16777216"))
usolver.add(Q("21990231", "2199023255552") <= weightedAbscissas_4_8)
usolver.add(weightedAbscissas_4_8 <= Q("16777217", "16777216"))
usolver.add(Q("21990231", "2199023255552") <= weightedAbscissas_0_4)
usolver.add(weightedAbscissas_0_4 <= Q("16777217", "16777216"))
usolver.add(aff25 != aff0)
usolver.add(aff30 != aff0)
usolver.add(aff14 != aff0)
usolver.add(aff19 != aff0)
usolver.add(aff1 != aff0)
usolver.add(aff8 != aff0)
usolver.add(aff29 != aff0)
usolver.add(aff18 != aff0)
usolver.add(aff7 != aff0)
usolver.add(Or(((aff0 + aff38)-(aff0 + aff38)*1/16777216) >= aff39, ((aff0 + aff38)+    (aff0 + aff38)*1/16777216) >= aff39))
usolver.add(Or(((aff0 + aff38)-(aff0 + aff38)*1/16777216) <= aff39, ((aff0 + aff38)+    (aff0 + aff38)*1/16777216) <= aff39))
usolver.add(Or(((aff0 - aff15)-(aff0 - aff15)*1/16777216) >= aff16, ((aff0 - aff15)+(aff0 - aff15)*1/16777216) >= aff16))
usolver.add(Or(((aff0 - aff15)-(aff0 - aff15)*1/16777216) <= aff16, ((aff0 - aff15)+(aff0 - aff15)*1/16777216) <= aff16))
usolver.add(Or(((aff0 - aff2)-(aff0 - aff2)*1/16777216) >= aff3, ((aff0 - aff2)+(aff0 - aff2)*1/16777216) >= aff3))
usolver.add(Or(((aff0 - aff2)-(aff0 - aff2)*1/16777216) <= aff3, ((aff0 - aff2)+(aff0 - aff2)*1/16777216) <= aff3))
usolver.add(Or(((aff0 - aff26)-(aff0 - aff26)*1/16777216) >= aff27, ((aff0 - aff26)+(aff0 - aff26)*1/16777216) >= aff27))
usolver.add(Or(((aff0 - aff26)-(aff0 - aff26)*1/16777216) <= aff27, ((aff0 - aff26)+(aff0 - aff26)*1/16777216) <= aff27))
usolver.add(Or(((aff1 * aff3)-(aff1 * aff3)*1/16777216) >= aff4, ((aff1 * aff3)+(aff1 * aff3)*1/16777216) >= aff4))
usolver.add(Or(((aff1 * aff3)-(aff1 * aff3)*1/16777216) <= aff4, ((aff1 * aff3)+(aff1 * aff3)*1/16777216) <= aff4))
usolver.add(Or(((aff12 * aff6)-(aff12 * aff6)*1/16777216) >= aff13, ((aff12 * aff6)+(aff12 * aff6)*1/16777216) >= aff13))
usolver.add(Or(((aff12 * aff6)-(aff12 * aff6)*1/16777216) <= aff13, ((aff12 * aff6)+(aff12 * aff6)*1/16777216) <= aff13))
usolver.add(Or(((aff13 + aff37)-(aff13 + aff37)*1/16777216) >= aff38, ((aff13 + aff37)+(aff13 + aff37)*1/16777216) >= aff38))
usolver.add(Or(((aff13 + aff37)-(aff13 + aff37)*1/16777216) <= aff38, ((aff13 + aff37)+(aff13 + aff37)*1/16777216) <= aff38))
usolver.add(Or(((aff14 * aff16)-(aff14 * aff16)*1/16777216) >= aff17, ((aff14 * aff16)+(aff14 * aff16)*1/16777216) >= aff17))
usolver.add(Or(((aff14 * aff16)-(aff14 * aff16)*1/16777216) <= aff17, ((aff14 * aff16)+(aff14 * aff16)*1/16777216) <= aff17))
usolver.add(Or(((aff17 * aff22)-(aff17 * aff22)*1/16777216) >= aff23, ((aff17 * aff22)+(aff17 * aff22)*1/16777216) >= aff23))
usolver.add(Or(((aff17 * aff22)-(aff17 * aff22)*1/16777216) <= aff23, ((aff17 * aff22)+(aff17 * aff22)*1/16777216) <= aff23))
usolver.add(Or(((aff18 / aff14)-(aff18 / aff14)*1/16777216) >= aff19, ((aff18 / aff14)+(aff18 / aff14)*1/16777216) >= aff19))
usolver.add(Or(((aff18 / aff14)-(aff18 / aff14)*1/16777216) <= aff19, ((aff18 / aff14)+(aff18 / aff14)*1/16777216) <= aff19))
usolver.add(Or(((aff20 * aff19)-(aff20 * aff19)*1/16777216) >= aff21, ((aff20 * aff19)+(aff20 * aff19)*1/16777216) >= aff21))
usolver.add(Or(((aff20 * aff19)-(aff20 * aff19)*1/16777216) <= aff21, ((aff20 * aff19)+(aff20 * aff19)*1/16777216) <= aff21))
usolver.add(Or(((aff23 * aff6)-(aff23 * aff6)*1/16777216) >= aff24, ((aff23 * aff6)+(aff23 * aff6)*1/16777216) >= aff24))
usolver.add(Or(((aff23 * aff6)-(aff23 * aff6)*1/16777216) <= aff24, ((aff23 * aff6)+(aff23 * aff6)*1/16777216) <= aff24))
usolver.add(Or(((aff24 + aff36)-(aff24 + aff36)*1/16777216) >= aff37, ((aff24 + aff36)+(aff24 + aff36)*1/16777216) >= aff37))
usolver.add(Or(((aff24 + aff36)-(aff24 + aff36)*1/16777216) <= aff37, ((aff24 + aff36)+(aff24 + aff36)*1/16777216) <= aff37))
usolver.add(Or(((aff25 * aff27)-(aff25 * aff27)*1/16777216) >= aff28, ((aff25 * aff27)+(aff25 * aff27)*1/16777216) >= aff28))
usolver.add(Or(((aff25 * aff27)-(aff25 * aff27)*1/16777216) <= aff28, ((aff25 * aff27)+(aff25 * aff27)*1/16777216) <= aff28))
usolver.add(Or(((aff28 * aff33)-(aff28 * aff33)*1/16777216) >= aff34, ((aff28 * aff33)+(aff28 * aff33)*1/16777216) >= aff34))
usolver.add(Or(((aff28 * aff33)-(aff28 * aff33)*1/16777216) <= aff34, ((aff28 * aff33)+(aff28 * aff33)*1/16777216) <= aff34))
usolver.add(Or(((aff29 / aff25)-(aff29 / aff25)*1/16777216) >= aff30, ((aff29 / aff25)+(aff29 / aff25)*1/16777216) >= aff30))
usolver.add(Or(((aff29 / aff25)-(aff29 / aff25)*1/16777216) <= aff30, ((aff29 / aff25)+(aff29 / aff25)*1/16777216) <= aff30))
usolver.add(Or(((aff31 * aff30)-(aff31 * aff30)*1/16777216) >= aff32, ((aff31 * aff30)+(aff31 * aff30)*1/16777216) >= aff32))
usolver.add(Or(((aff31 * aff30)-(aff31 * aff30)*1/16777216) <= aff32, ((aff31 * aff30)+(aff31 * aff30)*1/16777216) <= aff32))
usolver.add(Or(((aff34 * aff6)-(aff34 * aff6)*1/16777216) >= aff35, ((aff34 * aff6)+(aff34 * aff6)*1/16777216) >= aff35))
usolver.add(Or(((aff34 * aff6)-(aff34 * aff6)*1/16777216) <= aff35, ((aff34 * aff6)+(aff34 * aff6)*1/16777216) <= aff35))
usolver.add(Or(((aff35 + aff0)-(aff35 + aff0)*1/16777216) >= aff36, ((aff35 + aff0)+(aff35 + aff0)*1/16777216) >= aff36))
usolver.add(Or(((aff35 + aff0)-(aff35 + aff0)*1/16777216) <= aff36, ((aff35 + aff0)+(aff35 + aff0)*1/16777216) <= aff36))
usolver.add(Or(((aff4 * aff11)-(aff4 * aff11)*1/16777216) >= aff12, ((aff4 * aff11)+(aff4 * aff11)*1/16777216) >= aff12))
usolver.add(Or(((aff4 * aff11)-(aff4 * aff11)*1/16777216) <= aff12, ((aff4 * aff11)+(aff4 * aff11)*1/16777216) <= aff12))
usolver.add(Or(((aff5 * aff10)-(aff5 * aff10)*1/16777216) >= aff11, ((aff5 * aff10)+(aff5 * aff10)*1/16777216) >= aff11))
usolver.add(Or(((aff5 * aff10)-(aff5 * aff10)*1/16777216) <= aff11, ((aff5 * aff10)+(aff5 * aff10)*1/16777216) <= aff11))
usolver.add(Or(((aff5 * aff21)-(aff5 * aff21)*1/16777216) >= aff22, ((aff5 * aff21)+(aff5 * aff21)*1/16777216) >= aff22))
usolver.add(Or(((aff5 * aff21)-(aff5 * aff21)*1/16777216) <= aff22, ((aff5 * aff21)+(aff5 * aff21)*1/16777216) <= aff22))
usolver.add(Or(((aff5 * aff32)-(aff5 * aff32)*1/16777216) >= aff33, ((aff5 * aff32)+(aff5 * aff32)*1/16777216) >= aff33))
usolver.add(Or(((aff5 * aff32)-(aff5 * aff32)*1/16777216) <= aff33, ((aff5 * aff32)+(aff5 * aff32)*1/16777216) <= aff33))
usolver.add(Or(((aff6 * aff19)-(aff6 * aff19)*1/16777216) >= aff20, ((aff6 * aff19)+(aff6 * aff19)*1/16777216) >= aff20))
usolver.add(Or(((aff6 * aff19)-(aff6 * aff19)*1/16777216) <= aff20, ((aff6 * aff19)+(aff6 * aff19)*1/16777216) <= aff20))
usolver.add(Or(((aff6 * aff30)-(aff6 * aff30)*1/16777216) >= aff31, ((aff6 * aff30)+(aff6 * aff30)*1/16777216) >= aff31))
usolver.add(Or(((aff6 * aff30)-(aff6 * aff30)*1/16777216) <= aff31, ((aff6 * aff30)+(aff6 * aff30)*1/16777216) <= aff31))
usolver.add(Or(((aff6 * aff8)-(aff6 * aff8)*1/16777216) >= aff9, ((aff6 * aff8)+(aff6 * aff8)*1/16777216) >= aff9))
usolver.add(Or(((aff6 * aff8)-(aff6 * aff8)*1/16777216) <= aff9, ((aff6 * aff8)+(aff6 * aff8)*1/16777216) <= aff9))
usolver.add(Or(((aff7 / aff1)-(aff7 / aff1)*1/16777216) >= aff8, ((aff7 / aff1)+(aff7 / aff1)*1/16777216) >= aff8))
usolver.add(Or(((aff7 / aff1)-(aff7 / aff1)*1/16777216) <= aff8, ((aff7 / aff1)+(aff7 / aff1)*1/16777216) <= aff8))
usolver.add(Or(((aff9 * aff8)-(aff9 * aff8)*1/16777216) >= aff10, ((aff9 * aff8)+(aff9 * aff8)*1/16777216) >= aff10))
usolver.add(Or(((aff9 * aff8)-(aff9 * aff8)*1/16777216) <= aff10, ((aff9 * aff8)+(aff9 * aff8)*1/16777216) <= aff10))
usolver.add(Or(((const0)-(const0)*1/16777216) >= aff0, ((const0)+(const0)*1/16777216) >= aff0))
usolver.add(Or(((const0)-(const0)*1/16777216) <= aff0, ((const0)+(const0)*1/16777216) <= aff0))
usolver.add(Or(((const1)-(const1)*1/16777216) >= aff5, ((const1)+(const1)*1/16777216) >= aff5))
usolver.add(Or(((const1)-(const1)*1/16777216) <= aff5, ((const1)+(const1)*1/16777216) <= aff5))
usolver.add(Or(((const2)-(const2)*1/16777216) >= aff6, ((const2)+(const2)*1/16777216) >= aff6))
usolver.add(Or(((const2)-(const2)*1/16777216) <= aff6, ((const2)+(const2)*1/16777216) <= aff6))
usolver.add(Or(((models_0_4)-(models_0_4)*1/16777216) >= aff26, ((models_0_4)+(models_0_4)*1/16777216) >= aff26))
usolver.add(Or(((models_0_4)-(models_0_4)*1/16777216) <= aff26, ((models_0_4)+(models_0_4)*1/16777216) <= aff26))
usolver.add(Or(((models_4_8)-(models_4_8)*1/16777216) >= aff15, ((models_4_8)+(models_4_8)*1/16777216) >= aff15))
usolver.add(Or(((models_4_8)-(models_4_8)*1/16777216) <= aff15, ((models_4_8)+(models_4_8)*1/16777216) <= aff15))
usolver.add(Or(((models_8_12)-(models_8_12)*1/16777216) >= aff2, ((models_8_12)+(models_8_12)*1/16777216) >= aff2))
usolver.add(Or(((models_8_12)-(models_8_12)*1/16777216) <= aff2, ((models_8_12)+(models_8_12)*1/16777216) <= aff2))
usolver.add(Or(((weightedAbscissas_0_4)-(weightedAbscissas_0_4)*1/16777216) >= aff29, ((weightedAbscissas_0_4)+(weightedAbscissas_0_4)*1/16777216) >= aff29))
usolver.add(Or(((weightedAbscissas_0_4)-(weightedAbscissas_0_4)*1/16777216) <= aff29, ((weightedAbscissas_0_4)+(weightedAbscissas_0_4)*1/16777216) <= aff29))
usolver.add(Or(((weightedAbscissas_4_8)-(weightedAbscissas_4_8)*1/16777216) >= aff18, ((weightedAbscissas_4_8)+(weightedAbscissas_4_8)*1/16777216) >= aff18))
usolver.add(Or(((weightedAbscissas_4_8)-(weightedAbscissas_4_8)*1/16777216) <= aff18, ((weightedAbscissas_4_8)+(weightedAbscissas_4_8)*1/16777216) <= aff18))
usolver.add(Or(((weightedAbscissas_8_12)-(weightedAbscissas_8_12)*1/16777216) >= aff7, ((weightedAbscissas_8_12)+(weightedAbscissas_8_12)*1/16777216) >= aff7))
usolver.add(Or(((weightedAbscissas_8_12)-(weightedAbscissas_8_12)*1/16777216) <= aff7, ((weightedAbscissas_8_12)+(weightedAbscissas_8_12)*1/16777216) <= aff7))
usolver.add(Or(((weights_0_4)-(weights_0_4)*1/16777216) >= aff25, ((weights_0_4)+(weights_0_4)*1/16777216) >= aff25))
usolver.add(Or(((weights_0_4)-(weights_0_4)*1/16777216) <= aff25, ((weights_0_4)+(weights_0_4)*1/16777216) <= aff25))
usolver.add(Or(((weights_4_8)-(weights_4_8)*1/16777216) >= aff14, ((weights_4_8)+(weights_4_8)*1/16777216) >= aff14))
usolver.add(Or(((weights_4_8)-(weights_4_8)*1/16777216) <= aff14, ((weights_4_8)+(weights_4_8)*1/16777216) <= aff14))
usolver.add(Or(((weights_8_12)-(weights_8_12)*1/16777216) >= aff1, ((weights_8_12)+(weights_8_12)*1/16777216) >= aff1))
usolver.add(Or(((weights_8_12)-(weights_8_12)*1/16777216) <= aff1, ((weights_8_12)+(weights_8_12)*1/16777216) <= aff1))
usolver.add(And(Q("-25165825", "8388608") <= const1, const1 <= Q("-25165823", "8388608")))
usolver.add(And(0 <= const0, const0 <= 0))
usolver.add(And(Q("16777215", "16777216") <= const2, const2 <= Q("16777217", "16777216")))
usolver.add(objvar == (rnvar))

# ==== add additional constraints ====
upper = simplify(UBOUND - (UBOUND - LBOUND) * Q(1, 64))
usolver.add(objvar > upper)

# ==== start Z3py to check the satisfiability ==== 
TimedZ3Check(usolver)

我使用 z3py 4.1 来检查可满足性。花了很长时间（3 个多小时）但没有返回结果（SAT 或 UNSAT） 我的主要问题是：

  • 是否有任何 Z3py 的技巧或标志可以用来加速这种可满足性检查？
  • 函数（TimedZ3Check）没有在我指定的时间限制（300 秒）内终止 Z3py。是否有为 Z3py 设置超时的“标准”方式？

非常感谢任何建议。

问候， 韦凡

4

1 回答 1

0

您的问题似乎超出了 Z3 中使用的当前非线性实数算术求解器 (nlsat) 的能力。我们计划在未来为这个片段提供更好的求解器。关于超时，您可以在创建后使用以下命令设置超时usolver。

  usolver.set('timeout', 1000)

超时以毫秒为单位。顺便说一句，计时器可能在 4.1 版本上不起作用，我们修复了某些平台（例如 OSX）中计时器的一些问题。如果 Z3 不起作用，请将其更新到最新版本。

于 2013-05-06T05:59:57.760 回答