Loading [MathJax]/jax/output/CommonHTML/config.js

社区首页 >问答首页 >与z3.Optimize()一起使用z3py unsat内核

问与z3.Optimize()一起使用z3py unsat内核
EN

Stack Overflow用户

提问于 2018-06-19 17:33:38

回答 1查看 187关注 0票数 1

我使用的是z3 python api。我希望一方面使用Z3的非side核心功能，另一方面能够针对某些标准进行优化。

self.solver = z3.Solver()
self._solver.assert_and_track(constraint1, error_message1)
self._solver.assert_and_track(constraint2, error_message2)
...
self._solver.check()

if len(self._solver.unsat_core()) > 0
  print (self._solver.unsat_core())

这很好用。但除此之外，我还可以使用z3.Optimize()中的maximize()和minimize()函数。可以一起使用吗？

这里的区别是什么？

EN

回答 1

Stack Overflow用户

发布于 2018-06-19 18:41:49

Z3不支持同时生成优化和非饱和内核。这是大约两个月前的相关门票：https://github.com/Z3Prover/z3/issues/1577

请注意，这并不是因为它不能实现:只是他们还没有实现它。在那里注册您的请求可能会激励他们添加支持！

关于你用隐含的方式跟踪未饱和内核的问题:我认为这基本上就是assert_and_track所做的。你可以在这里看到它的源代码：https://github.com/Z3Prover/z3/blob/d2c937a989ea360e9cba06583eccaa257c75870f/src/api/python/z3/z3.py#L6418-L6446是不是因为某种原因它不能为你工作？

票数 0

EN

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/50934008

复制

相关文章

详解ANGULAR2组件中的变化检测机制（对比ANGULAR1的脏检测）

typescript angularjs

组件和变化检测器如你所知，Angular 2 应用程序是一颗组件树，而每个组件都有自己的变化检测器，这意味着应用程序也是一颗变化检测器树。顺便说一句，你可能会想。是由谁来生成变化检测器？这是个好问题，它们是由代码生成。 Angular 2 编译器为每个组件自动创建变化检测器，而且最终生成的这些代码 JavaScript VM友好代码。这也是为什么新的变化检测是快速的 (相比于 Angular 1.x 的 $digest)。基本上，每个组件可以在几毫秒内执行数万次检测。因此你的应用程序可以快速执行，而无需调

前朝楚水

2018/04/03

2.9K0

jQuery 双击事件（dblclick）时，不触发单击事件(click)

在jQuery的事件绑定中，执行双击事件(dblclick)时能触发两次单击事件(click)。即一个标签元素（如div等），如果元素同时绑定了单击事件(click)和双击事件(dblclick),那么执行单击事件(click)时，不会触发双击事件(dblclick)，执行双击事件(dblclick)时却会触发两次单击事件(click)。先看一下点击事件的执行顺序：

飞奔去旅行

2019/06/13

5.3K0

angular4实战（4）ngrx

javascript node.js https 网络安全 redux

版权声明：本文为博主原创文章，未经博主允许不得转载。 https://blog.csdn.net/j_bleach/article/details/78161765

j_bleach

2019/07/02

1.1K0

angular4实战（4）ngrx

Angular开发实践（五）：深入解析变化监测

什么是变化监测在使用 Angular 进行开发中，我们常用到 Angular 中的绑定——模型到视图的输入绑定、视图到模型的输出绑定以及视图与模型的双向绑定。而这些绑定的值之所以能在视图与模型之间保持同步，正是得益于Angular中的变化监测。简单来说，变化监测就是 Angular 用来监测视图与模型之间绑定的值是否发生了改变，当监测到模型中绑定的值发生改变时，则同步到视图上，反之，当监测到视图上绑定的值发生改变时，则回调对应的绑定函数。变化监测的源头变化监测的关键在于如何最小粒度地监测到绑定的值是

laixiangran

2018/04/11

1.8K0

JavaScript 技巧篇-js增加延迟时间解决单击双击事件冲突，双击事件触发单击事件

click settimeout store 事件原理

js 的单双击事件同时存在会有一个问题：双击事件会同时触发单击事件，两个事件存在冲突。我们加一个延迟时间就能很好的解决这个问题。

小蓝枣

