腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
Z3
中
警告消息“找不到
量词
的
模式
(
量词
id: k!18)失败”背后
的
原因是什么?
z3
我发现了一个问题,如下面这个简单
的
SMT-LIB程序所示。
浏览 0
提问于2012-02-08
得票数 7
回答已采纳
1
回答
显示
Z3
对
量词
的
推断
模式
triggers
、
z3
、
quantifiers
我想看看
Z3
对我
的
公式
中
的
一些
量词
使用了什么
模式
。如何让
Z3
打印这些信息?
浏览 3
提问于2017-08-24
得票数 0
回答已采纳
1
回答
将包含函数公理化为
Z3
列表
的
不同方法
list
、
encoding
、
z3
、
axiom
将列表上
的
包含操作()公理化为 (not (Seq.innil)) (Seq.in xs e) (= e (head xs))使
Z3
4.0能够反驳该断言(assert (Seq.in nil x)) (check-sat) ; UNSAT,
浏览 1
提问于2012-06-20
得票数 1
回答已采纳
1
回答
在
Z3
中
自定义LIA
量词
消除
z3
、
quantifiers
我正在使用F#和
Z3
3.2API对LIA进行
量词
消除。我想在内部问一下,
Z3
3.2是如何知道使用哪种方法来消除
量词
的
?用户会像以前
的
QUANT_ARITH一样影响方法
的
选择吗? 此外,随着
的
引入,
Z3</em
浏览 3
提问于2011-10-15
得票数 2
回答已采纳
1
回答
量词
消除-更多问题
z3
然而,对于真实
的
案例,它可以消除。(当i和k都是实数时)对于整数来说,消除
量词
是不是更难?我知道在
量词
消除后,这些约束被简化为线性约束。 我认为
z3
在检查可满足性之前会自动进行
量词
消
浏览 1
提问于2012-05-04
得票数 5
回答已采纳
1
回答
用
Z3
确定BV查询
的
量词
消去难度
z3
、
smt
、
quantifiers
我目前正在使用
Z3
C++ API来解决位向量上
的
查询。有些查询可能在顶层包含一个存在
量词
。 通常情况下,
量词
消除很简单,并且可以由
Z3
快速执行。但是,在
量词
消除返回到枚举数千个可行解决方案
的
情况下,我想放弃这一策略,并以其他方式处理查询。我试过用“尝试-为”策略包装‘qe’-策略,希望如果
量词
消除失败(比如100 if ),我会知道我最好以其他方式处理查询。不幸
的
是,“尝试-for”策略无法取消
量词
消除(对于任何时
浏览 5
提问于2015-09-06
得票数 4
回答已采纳
1
回答
如何在
Z3
中
进行增量解决?
z3
、
smt
关于
Z3
如何增量地解决问题,我有一个问题。在阅读了这里
的
一些答案后,我发现如下: 在假设
模式
(我不知道名称,也就是我想到
的
名称)
中
,
z3
不会简化某些公式,例如
浏览 2
提问于2013-05-07
得票数 54
回答已采纳
1
回答
禁止在线性算术证明
中
引入Skolem函数
z3
(<= (ite (< (re$ s$) 0.0) (- (re$ s$)) (re$ s$)) (+ r$ 1.0)))) :named a0))(get-proof)(ALL v0.也就是说,有没有一个选项可以让
Z3
在不使用Skolem函数
的
情况下生成一个证明?原则上,这应该是可能
的
,因为
Z3
版本3.2找到了不需要Skolem
浏览 0
提问于2014-09-29
得票数 0
1
回答
在
Z3
中
证明归纳事实
z3
、
smt
我试图证明
Z3
中
的
一个归纳事实,这是一个微软
的
SMT解算器。我知道
Z3
通常不提供此功能,如 (第8节:数据类型)中所解释
的
,但当我们约束我们想要证明事实
的
域时,这似乎是可能
的
。问题是,当我们进一步放松此约束时(我们将上一个示例
中
的
20替换为任何大于20
的
整数),求解器将以unknown作为响应。我觉得这很奇怪,因为
Z3
解决原始问题
的
时间并不长,但当我们将上限增加1
浏览 4
提问于2012-11-02
得票数 4
回答已采纳
1
回答
获取包含量化布尔变量
的
问题
的
模型
z3
我正在使用
Z3
来检查逻辑
中
的
可满足性,包括线性整数运算、未解释
的
函数和布尔变量上
的
量词
。
Z3
没有为可满足
的
问题提供模型,我想这是因为
量词
(或者我选择
的
逻辑: AUFLIA)。除了自己实例化所有布尔变量之外,有没有办法让
Z3
为我提供此类问题
的
模型?
浏览 2
提问于2011-09-08
得票数 2
1
回答
从Ocaml调用
Z3
为黑匣子
ocaml
、
z3
、
formal-verification
、
first-order-logic
、
satisfiability
为了避免实现所需
的
所有有效性和
量词
消除方法,我希望能够在Ocaml
中
访问
Z3
的
量词
消去策略。有人能帮忙吗?我问这是为了找到更多
的
信息,类似的问题在未来。
浏览 3
提问于2021-11-09
得票数 2
回答已采纳
1
回答
没有
量词
的
z3
数据类型匹配
z3
假设我在
z3
中
创建了一个数据类型
z3
:现在,我可以声明一个变量t,然后断言t是一个c类型:(declare-fun t () A)然而,这需要一个存在
量词
。我
的
问题是:没有
量词
就能做到这一点吗? 具体来说,我想要一个表达式,比如is_c t或其他类似于(exists ((x Int)) (= t
浏览 6
提问于2018-01-05
得票数 1
回答已采纳
2
回答
使用数组
的
Z3
Forall
arrays
、
z3
、
quantifiers
Z3
为这个简单
的
问题提供了未知: (assert (= (select y 1) 0))(check-sat) 我发现如果否定forall,它就变成了sat,但这似乎是一件特别简单
的
事情,无法解决。这引起了一些问题,因为我想解决
的
问题更像是, (declare-fun u () Int) (forall ((y (Array Int Int)) ) (=>(= u 0) (<= (select y 1) 0))
浏览 53
提问于2020-08-27
得票数 1
回答已采纳
1
回答
z3
:超时
的
原因可能是什么(rise4fun)
z3
问题是:在rise4fun
中
尝试时超时: 我已经试着不使用"forall",但它也不起作用。
浏览 0
提问于2015-05-30
得票数 1
1
回答
Z3
v4.3+是否支持非线性算术
的
量词
消除
z3
、
nonlinear-functions
、
quantifiers
我找不到
Z3
完全支持哪种
量词
消除。我得到
的
是一个关于-in一般非线性项
的
通用量化公式。我想得到一个等价
的
无
量词
公式。使用
Z3
可以做到这一点吗? 谢谢,弗里德里希
浏览 1
提问于2013-04-17
得票数 1
回答已采纳
1
回答
在
Z3
中
,pull_nested_quantifiers选项是否与simplify一起使用?
z3
、
quantifiers
我希望将公式
中
的
所有嵌套
量词
拉到最外层。我希望以下命令能在
Z3
中
工作,但它们不能:(simplify (exists ((x Int)) (and (>=) :pull-nested-quantifiers
的
用途是什么如何使用SMT-LI
浏览 6
提问于2012-03-07
得票数 1
回答已采纳
1
回答
Z3
是否使用了用户在"AUFLIA-p“部分
中
为smtComp结果提供
的
模式
?
z3
、
smt
我正在测试一些简化
的
通用性(主要是:定向部分
量词
实例化)。因此,我在smtComp
的
"AUFLIA-p“部分运行了一组基准测试,无论是否简化。为了尽可能减少副作用,我对在没有(用户提供)
模式
的
情况下运行
Z3
很感兴趣。 我在"AUFLIA-p“一节
中
研究了一些基准,我想知道为什么这一节
的
基准包含
模式
。也许您已经为这一部分运行了
Z3
,并提供了禁用
模式
的
选项。最近,我
浏览 0
提问于2012-09-11
得票数 2
3
回答
如何利用
Z3
的
Python实现
量词
消去
z3
、
smt
、
z3py
如何使用
Z3
的
Python执行
量词
消除?虽然我检查了教程和API,但无法做到这一点。谢谢! 此外:在做了
量词
消除后,我将“添加”与另一个无
量词
公式。那么,如果我使用这个策略,有没有办法将一个子目标(这是策略
的
输出)转
浏览 0
提问于2013-07-28
得票数 4
回答已采纳
1
回答
Z3
支持哪些SMT-LIB属性?为什么?
z3
SMT-LIB标准支持任意属性,但只规定了很少
的
属性,例如:pattern。另一方面,
Z3
目前只支持几个选定
的
属性,并对未识别的属性发出警告。 支持哪些属性,它们
的
典型用例是什么?
浏览 0
提问于2020-06-22
得票数 1
1
回答
(应用qe)不会一次消除所有
量词
?
z3
、
quantifiers
我要求
Z3
使用SMTLIB2接口在UFLIA理论中进行
量词
消除。所以我断言一个公式有21个存在量化
的
变量,其中7个是整数,14个是布尔型。然后我做(apply qe),
Z3
返回一个目标,它仍然包含九个存在量化
的
变量,名为(x!1 Int),(x!14 Int)和(x!14!1 Int)到(x!14!7 Int)。这是否意味着qe策略不会一次消除所有
量词
? 如果我执行两次(assert qe),除了重命名
的
量化变量之外,目标保持不变。但是,如果我从目标中提取量化公式,自己
浏览 4
提问于2013-08-27
得票数 2
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
(七)Perl中的模式匹配和模式替换介绍
Netty中的设计模式(一)建造者设计模式
Python 中的单例模式
python 中的设计模式(1)
Python编程中的反模式
热门
标签
更多标签
云服务器
ICP备案
对象存储
实时音视频
即时通信 IM
活动推荐
运营活动
广告
关闭
领券