0
我叫偉凡。 我試圖用Z3py檢查哪個被示出如下的特定式的滿足性：加速使用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）沒有終止Z3py在我指定的時間限制（300秒）。有沒有爲Z3py設置超時的「標準」方式？
任何建議，非常感謝。
問候， 偉凡