PyExZ3 未找到程序的所有可行路径

问题描述 投票：0回答：1

我提出的 PyExZ3 用法的一个小例子没有按预期工作。 这是例子：

def d1(x,y):
  if y < x - 2 :
    return 7
  else :
    return 2

def d2(x,y):
  if y > 3 :
    return 10
  else:
    return 50

def d3(x,y):
  if y < -x + 3 :
    return 100
  else :
    return 200

def yolo(a,b):
  return d1(a,b)+d2(a,b)+d3(a,b)

def expected_result():
  return [ 112, 157, 152, 217, 212, 257, 252]

以上内容保存在

FILE.py
中并使用
.\pyexz3.py FILE.py --start yolo
进行测试（在Windows上）。 我原以为有 7 条路径，但只找到了 6 条唯一的路径。其中 1 个（共 251 个）被列出两次。

我的期望是错误的还是 pyexz3 返回了错误的结果？

python z3 z3py pyexz3
1个回答
0
投票

貌似 PyExZ3 不再维护了；所以不可能说这是 PyExZ3 中的一个错误，还是 z3 随着时间的推移而发展的一些不兼容性。如果你想调查这一点，你必须使用他们声称支持的 z3 版本来运行它； 2015 年左右发布的 z3。但是，我不确定这会带来什么好处，因为我怀疑 PyExZ3 会很快被“修复”或修改。

但是，如果您愿意使用常规 z3 编程，则只需使用常规 z3 功能即可轻松解决此问题。当然，这需要您“重写”Python 代码以支持 z3；一般来说，这项任务可能令人畏惧，具体取决于您想要使用哪种类型的 Python 程序。然而，您给出的示例以这种风格重写是微不足道的：

from z3 import *

def d1(x, y): return If(y < x - 2 ,   7,   2)
def d2(x, y): return If(y > 3     ,  10,  50)
def d3(x, y): return If(y < -x + 3, 100, 200)

def yolo(a, b): return d1(a, b) + d2(a, b) + d3(a ,b)

一旦有了这个，您就可以根据 

a
和 
b
的符号输入为结果值创建约束：

s = Solver()
a, b, r = Ints('a b r')
s.add(r == yolo(a, b))

有了这个设置，我们还需要一种成分。 

https://theory.stanford.edu/~nikolaj/programmingz3.html
第 5.1 节中的 all_smt 函数。 （第 5.2 节开始之前的那个。）一旦包含了它，就可以通过简单的迭代轻松获得 
r
的所有可能（和不同）值：

for i, m in enumerate(all_smt(s, [r])):
    print(f"{i+1}. a = {m[a].as_long():>2d}, b = {m[b].as_long():>2d}, r = {m[r]}")

打印：

1. a =  0, b =  0, r = 152
2. a =  7, b =  4, r = 217
3. a =  3, b = -1, r = 157
4. a =  4, b =  0, r = 257
5. a =  0, b =  4, r = 212
6. a =  1, b =  3, r = 252
7. a = -2, b =  4, r = 112

我相信这就是您一直在寻找的结果。

为了完整起见，这是整个脚本，包括上面提到的 

all_smt
函数：

from z3 import *

def d1(x, y): return If(y < x - 2 ,   7,   2)
def d2(x, y): return If(y > 3     ,  10,  50)
def d3(x, y): return If(y < -x + 3, 100, 200)

def yolo(a, b): return d1(a, b) + d2(a, b) + d3(a ,b)

s = Solver()
a, b, r = Ints('a b r')
s.add(r == yolo(a, b))

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()
    yield from all_smt_rec(list(initial_terms))

for i, m in enumerate(all_smt(s, [r])):
    print(f"{i+1}. a = {m[a].as_long():>2d}, b = {m[b].as_long():>2d}, r = {m[r]}")

在哈斯克尔

虽然 Python 是编写 z3 脚本的不错选择，但它并不总是执行程序分析等任务的最佳选择。对于这类问题，像 Haskell 这样的函数式语言提供了一个更好的平台。特别是 Haskell 的 SBV 包配备了“包含电池”的方法来解决此类问题，利用 Haskell 生态系统的出色功能进行程序分析。因此，如果这适合您的环境，我建议您使用 Haskell 来解决此类问题。 作为示例，以下是我们如何使用 SBV 库在 Haskell 中解决同样的问题：

import Data.SBV d1, d2, d3, yolo :: (SInteger, SInteger) -> SInteger d1 (x, y) = ite (y .< x - 2 ) 7 2 d2 (x, y) = ite (y .> 3 ) 10 50 d3 (x, y) = ite (y .< -x + 3) 100 200 yolo (a, b) = d1 (a, b) + d2 (a, b) + d3 (a, b) paths :: IO AllSatResult paths = allSat $ do a <- sInteger "a" b <- sInteger "b" partition "r" $ yolo (a, b) 

在这种情况下，Python 和 Haskell 版本的代码复杂性相当，但对于较大的程序，我认为您会发现 Haskell 的性能更好。这打印：

Solution #1: a = -2 :: Integer b = 4 :: Integer r = 112 :: Integer Solution #2: a = 0 :: Integer b = 3 :: Integer r = 252 :: Integer Solution #3: a = -1 :: Integer b = 4 :: Integer r = 212 :: Integer Solution #4: a = 3 :: Integer b = 0 :: Integer r = 257 :: Integer Solution #5: a = 2 :: Integer b = -1 :: Integer r = 157 :: Integer Solution #6: a = 7 :: Integer b = 4 :: Integer r = 217 :: Integer Solution #7: a = 0 :: Integer b = 0 :: Integer r = 152 :: Integer Found 7 different solutions. 


      

      
    

  

  

    
最新问题


  





  

    © www.soinside.com 2019 - 2024. All rights reserved.