Python中文
首页
教程
问答
标签
搜索
登录
注册
Z3Py prove函数返回错误的counterexamp
回答此问题可获得
20
贡献值,回答如果被采纳可获得
50
分。
<p>我试图使用Z3Py证明函数,但它似乎返回了一个不正确的反例。 有什么问题??(Z3-4.7.1-x86-win、Python-2.7.15)</p> <pre><code>>>> import z3 >>> A = z3.BitVec('A', 8) >>> B = z3.BitVec('B', 8) >>> C = z3.BitVec('C', 8) >>> z3.prove((A*B)/C == A*(B/C)) counterexample [A = 67, B = 86, C = 2] >>> ((67*86)%256)/2 65 >>> (67*(86/2))%256 65 </code></pre>
0 条评论
分类:
Python问答
请先
登录
后评论
默认排序
时间排序
1 个回答
匿名
1天前
擅长:python、mysql、java
<p>我认为您看到了算术“模8”(8位宽度)的一个问题:a*B(两个8位值)不能表示为8位值,导致一些环绕/剪裁。你知道吗</p> <p>这类等式一般不适用于固定宽度的数学。你知道吗</p>
请先
登录
后评论
针对此问题:
更多的回答
关注
89
关注
收藏
1
收藏,
216
浏览
网友 提问于 2天前
相关Python问题
尽管Python中的所有内容都是引用,为什么Python导师在没有指针的列表中绘制字符串和整数?
9 回答
尽管python中的表达式为false,但循环仍在运行
8 回答
尽管python代码正确,但从nifi ExecuteScript处理器获取语法错误
8 回答
尽管Python在Neovim中工作得很好,但插件不能识别Neovim中的Python主机
4 回答
尽管python字典包含了大量的条目,但它并没有增长
9 回答
尽管python说模块存在,为什么我会得到这个消息?
8 回答
尽管setuptools和控制盘是最新的,但无法识别singleversionexternallymanaged
10 回答
尽管stdout和stderr重定向,但未捕获错误消息
10 回答
尽管Tensorboard的事件太大,但Tensorboard的步骤太少了
2 回答
尽管tkinter上的变量已更改,但显示未更改
4 回答
尽管try/except使用Python进行单元测试时出现断言错误
3 回答
尽管URL是sam,但仍会抛出“达到最大重定向”
3 回答
尽管url有效,Pandas仍读取url的\u csv错误
1 回答
尽管while中存在时间延迟,但LINUX线程的CPU利用率为100%(1)
10 回答
尽管x0在范围内,Scipy优化仍会引发ValueError
9 回答
尽管xpath正确,但使用selenium单击链接仍不起作用
9 回答
尽管下载了ffmpeg并设置了路径变量python,但没有后端错误
4 回答
尽管下载了i,但找不到型号“fr”
8 回答
尽管下载了plotnine包,但未获取名为“plotnine”的模块时出错
6 回答
尽管为所有行指定了权重,网格(0)仍不起作用
7 回答