z3 - 优文库

z3

0热度

1回答

我正在使用C++ API for z3，因此我不需要担心引用计数或内存管理。但是，我想使用沿着std::map<Z3_ast, some_struct>的行std :: map存储信息对z3 AST。当一个特定的Z3_ast对象被删除时，我想从这张地图中删除它的条目。有没有办法建立一个回调函数，当 Z3_ast对象的引用计数返回到0并且Z3_ast对象被删除时将被调用？

1热度

1回答

如果在z3py中声明

我是z3py的新用户。我需要写检查一些规则的满意度像 IF room.temp < 18 THEN room.fireplace = on IF room.temp > 24 THEN room.fireplace = off IF room.CO > 180 THEN room.fireplace = off IF room.temp > 28 THEN house.hvac = off

0热度

1回答

在Z3 .NET API中优化会导致错误的结果 - bug？

我正在使用Z3的.NET API，并且使用下面的代码发现了奇怪的行为（可能是优化器中的错误）。与类Optimize一起运行时，它不正确地找到解决方案，而与类Solver一起运行时，它正确地报告不可行。任何人都可以运行代码来验证我的声明？任何有关正在发生的事情的提示都将受到高度赞赏。亲切的问候马立克 using System; using System.Collections.Generic;

0热度

1回答

z3中的主要含义

我使用z3求解器查找QF_AUBV逻辑中用于查找公式（最小）主要含义的解决方案。是否有可能从z3求解器中获得这样的部分主要含义？

0热度

1回答

Z3量化公式暗示给予不足

我还是Z3的新手，因此不确定为什么我不满足下面的公式;它应该至少适用于那些ts_var数组，每个数组元素（bitvector）（32个数组元素）在32位的不同位置上有1，而在所有其他位置上有0（所以bvxor结果将会不同）。那么对于我在做什么的任何建议或提示都是错误的？当我在exp4（（=> a！1 a！2））中以与代码中相反的方式做了暗示的时候，Z3产生了SAT！但这不是我想要的。我想找到一个数

0热度

1回答

将子句直接添加到z3解算器

我有一个AIG（和逆变器图），我一直在修改它，并且需要使用Z3以增量方式检查其可满足性。我可以生成AIG的CNF表示，并且理想情况下将这些子句直接提供给求解器，并从我的代码中重复调用它。有什么方法可以通过C/C++ API直接向Z3求解器添加子句（或AIG）？

1热度

1回答

量词和数组在Z3

Z3的答案为“未知”时，给出了使用量词在阵列验证码： (declare-const ia Int) (declare-const ib Int) (declare-const la Int) (declare-const lb Int) (declare-const A (Array Int Int)) (declare-const a (Array Int Int)) (declar

2热度

1回答

有没有办法在C＃中使用Z3求解器的最大化/最小化目标？

我正在寻找一种方法来使用.NET API将最小化/最大化目标添加到Z3解算器。有什么办法吗？感谢您的帮助和圣诞快乐:-)

0热度

1回答

Z3Py：解析表达式使用eval或z3.parse_smt2_string

我正在写一个python程序，其中包括其他事情必须将大型命题公式转换为z3实例。例如，可以通过我的程序通过 a = my_atomic_proposition("a") # Bool b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42 c = my_atomic_proposition("c") # Bool f =

0热度

1回答

Z3中的部分分配

我有一个布尔公式（格式：CNF），它的满足性我使用Z3 SAT解算器进行检查。当公式可以满足时，我有兴趣获得部分作业。我试图用model.partial=true对一个OR门的简单公式进行分析，但没有得到任何部分分配。你能建议如何做到这一点吗？除了它是部分的，我对任务没有任何限制。