我正在编写一个程序，从TMX网站上抓取option_chain数据，并根据这些数据提出优化的Covered Call期权组合。对于优化过程，我使用了z3py库，正如许多用户在本网站上讨论的那样。优化过程通过最大化保费并将投资组合delta设置为用户指定的金额来工作。
起初，我在计算投资组合delta时犯了一个错误，这使得一切都很顺利，但在更正后我遇到了问题。投资组合del塔是通过计算投资组合中非零头寸的加权平均delta来计算的。为了实现这一点，我使用了以下设置：
eng = Optimize()
Weights = [Real(row.symbol) for row in df.itertuples()]
#to count non-zero positions
TotCount = Real("TotCount")
eng.add(TotCount == Sum([If(w > 0, 1, 0) for w in Weights]))
eng.add(TotCount == If(TotCount >= 0, TotCount, 1))
#to get portfolio delta
eng.add(TotDelta == (Sum([(w * row.delta) for w, row in zip(Weights, df.itertuples())]) / TotCount))
eng.add(TotDelta == delta)
res = eng.check()
当我在一个具有不同delta值的循环中运行这个函数时，会发生奇怪的行为，第一个循环实际上进行了计算并给出了答案，但在那之后，我的代码在最后一行停留了几个小时，没有任何进展。我尝试了一些方法，比如完全重新格式化它，但似乎没有什么不同。我想知道有没有人知道这里发生了什么？
不幸的是，在您的描述中没有太多内容可供任何人在不了解您的设置详细信息的情况下继续操作。从你的文本中可以推断出，对于那些需要更长时间的delta值，约束很难求解。如果看不到程序的其余部分，就不可能对其他可能发生的事情发表意见。
看看你是否可以隔离它运行缓慢的delta的值，然后单独为那个实例运行它，看看是否有来自其他地方的交互。当然，这绝不是一个解决方案，但这是开始的一种方式。
不过，我注意到的一件事是，你有这样一行：
eng.add(TotCount == If(TotCount >= 0, TotCount, 1))
让我们看看这行是怎么说的：如果是TotCount >= 0，那么它就是TotCount == TotCount。即，它不限制它。否则，它说TotCount == 1；即，如果为TotCount < 0，则为TotCount == 1。后一种说法显然是错误的。也就是说，如果其他约束强制TotCount < 0，那么您的程序将是unsat。这本质上意味着整条线路在功能上等同于：
eng.add(TotCount >= 0)
任何人都很难判断这是否是你的意图；但我怀疑也许不是；因为你刚刚写了上面更简单的表格。也许你想说更多类似于TotCount < 0的话，那么就把它变成1。但看看前一行(即Sum表达式(，我们会发现情况永远不会如此。所以，那里有点可疑。
希望这能帮助你开始；请注意，不能模型"；顺序分配"；就像在编程语言中一样。(你需要做所谓的单一静态分配，也就是SSA，转换。(但话说回来，在不知道你的确切意图的情况下，很难发表意见。