git.libre-soc.org Git - cvc5.git/commit

author	Haniel Barbosa <hanielbbarbosa@gmail.com>
	Thu, 20 May 2021 18:29:32 +0000 (15:29 -0300)
committer	GitHub <noreply@github.com>
	Thu, 20 May 2021 18:29:32 +0000 (18:29 +0000)
commit	a0644780130dd0ed86a9486e29aa326b3fe5d804
tree	8cd1f0e0b18e67fa91dfff48eac5204eaf4ee3fc	tree
parent	61b14cbbbb1665496913e047d14fedee610efef1	commit \| diff

Remove old unsat cores (#6581)

This commit removes the remaining old proof code and the code to produce unsat cores based on it.

35 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.cpp		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/proof/cnf_proof.cpp	[deleted file]	blob \| history
src/proof/cnf_proof.h	[deleted file]	blob \| history
src/proof/proof_manager.cpp	[deleted file]	blob \| history
src/proof/proof_manager.h	[deleted file]	blob \| history
src/proof/sat_proof.h	[deleted file]	blob \| history
src/proof/sat_proof_implementation.h	[deleted file]	blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/core/SolverTypes.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_engine_scope.cpp		diff \| blob \| history
src/smt/smt_engine_scope.h		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_macros.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history

RSS Atom