- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
你能告诉我如何拆分 unsat 核心的子句吗?这是问题2,关于找到unsat核心后,我将尝试再次寻找。您愿意告诉我如何做到这一点吗?
非常感谢。
如何拆分子句如下
`and` (`or` (`<=_int` 1002 x1) (`<=_int` 1000 x1)) (`and` (`or` (`<=_int` 0 (`+_int` x2 (`*_int` -1003 x1))) (`<=_int` 0 (`+_int` x2 (`*_int` -1230 x1)))) (`and` (`or` (`<=_int` 0 (`+_int` x3 (`*_int` -1999 x2)))
关于问题2,
cout<<s.check(3,assumptions)<<endl;
expr_vector core = s.unsat_core();
................
expr assumptions2[2] = {p1,p3};
cout<<"check next"<<s.check(2,assumptions2)<<endl;
expr_vector core1 = s.unsat_core();
for(unsigned int k=0;k<core1.size();++k){
cout<<"New core size "<<k<<endl;
cout<<"New unsat core "<<core1[k]<<endl;
}
再次调用unsat core函数,无法再次给unsat cores。非常感谢。
最佳答案
我不确定我是否理解你的问题。您似乎有一个 (and c1 (and c2 c3))
形式的断言,并且您想跟踪 c1
, c2
和 c3
单独。
在 Z3 中,我们使用答案文字来跟踪断言。答案文字本质上是一个新的 bool 值,用于跟踪断言。也就是说,该断言是否(由 Z3)用于显示整组断言的不可满足性。例如,如果我们要跟踪断言 F
,我们创建一个新的 bool 变量 p
并断言 p implies F
.然后,我们提供p
作为检查方法的参数。
如果F
是一个大合取,我们想单独跟踪它的元素,我们应该提取它的元素并为每个元素创建一个答案文字。这是完成此操作的完整示例。您可以通过将其包含在 example.cpp
中来对其进行测试Z3 发行版中包含的文件。请注意,您必须包括 #include<vector>
.
/**
\brief Unsat core example 2
*/
void unsat_core_example2() {
std::cout << "unsat core example 2\n";
context c;
// The answer literal mechanism, described in the previous example,
// tracks assertions. An assertion can be a complicated
// formula containing containing the conjunction of many subformulas.
expr p1 = c.bool_const("p1");
expr x = c.int_const("x");
expr y = c.int_const("y");
solver s(c);
expr F = x > 10 && y > x && y < 5 && y > 0;
s.add(implies(p1, F));
expr assumptions[1] = { p1 };
std::cout << s.check(1, assumptions) << "\n";
expr_vector core = s.unsat_core();
std::cout << core << "\n";
std::cout << "size: " << core.size() << "\n";
for (unsigned i = 0; i < core.size(); i++) {
std::cout << core[i] << "\n";
}
// The core is not very informative, since p1 is tracking the formula F
// that is a conjunction of subformulas.
// Now, we use the following piece of code to break this conjunction
// into individual subformulas. First, we flat the conjunctions by
// using the method simplify.
std::vector<expr> qs; // auxiliary vector used to store new answer literals.
assert(F.is_app()); // I'm assuming F is an application.
if (F.decl().decl_kind() == Z3_OP_AND) {
// F is a conjunction
std::cout << "F num. args (before simplify): " << F.num_args() << "\n";
F = F.simplify();
std::cout << "F num. args (after simplify): " << F.num_args() << "\n";
for (unsigned i = 0; i < F.num_args(); i++) {
std::cout << "Creating answer literal q" << i << " for " << F.arg(i) << "\n";
std::stringstream qname; qname << "q" << i;
expr qi = c.bool_const(qname.str().c_str()); // create a new answer literal
s.add(implies(qi, F.arg(i)));
qs.push_back(qi);
}
}
// The solver s already contains p1 => F
// To disable F, we add (not p1) as an additional assumption
qs.push_back(!p1);
std::cout << s.check(qs.size(), &qs[0]) << "\n";
expr_vector core2 = s.unsat_core();
std::cout << core2 << "\n";
std::cout << "size: " << core2.size() << "\n";
for (unsigned i = 0; i < core2.size(); i++) {
std::cout << core2[i] << "\n";
}
}
关于c++ - 如何使用 z3 split clauses of unsat cores & try to find out unsat core again,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/13270696/
主要思想是将 EF Core nuget 包添加到 .NET Core 库项目,然后在一堆应用程序(例如 ASP.NET Core、Win 服务、控制台应用程序)中使用该库,而无需在每个应用程序中配置
我想要实现的是编写一个简单的.net核心后台工作程序(.net core 3.1)的代码,在该工作程序作为Windows服务运行时,我在其中将数据写入SQL Server数据库(通过EF Core 3
关于 .Net Core SDK download page 二进制文件有什么用?它与安装程序有何不同? 最佳答案 二进制文件是 .NET Core 的编译代码。它们拥有运行 .NET Core 所需
.NET Core 和 Entity Framework Core 之间的区别?我们可以在 .NET Core 中使用 Entity Framework Core 吗?两者都有什么优势? 最佳答案 E
.NET Core 和 ASP.NET Core 到底有什么区别? 它们是相互排斥的吗?我听说 ASP.NET Core 是基于 .NET Core 构建的,但它也可以基于完整的 .NET 框架构建。
我对 ASP.NET Core 开发完全陌生。我正在尝试使用单个模型和 mysql 创建一个简单的 asp.net core Web api 来存储模型数据,然后我想使用 Swagger 将其作为 R
.NET Core 和 Entity Framework Core 之间的区别?我们可以在 .NET Core 中使用 Entity Framework Core 吗?两者都有什么优势? 最佳答案 E
好吧,作为一个新的 .net 开发生态系统,我有点迷失在核心工具、版本等方面。 有人可以解释我之间的区别吗 VS 2015 核心工具预览版 x - See here .NET Core/SDK 与否
我已阅读有关如何通过信号器核心集线器从后台服务向客户端发送通知的文档。如何从客户端接收到后台服务的通知? 后台服务应该只是一个单例。 public class Startup { public
关闭。这个问题是opinion-based .它目前不接受答案。 想改善这个问题吗?更新问题,以便可以通过 editing this post 用事实和引文回答问题. 4年前关闭。 Improve t
非常简单的问题: 我正在尝试创建一个像这样的谓词构建器: var predicate = PredicateBuilder.False(); 但似乎在Net Core和EF Core中不可用。
在 .NET Core 自包含应用程序 中...我们需要在 project.json 中指定运行时 (RID) 我们希望我们的应用程序针对...发布为什么会这样? .NET Core 是跨平台的,与我
如何用 iCloud Core Data 替换我现有的 Core Data?这是我的持久商店协调员: lazy var persistentStoreCoordinator: NSPersistent
关闭。这个问题是opinion-based 。目前不接受答案。 想要改进这个问题吗?更新问题,以便 editing this post 可以用事实和引文来回答它。 . 已关闭 2 年前。 Improv
今天我正在学习新的 ASP.net 核心 API 3.1,我想将我的旧网站从 MVC4 转移到 Web API。除了一件事,一切都很好。数据库连接。在我的旧网站中,我为每个客户端(10/15 数据库)
我在 Visual Studio 2015 Update 3 和 .NET Core 1.0 中工作。我有一个 .NETCoreApp v1.0 类型的 Web API 项目。当我添加一个 .NET
我一直在尝试遵循 Ben Cull ( http://benjii.me/2016/06/entity-framework-core-migrations-for-class-library-proj
当我打开我的 vs 代码程序时,我收到以下消息: 无法找到 .NET Core SDK。 .NET Core 调试将不会启用。确保 .NET Core SDK 已安装并且在路径上。 如果我安装甚至卸载
我偶然发现了一个非常奇怪的问题。每当 Web 应用程序启动时,dotnet.exe 都会使用相当多的内存(大约 300M)。然而,当它触及某些部分时(我感觉这与 EF Core 使用有关),它会在短时
ASP.NET Core Web (.NET Core) 与 ASP.NET Core Web (.NET Framework) 有什么区别? .NET Framework 是否提供 similar
我是一名优秀的程序员,十分优秀!