z3py：如何提高以下代码的时间效率

Question

这是一个简化的代码，使用与 z3py 代码类似的实现思想，用于解决我试图解决的另一个问题，该问题更复杂，运行大约需要 1 分钟。

下面代码的直觉是将inputArray中的整数数组翻译成定义为EnumSort的月份数组，本质上是推断monthArray的模型。

from z3 import *
s = Solver()

Month,(Jan,Feb,Mar,Apr,May,Jun,Jul,Aug,Sep,Oct,Nov,Dec)=EnumSort('Month',['Jan','Feb','Mar','Apr','May','Jun','Jul','Aug','Sep','Oct','Nov','Dec'])
monthArray = Array('monthArray',IntSort(), Month)
inputArray = Array('inputArray',IntSort(),IntSort())
tempArray = Array('tempArray',IntSort(),IntSort())

intArray = [1,3,6,7,8,3,5,6,3,12,11,5,2,5,7,3,7,3,2,7,12,4,5,1,10,9]
for idx,num in enumerate(intArray):
    tempArray = Store(tempArray,idx,num)

s.add(inputArray==tempArray)

length = Int('length')
s.add(length == len(intArray))
i = Int('i')
s.add(ForAll(i,Implies(And(i>=0,i<length),And(
    Implies(inputArray[i]==1,monthArray[i]==Jan),
    Implies(inputArray[i]==2,monthArray[i]==Feb),
    Implies(inputArray[i]==3,monthArray[i]==Mar),
    Implies(inputArray[i]==4,monthArray[i]==Apr),
    Implies(inputArray[i]==5,monthArray[i]==May),
    Implies(inputArray[i]==6,monthArray[i]==Jun),
    Implies(inputArray[i]==7,monthArray[i]==Jul),
    Implies(inputArray[i]==8,monthArray[i]==Aug),
    Implies(inputArray[i]==9,monthArray[i]==Sep),
    Implies(inputArray[i]==10,monthArray[i]==Oct),
    Implies(inputArray[i]==11,monthArray[i]==Nov),
    Implies(inputArray[i]==12,monthArray[i]==Dec)
    ))))

print s.check()
print s.model()

谁能给我一些关于使用此代码作为示例提高时间效率的方法的建议？谢谢。

编辑： 通过调用 Solver.to_smt2() 输出 SMT 语言

(set-info :status unknown)
(declare-datatypes () ((Month (Jan ) (Feb ) (Mar ) (Apr ) (May ) (Jun ) (Jul ) (Aug ) (Sep ) (Oct ) (Nov ) (Dec ))))
(declare-fun inputArray () (Array Int Int))
(declare-fun length () Int)
(declare-fun monthArray () (Array Int Month))
(assert
(= (select inputArray 0) 1))
(assert
(= (select inputArray 1) 3))
(assert
(= (select inputArray 2) 6))
(assert
(= (select inputArray 3) 7))
(assert
(= (select inputArray 4) 8))
(assert
(= (select inputArray 5) 3))
(assert
(= (select inputArray 6) 5))
(assert
(= (select inputArray 7) 6))
(assert
(= (select inputArray 8) 3))
(assert
(= (select inputArray 9) 12))
(assert
(= (select inputArray 10) 11))
(assert
(= (select inputArray 11) 5))
(assert
(= (select inputArray 12) 2))
(assert
(= (select inputArray 13) 5))
(assert
(= (select inputArray 14) 7))
(assert
(= (select inputArray 15) 3))
(assert
(= (select inputArray 16) 7))
(assert
(= (select inputArray 17) 3))
(assert
(= (select inputArray 18) 2))
(assert
(= (select inputArray 19) 7))
(assert
(= (select inputArray 20) 12))
(assert
(= (select inputArray 21) 4))
(assert
(= (select inputArray 22) 5))
(assert
(= (select inputArray 23) 1))
(assert
(= (select inputArray 24) 10))
(assert
(= (select inputArray 25) 9))
(assert
(= length 26))
(assert
(forall ((i Int) )(let (($x172 (=> (= (select inputArray i) 12) (= (select monthArray i) Dec))))
(let (($x175 (=> (= (select inputArray i) 11) (= (select monthArray i) Nov))))
(let (($x178 (=> (= (select inputArray i) 10) (= (select monthArray i) Oct))))
(let (($x181 (=> (= (select inputArray i) 9) (= (select monthArray i) Sep))))
(let (($x184 (=> (= (select inputArray i) 8) (= (select monthArray i) Aug))))
(let (($x187 (=> (= (select inputArray i) 7) (= (select monthArray i) Jul))))
(let (($x190 (=> (= (select inputArray i) 6) (= (select monthArray i) Jun))))
(let (($x193 (=> (= (select inputArray i) 5) (= (select monthArray i) May))))
(let (($x196 (=> (= (select inputArray i) 4) (= (select monthArray i) Apr))))
(let (($x199 (=> (= (select inputArray i) 3) (= (select monthArray i) Mar))))
(let (($x202 (=> (= (select inputArray i) 2) (= (select monthArray i) Feb))))
(let (($x205 (=> (= (select inputArray i) 1) (= (select monthArray i) Jan))))
(=> (and (>= i 0) (< i length)) (and $x205 $x202 $x199 $x196 $x193 $x190 $x187 $x184 $x181 $x178 $x175 $x172)))))))))))))))
)
(check-sat)

Answer 1

我发现使用“qflia”（无量词线性整数算术）求解器，而不是通用求解器“Solver()”，在我的例子中效率提高了大约 3 倍。