c3:用C编写的C3，SMTSAT求解器

【文件属性】：
文件名称：c3:用C编写的C3，SMTSAT求解器
文件大小：37KB
文件格式：ZIP
更新时间：2021-05-09 22:41:46
C C3 用C编写的C3，SMT求解器。当前WIP项目... 用法（SAT解算器） C3支持DIMACS文件格式作为SAT求解器的输入。 $ ./c3 -D < DIMACS> 您也可以通过以下命令解决Sudoku 。 $ ./test/sudoku/gen_cnf.sh 用法（SMT求解器） C3还支持SMT-LIB2文件格式作为SMT求解器的输入。 $ ./c3 -S < SMT> 测试 您可以尝试随机测试。 所有表达式都是随机生成的。 $ make test

【文件预览】：
c3-master
----hashmap.c(3KB)
----utils.c(3KB)
----core.c(12KB)
----ordered_map.c(2KB)
----tosat()
--------bitblaster.c(6KB)
----bstree.c(6KB)
----Makefile.common(385B)
----list.c(6KB)
----run_tests.sh(777B)
----LICENSE(11KB)
----test_template.sh(2KB)
----test()
--------simple3.cnf(153B)
--------sort.cnf(73B)
--------simple.cnf(84B)
--------simple2.cnf(147B)
--------sudoku()
--------simple4.cnf(172B)
--------sign-extend.smt2(385B)
--------random()
----parser()
--------smt2.y(16KB)
--------astkind.c(702B)
--------ast.c(5KB)
--------smt2.lex(8KB)
--------parsecnf.c(3KB)
--------Makefile(407B)
----README.md(513B)
----Makefile(599B)
----.gitignore(251B)
----include()
--------c3_hashmap.h(739B)
--------c3_list.h(1KB)
--------tosat()
--------c3_utils.h(465B)
--------parser()
--------c3_core.h(1KB)
--------c3_ordered_map.h(520B)
--------c3_bstree.h(797B)