2020/09/23

6.1K0

angular-cli.json配置参数解释，以及依稀常用命令的通用关键参数解释

json cli 配置

一. angular-cli.json常见配置 { "project": { "name": "ng-admin", //项目名称 "ejected": false // 标记该应用是否已经执行过eject命令把webpack配置释放出来 }, "apps": [ { "root": "src", // 源码根目录 "outDir": "dist", // 编译后的输出目录，默认是dist/ "assets": [ // 记录资源文件夹

喝茶去

2019/04/16

1.6K0

在触发思考

费用中心 sql

读到周洲同学的博客,看到一篇关于触发器的文章,是在用户充值时,须要在t_reCharge表中插入一条记录,同一时候更新t_card表以保证数据一致性.我们当时没想特别多,没想到触发器,就是写了多条sql语句,为了不出错后来使用了事务或存储过程,没记错的话是放在存储过程里了。她是这么实现的:

全栈程序员站长

2022/07/06

6960

Angular 实践：如何优雅地发起和处理请求

Tips: 本文实现重度依赖 ObservableInput，灵感来自同事 @Mengqi Zhang 实现的 asyncData 指令，但之前没有 ObservableInput 的装饰器，处理响应 Input 变更相对麻烦一些，所以这里使用 ObservableInput 重新实现。

灵雀云

2020/02/26

8660

Angular 实践：如何优雅地发起和处理请求

只在必要时保存服务器控件视图状态

编程算法 java

自动视图状态管理是服务器控件的功能，该功能使服务器控件可以在往返过程上重新填充它们的属性值（您不需要编写任何代码）。但是，因为服务器控件的视图状态在隐藏的窗体字段中往返于服务器，所以该功能确实会对性能产生影响。您应该知道在哪些情况下视图状态会有所帮助，在哪些情况下它影响页的性能。例如，如果您将服务器控件绑定到每个往返过程上的数据，则将用从数据绑定操作获得的新值替换保存的视图状态。在这种情况下，禁用视图状态可以节省处理时间。

Java架构师必看

2021/03/22

6280

关于 title 属性导致触发 mousedown 事件时连带触发 mousemove

　　大家都知道，鼠标点击的整个事件的执行流程是：mousedown -> mouseup -> click ，而拖放的整个流程是：mousedown -> mousemove -> mouseup -> click

胡尐睿丶

2022/03/28

1.3K0

选择篇(039)-单击按钮时event.target是什么?

button event 事件数组

导致事件的最深嵌套元素是事件的目标。你可以通过event.stopPropagation停止冒泡

齐丶先丶森

2022/05/12

1.6K0

Map 有变动时触发特定行为实现

在平时开发过程中，通常我们会选择使用 Guava 的 Cache 类用作本地缓存。

明明如月学长

2021/11/11

5750

input输入中文时，拼音触发input事件

在上一篇文章中写到了函数防抖，在使用函数防抖来进行搜索框优化的时候会遇到一个问题，就是监听文本输入框的input事件，在拼写汉字（输入法）但汉字并未实际填充到文本框中时会触发input事件，会出现下图的效果

OECOM

2020/07/01

8.2K1

Angular学习（02）--Angular-CLI命令

angularjs 打包 typescript c++

官方的教程，其实已经很详细且易懂，这里再次梳理的目的在于复习和巩固相关知识点，刚开始接触学习 Angular 的还是建议以官网为主。

请叫我大苏

2019/03/19

2.6K0

Angular学习（02）--Angular-CLI命令

Android Button 单击事件

方法一：在XML文件中指定单击事件函数 <Button android:id="@+id/button1" android:layout_width="120dip" android:layout_height="wrap_content" android:layout_alignParentLeft="true" android:layout_below="@+id/textView1

磊哥

2018/05/08

1.7K0

点击加载更多

相似问题

JOOQ LoggerListener扩展调试日志记录

120

wordpress的调试日志不工作

32

春季调试日志记录级别不工作

17

spring-jooq，事务不工作

10

django-调试-工具栏日志不工作？

12

添加站长进交流群

领取专属 10元无门槛券

AI混元助手 在线答疑

关注 腾讯云开发者公众号

洞察 腾讯核心技术

剖析业界实践案例