projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d140a2) | patch
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 10 Mar 2015 14:15:26 +0000 (15:15 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 10 Mar 2015 14:15:26 +0000 (15:15 +0100)
commit10df4ba0752eb23c76b9aa847e3ad116673a47b6
treef41eec3963b7a9d96c0ea85179227d88ae57f0f6tree
parent8d140a28c76095e148acd64e47b5ca0a92ca09becommit | diff
CNF proofs.  Infrastructure for preprocessing proofs.  Updates to smt.plf signature.  Add regressions.
15 files changed:
proofs/signatures/smt.plf diff | blob | history
proofs/signatures/th_base.plf diff | blob | history
src/proof/cnf_proof.cpp diff | blob | history
src/proof/cnf_proof.h diff | blob | history
src/proof/proof_manager.cpp diff | blob | history
src/proof/proof_manager.h diff | blob | history
src/proof/sat_proof.cpp diff | blob | history
src/proof/theory_proof.cpp diff | blob | history
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/regress0/uf/Makefile.am diff | blob | history
test/regress/regress0/uf/cnf-iff-base.smt2 [new file with mode: 0644] blob
test/regress/regress0/uf/cnf-iff.smt2 [new file with mode: 0644] blob
test/regress/regress0/uf/cnf-ite.smt2 [new file with mode: 0644] blob