signatures:CVC4的证明签名

【文件属性】：

文件名称：signatures:CVC4的证明签名

文件大小：102KB

文件格式：ZIP

更新时间：2024-05-03 22:56:30

Lean

证明签名 该存储库包含CVC4的证明签名。 测验 测试LFSC签名 运行测试 make test运行所有LFSC测试。 make 运行单个测试，例如make drat_test 。 添加新的签名测试 要添加新的签名测试文件，请在test/lfsc创建一个新文件，并将其添加到git中，例如： git add test/lfsc/new_signature_test.plf LFSC_TESTS其添加到根目录的中的LFSC_TESTS变量中，并声明测试的依赖性，如下所述。 测试可以使用来声明它们依赖的签名文件; Deps: ; Deps:伪指令，后跟一个用空格分隔的文件列表。 例如： ; Deps: sat.plf smt.plf 表示测试取决于sat.plf和smt.plf 。 运行脚本会自动搜索lfsc列出的文件以及测试输入的目录。

【文件预览】：
signatures-master
----.github()
--------workflows()
----lean()
--------examples.lean(1KB)
--------euf.lean(1KB)
--------reordering.lean(2KB)
--------bv.lean(10KB)
--------examplesQuant.lean(740B)
--------leanpkg.toml(234B)
--------term.lean(14KB)
--------cdclt.lean(10KB)
--------README.md(559B)
--------leanpkg.path(53B)
--------quant.lean(929B)
--------exampleEUF.lean(3KB)
--------aux.lean(2KB)
----contrib()
--------get-lfsc-checker(1KB)
----doc()
--------bv()
----lfsc()
--------old()
--------new()
----lean4()
--------Cdclt()
--------leanpkg.toml(93B)
--------Cdclt.lean(51B)
--------README.md(452B)
--------leanpkg.path(21B)
----test()
--------lfsc()
----README.md(927B)
----.gitignore(85B)