SMT求解器Q3B——在WSL上的Docker配置

SMT求解器Q3B——在WSL上的Docker配置

  • 1、配置wsl下的Docker
  • 2、在github上下载Q3B
  • 3、更换配置文件
  • 4、安装docker镜像
  • 5、运行Docker容器
  • 6、编译Q3B
  • 7、使用Q3B

1、配置wsl下的Docker

WSL 2 上的 Docker 远程容器入门

2、在github上下载Q3B

Q3B下载地址

3、更换配置文件

下载完后,将如下文件更换为smtlibv2-grammar

Q3B文件目录

4、安装docker镜像

进入Q3B的安装目录,执行如下命令

docker build -t q3b:v1 .

其中,q3b为容器名称,v1为target

5、运行Docker容器

docker run -t -i q3b:v1

-i: 交互式操作。
-t: 终端。

6、编译Q3B

事实上,如果使用DockerFile构造的容器,那么这一步完全不必。

mkdir build
cd build
cmake ..
make

7、使用Q3B

进入build文件夹下,测试文件在Q3B/tests/data下提供。

./q3b file.smt2

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.hqwc.cn/news/130067.html

如若内容造成侵权/违法违规/事实不符,请联系编程知识网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

【SpringMVC篇】详解SpringMVC入门案例

🎊专栏【SpringMVC】 🍔喜欢的诗句:天行健,君子以自强不息。 🎆音乐分享【如愿】 🎄欢迎并且感谢大家指出小吉的问题🥰 文章目录 🎍SpringMVC简介⭐优点 🌺SpringMVC入门…

详解TCP三次握手(建立连接)和四次握手(释放连接)

VC常用功能开发汇总(专栏文章列表,欢迎订阅,持续更新...)https://blog.csdn.net/chenlycly/article/details/124272585C软件异常排查从入门到精通系列教程(专栏文章列表,欢迎订阅,持续更新...&a…

Typora-Drake主题

关于Typora-Drake主题的小调整 下载安装 下载地址:Drake (typora.io) 点击下载跳转GitHub,下载该主题 下载完成安装主题 打开主题文件夹,把下载的zip全部加压丢进去重启Typora Drake主题样式小调整 打开主题文件夹,找到Drake.css文件&am…

多线程 - 线程池

线程池 相关的背景知识 线程池存在的意义: 使用进程来实现并发编程,效率太低了,任务太重了,为了提高效率,此时就引入了线程,线程也叫做“轻量级进程”,创建线程比创建进程更高效;销毁线程比销毁进程更高效;调度线程比调度进程更高效…此时,使用多线程就可以在很多时候代替进程…

HomeView/主页 的实现

1. 创建数据模型 1.1 创建货币模型 CoinModel.swift import Foundation// GoinGecko API info /*URL:https://api.coingecko.com/api/v3/coins/markets?vs_currencyusd&ordermarket_cap_desc&per_page250&page1&sparklinetrue&price_change_percentage24…

2023中考满分多少 中考总分数展示

中考总分根据地区而不同,以下是各地区总分数展示: 大部分地区的中考总分为750分,包括语文150分、数学150分、英语150分(其中听力测试30分)、思想品德与历史合卷共150分,物理与化学合卷共150分。 安徽中考…

Qt打开ui文件经常报错

报错如下: 解决方法: 最后设置成默认值 即可

强化学习------Qlearning算法

简介 Q learning 算法是一种value-based的强化学习算法,Q是quality的缩写,Q函数 Q(state,action)表示在状态state下执行动作action的quality, 也就是能获得的Q value是多少。算法的目标是最大化Q值,通过在状态state下…

基于三平面映射的地形纹理化【Triplanar Mapping】

你可能遇到过这样的地形:悬崖陡峭的一侧的纹理拉伸得如此之大,以至于看起来不切实际。 也许你有一个程序化生成的世界,你无法对其进行 UV 展开和纹理处理。 推荐:用 NSDT编辑器 快速搭建可编程3D场景 三平面映射(Trip…

【可视化大屏】用该软件,无代码,更易用

奥威BI系统是一种自助式BI数据可视化工具,它可以在无代码的情况下,通过简单的拖拉拽实现数据可视化,并支持多种数据源接入,包括各类数据库、Excel、API接口等,只需简单的输入数据源连接地址即可,操作非常方…

[UE虚幻引擎] DTCopyFile 插件说明 – 使用蓝图拷贝复制文件 (Windows)

本插件可以在虚幻引擎中使用蓝图对系统的其他文件进行拷贝复制操作。 1. 节点说明 Async Copy File ​ 异步复制文件 Param Source File : 要复制的源文件的完整路径。Param Target File : 要复制的目标文件的完整路径。Param Force Copy : 如果为true,则如果目标…

大模型部署手记(13)LLaMa2+Chinese-LLaMA-Plus-2-7B+Windows+LangChain+摘要问答

1.简介: 组织机构:Meta(Facebook) 代码仓:GitHub - facebookresearch/llama: Inference code for LLaMA models 模型:chinese-alpaca-2-7b-hf、text2vec-large-chinese 下载:使用百度网盘和…