-
1 votesanswersviews
Z3 API中的自定义理论求解器方法发生了什么变化？
我一直在阅读Nikolai关于Z3工程理论的文章，了解如何将自定义决策程序与Z3接口 . 在那里提到了几种方法，如AssertTheoryAxiom，NewAssignment和FinalCheck等 . 但是我无法在http://research.microsoft.com/en-us/um/redmond/projects/z3/namespace_microsoft_1_1_z3.html的... -
7 votesanswersviews
在位向量算法的决策过程中使用术语重写
我正在研究一个项目，其重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对于某些决策程序（例如基于钻头爆破的程序）的先前步骤是有用的 . 术语重写可以完全解决问题，或者产生更简单的等效问题，因此两者的组合可以导致相当大的加速 . 我知道许多SMT求解器实现了这种策略（例如Boolector，Beaver，Alt-Ergo或Z3），但是很难找到详细描述这些重写步骤的论文/技术报告/等 . 一... -
0 votesanswersviews
可以通过命名表达式实现软约束吗？
我想知道是否可以使用命名表达式来实现软约束，而无需明确使用手动“跟踪”变量 . 在消息Soft/Hard constraints in Z3中，Leonardo解释了如何使用辅助布尔值以手动方式实现软约束 . 在以下消息：z3 behaviour changing on request for unsat core中，莱昂纳多说命名表达式基本上被视为模型查找的含义 . 使用上面第一条消... -
0 votesanswersviews
Python相当于Z3_API Z3_benchmark_to_smtlib_string的第7个参数
我们目前在python上使用z3来检查程序跟踪的可行性 . 基于跟踪我们创建z3公式和断言，我们的下一个方法是使用SMT2作为中间语言通过Z3_benchmark_to_smtlib_string将这些断言提供给iZ3和smtinterpol . 一个小例子：x = Int（'x'）y = Int（'y'） s = Solver() # Assertions s.assert_and_track... -
2 votesanswersviews
订单理论的定制理论求解器？
我的程序，反应有限状态系统的有限合成器，产生SMT查询以注释（未解释的）系统的产品自动机和规范 . 本质上，它是一个使用未解释函数检查的模型 . 如果注释存在=> Z3找到的模型满足规范 . 查询包含： 数据类型（用于编码系统和规范自动机的状态） =（更大），>（严格地）（指定自动机系统*规范的状态的排序函数，用于搜索具有不良状态的套索）或换句话说，对该自动机的状态的排序， ... -
1 votesanswersviews
Z3 - check-sat-using的参数
抱歉，如果这是一个愚蠢的问题 - 我对使用Z3（以及一般的SMT）很陌生 - 但我有点难过 . 假设我有两个SMT2输入语言文件，略有不同，总结如下： (define-fun T ((i Int)) Bool (... - too long to paste completely, but does define $prop) (assert (T 0)) (declare-fun assum1 ... -
0 votesanswersviews
使用C，使用Z3_parse_smtlib2_string在Z3中获取Unsat Core
我需要使用 Z3_parse_smtlib2_string 使用C API将一些SMTLIB字符串解析为Z3，并使用Z3 C API来查找不满核心 . 我知道还有其他方法可以找到更容易且不那么繁琐的here和here描述的不饱和核心，但我真的希望能够仅使用从字符串解析到Z3的数据结构来做到这一点 . 原因是我试图使用Z3自动化某些东西 . 很明显，如果我将这个SMTLIB程序传递给Z3，那就是UN... -
3 votesanswersviews
SMT求解器中约束强化的效率
解决优化问题的一种方法是使用SMT求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到命题不再可满足为止 . 例如，http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf讨论了这种方法 . 这种方法有效吗... -
0 votesanswersviews
跟踪非线性实数算术断言使用含义与：命名机制给出不同的答案
在尝试解决大型非线性实际算术问题时，我使用答案文字和显式含义来跟踪每个断言，如其他帖子中所建议的那样 . 它应该等同于使用SMT2格式的（！（...）：named p1）语法 . 但是，似乎两种方法在内部都有不同的处理方式 . 以下SMT2代码给出了UNKNOWN结果，解释为“（不完整（理论算术））”： (set-option :print-success false) (set-option ... -
0 votesanswersviews
具有前提的非线性实数算法的可解性
一个小例子表明，当NRA断言由与（sat p1 ... pn）检查相关的前提pi标记时，非线性实数算术（NRA）求解器受到阻碍 . 以下SMT2示例返回具有正确模型的SAT： (declare-const p1 Bool) (declare-const p2 Bool) (declare-const p3 Bool) (declare-const p4 Bool) (declare-const ... -
2 votesanswersviews
支持在SAT时获取模型（类似于CVC4中的--dump-models）
在开源之后我刚开始玩Z3求解器 . 我目前使用Z3作为命令行黑盒工具，如果模型是SAT，我希望它可以转储反例 . 我主要通过QF_NIA和QF_LIA查询 . 我注意到在Z3中不存在等同于CVC4s --dump-models的选项 . 我可以在SMT2lib文件中写入（check-sat）之后写入（dump-model），但如果公式实际上不满意则会出错 . SMT2 lib的语言虽然看起来很低调... -
0 votesanswersviews
Z3 Java API - 获得不满的核心
我试图弄清楚如何使用Java API for Z3获得不饱和核心 . 我们的场景如下（代码在下面，在rise4fun中工作）： 我们以编程方式创建SMT2输入 输入包含函数定义，数据类型声明和断言 我们使用parseSMTLIB2String API解析它 我们确保上下文和解算器具有unsat_core - > true Z3为提供的输入返回UNSAT，这是正确的 ... -
3 votesanswersviews
Z3：非线性算术和量词 - 错误的结果？
这是一个生成“sat”的Z3查询 . （我正在运行Z3版本4.8.0，结果在rise4fun Web界面中是相同的 . ） (assert (forall ((x Real)) (exists ((y Real)) (and (<= 0.0 y) (<= y 1.0) (<= x (* y y)))))) (check-sat) ... -
3 votesanswersviews
列表的理论是可判定的吗？
我想知道列表的z3理论是否可判定？看起来我们只能证明事实是不完整但不能使用理论，所以我很好奇它是否真的可以判断 . 谢谢你的帮助 . -
3 votesanswersviews
使用理论插件和解算器
Z3的最新版本将 Z3_context 和 Z3_solver 的概念分离 . API主要反映了这些变化;例如 push 在上下文中被弃用，并被重新指定为将求解器作为额外参数 . 然而，理论界面尚未更新 . 理论仍然是从上下文创建的，据我所知，从未明确地附加到求解器上 . 人们可能会认为从上下文创建的理论将始终附加到从上下文创建的所有求解器，但从我们的经验来看，似乎并非如此 . 相反，用户定义的... -
1 votesanswersviews
以正确的策略加速z3-solver
我创建了大约20k的约束，在我的机器上解决它们大约需要3分钟 . 我有不同类型的约束，下面我举例并解释它们 . 我将断言上传到http://filebin.ca/vKcV1gvuGG3 . 我对解决更大的约束系统感兴趣，因此我想加快这个过程 . 我想问你是否有关于如何更快地解决问题的建议，例如：通过使用适当的策略 . 从策略教程我知道战术，但我似乎没有通过应用战术得到积极的差异...... li ... -
1 votesanswersviews
z3实存的存在论
Z3是否决定了非线性实数算术的存在性片段？也就是说，我可以将它作为一个决策程序用于测试带有和x的量词无关公式是否具有超过实数的解决方案？ -
0 votesanswersviews
在Z3中 Build 自定义理论
这个问题是对以下问题的跟进 . Procedural Attachment in Z3 我有一个谓词（我在这种情况下使用“更重”的名称）超过两个整数，我需要使用自定义算法进行评估 . 我编写了以下代码来完成它 . 但我发现传递给函数CMTh_reduce_app（）的参数不是实际的整数，而是整数类型的consts . 我需要的是2个整数，这样我就可以评估谓词并返回结果（现在函数CMTh_reduc... -
1 votesanswersviews
没有元组（declare-datatypes）？
我用SMT-LIB的Z3方言写了一个大型的库 . 不幸的是，我使用 (declare-datatypes) 来创建元组意味着我无法按照我的意愿将逻辑设置为 QF_AUFBV . 这有使我的脚本更慢（有时超时）的副作用比我以编程方式手动创建公式并使用 QF_ABV 解决 . 因此，我想从我的脚本中删除 (declare-datatypes) . 大多数数据类型可以编码为位向量 . 但是，库中最重... -
1 votesanswersviews
随机可满足模理论
有人知道Z3是否支持SSMT（即随机量词）或是否有计划添加它？ Reference paper -
3 votesanswersviews
Z3 / SMT：我什么时候应该选择push / pop来重置？
我使用Z3来解决符号 Actuator 产生的路径条件，它以深度优先顺序探索状态空间，与CUTE，DART或（可能）SAGE非常相似 . 我们正在尝试使用Z3的不同方法 . 在一个极端，我们将每个查询发送到Z3并立即（重置）它 . 另一方面，我们（推）每个额外的分支约束，并且（弹出）（pop）在回溯时正确削弱路径条件所需的最小值 . 问题是，在所有情况下，没有任何策略似乎比任何其他策略更好 . 推... -
2 votesanswersviews
将z3 C API ast（或解算器）对象转换为SMTLIB字符串
我正在玩z3和其他SMT求解器，并且想要检查其他求解器如boolector胜过z3的情况，反之亦然 . 为此，我需要一种方法将声明和断言转换为SMT-LIB2格式，而其他SMT求解器可以识别这种格式 . 例如，对于此示例 void print_as_smtlib2_string() { context c; expr x = c.int_const("x"); ... -
2 votesanswersviews
Z3位向量操作
如何使用'repeat'和'rotate_left'位向量操作？ 更一般地说，在哪里可以找到Z3使用的SMT2脚本格式的bitvector操作的详细文档？ 我发现的一切似乎只是去教程或破坏的链接：https://github.com/Z3Prover/z3/wiki/Documentationhttp://research.microsoft.com/en-us/um/redmond/projec... -
1 votesanswersviews
在SMT中表达不关心的位向量
我想定义一个接受位向量的函数，如果某个位置的位满足某些值，则返回true . 例如：如果bitvector是1x00x01x，我需要返回true，其中x表示不关心 . 我目前的实施是： (define-fun function_i ((i (_ BitVec 8))) Bool (and true (= #b1 ((_ extract 1 1) i)) (=... -
12 votesanswersviews
用Z3 / SMT-LIB2定义集合论
我正在尝试使用SMTLIB接口为Z3定义集合理论（并集，交集等） . 不幸的是，我的当前定义为一个简单的查询挂起z3，所以我想我错过了一些简单的选项/标志 . 这是永久链接：http://rise4fun.com/Z3/JomY (declare-sort Set) (declare-fun emp () Set) (declare-fun add (Set Int) Set) (declare-... -
2 votesanswersviews
为什么连词的E匹配对订单/案例分割策略敏感？
鉴于以下简化量词，根据Boogie生成的Z3选项设置（下面的完整详细信息），我得到“未知”的结果： (declare-fun F (Int) Bool) (declare-fun G (Int) Bool) (assert (forall ((x Int)) (! (and (F x) (G x)) :pattern ((F x)) ))) (assert (not (forall ((... -
1 votesanswersviews
Z3 MBQI针对同一模型的API和SMT-LIB之间的不同行为
我正在使用Z3来检查一些量化的公式 . 如果我通过Z3的Java API断言公式，如果公式不合格，MBQI引擎可能不会收敛 . 我知道我的公式不是FOL的片段，已知它是可判定的，但是如果我通过Z3的smt-lib接口输入相同的公式，它会很快产生答案 . 我怀疑某些选项不是通过通常使用正常SMTLIB输入激活的API设置的，或者我没有通过API向公式添加重要的元信息 . 以下SMTLIB会话中的断言... -
1 votesanswersviews
使用Z3和SMT-LIB定义具有实数的sqrt函数
我如何以smt-libv2格式编写sqrt函数 . 注意：要获得最多两个值，我在这里找到了一个有用的链接：Use Z3 and SMT-LIB to get a maximum of two values . -
2 votesanswersviews
Z3无法找到具有量词和模式的简单公式的令人满意的赋值
我目前正在为Z3之上的编程语言编写一个自动Verifier作为一个有趣的项目，我试图用它来证明使用循环的fibonacci实现等同于递归 . 如果输入程序是正确的，它似乎有效，即它为Z3生成合理的输入，Z3表示它是不可满足的，这意味着在我的上下文中，程序是正确的 . 但是当我改变一个变量初始化并因此使程序不正确时，我的验证者提出了以下Z3公式，这对我来说似乎并不太复杂，但Z3说“未知” . (se... -
3 votesanswersviews
z3是否支持将运算符标记为关联运算符，可交换运算符或两者兼有？
我想用SMT格式编写证明义务，其中一些函数具有一些共同的通用属性（即关联性和可交换性） . 一个简单的解决方案是在证明义务中包含相应的公理 . 我想这意味着这些属性的推理将在很大程度上取决于量词实例化算法 . 其他技术，如重写，可能更有效，我想知道Z3是否实现了这种技术 . API中存在诸如Z3_OP_PR_REFLEXIVITY和Z3_OP_PR_COMMUTATIVITY之类的值表明这可能是...