projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4d9caf9) | patch
First attempt at incorporating LFSC proof checker into CVC4.
authorMorgan Deters <mdeters@cs.nyu.edu>
Thu, 12 Dec 2013 23:24:54 +0000 (18:24 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Tue, 17 Dec 2013 03:28:26 +0000 (22:28 -0500)
commit5186ca79710fe935d1f7ed27c4a34e913ab547e8
tree4f5ce4957063085f607492a6474b0d244e4b2da4tree
parent4d9caf9782c59823fb95519b9b518b7d7f89738acommit | diff
First attempt at incorporating LFSC proof checker into CVC4.
38 files changed:
.travis.yml diff | blob | history
COPYING diff | blob | history
Makefile.am diff | blob | history
Makefile.builds.in diff | blob | history
NEWS diff | blob | history
configure.ac diff | blob | history
proofs/lfsc_checker/.gitignore [new file with mode: 0644] blob
proofs/lfsc_checker/AUTHORS [new file with mode: 0644] blob
proofs/lfsc_checker/COPYING [new file with mode: 0644] blob
proofs/lfsc_checker/INSTALL [new file with mode: 0644] blob
proofs/lfsc_checker/Makefile.am [new file with mode: 0644] blob
proofs/lfsc_checker/NEWS [new file with mode: 0644] blob
proofs/lfsc_checker/README [new file with mode: 0644] blob
proofs/lfsc_checker/check.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/check.h [new file with mode: 0644] blob
proofs/lfsc_checker/chunking_memory_management.h [new file with mode: 0644] blob
proofs/lfsc_checker/code.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/code.h [new file with mode: 0644] blob
proofs/lfsc_checker/configure.ac [new file with mode: 0644] blob
proofs/lfsc_checker/expr.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/expr.h [new file with mode: 0644] blob
proofs/lfsc_checker/libwriter.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/libwriter.h [new file with mode: 0644] blob
proofs/lfsc_checker/main.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/position.h [new file with mode: 0644] blob
proofs/lfsc_checker/print_smt2.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/print_smt2.h [new file with mode: 0644] blob
proofs/lfsc_checker/scccode.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/scccode.h [new file with mode: 0644] blob
proofs/lfsc_checker/sccwriter.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/sccwriter.h [new file with mode: 0644] blob
proofs/lfsc_checker/trie.cpp [new file with mode: 0644] blob
proofs/lfsc_checker/trie.h [new file with mode: 0644] blob
src/Makefile.am diff | blob | history
src/smt/options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/smt_engine_check_proof.cpp [new file with mode: 0644] blob