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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Mon, 1 Nov 2021 20:59:47 +0000 (13:59 -0700)
committer	GitHub <noreply@github.com>
	Mon, 1 Nov 2021 20:59:47 +0000 (20:59 +0000)
commit	9cae42243a4c0be14fd72f5379ee4eb9f4bc88e9
tree	0a9cfac9b3ec68737955d3b05c3ae69088eeaa7b	tree
parent	77416fa5f7cd004bbec3fb4901f47908d1e8fdd4	commit \| diff

bv: Remove layered solver. (#7455)

This commit removes the old bit-vector solver code.

83 files changed:

CMakeLists.txt		diff \| blob \| history
INSTALL.rst		diff \| blob \| history
cmake/FindABC.cmake	[deleted file]	blob \| history
configure.sh		diff \| blob \| history
contrib/get-abc	[deleted file]	blob \| history
src/CMakeLists.txt		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/configuration_private.h		diff \| blob \| history
src/options/bv_options.toml		diff \| blob \| history
src/options/didyoumean_test.cpp	[new file with mode: 0644]	blob
src/options/options_handler.cpp		diff \| blob \| history
src/preprocessing/passes/bv_abstraction.cpp	[deleted file]	blob \| history
src/preprocessing/passes/bv_abstraction.h	[deleted file]	blob \| history
src/preprocessing/preprocessing_pass_registry.cpp		diff \| blob \| history
src/prop/bv_sat_solver_notify.h	[deleted file]	blob \| history
src/prop/bvminisat/LICENSE	[deleted file]	blob \| history
src/prop/bvminisat/README	[deleted file]	blob \| history
src/prop/bvminisat/bvminisat.cpp	[deleted file]	blob \| history
src/prop/bvminisat/bvminisat.h	[deleted file]	blob \| history
src/prop/bvminisat/core/Dimacs.h	[deleted file]	blob \| history
src/prop/bvminisat/core/Solver.cc	[deleted file]	blob \| history
src/prop/bvminisat/core/Solver.h	[deleted file]	blob \| history
src/prop/bvminisat/core/SolverTypes.h	[deleted file]	blob \| history
src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Alg.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Alloc.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Heap.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/IntTypes.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Map.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Queue.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Sort.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/Vec.h	[deleted file]	blob \| history
src/prop/bvminisat/mtl/XAlloc.h	[deleted file]	blob \| history
src/prop/bvminisat/simp/SimpSolver.cc	[deleted file]	blob \| history
src/prop/bvminisat/simp/SimpSolver.h	[deleted file]	blob \| history
src/prop/bvminisat/utils/Options.cc	[deleted file]	blob \| history
src/prop/bvminisat/utils/Options.h	[deleted file]	blob \| history
src/prop/bvminisat/utils/ParseUtils.h	[deleted file]	blob \| history
src/prop/bvminisat/utils/System.cc	[deleted file]	blob \| history
src/prop/bvminisat/utils/System.h	[deleted file]	blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp	[deleted file]	blob \| history
src/theory/bv/abstraction.h	[deleted file]	blob \| history
src/theory/bv/bitblast/aig_bitblaster.cpp	[deleted file]	blob \| history
src/theory/bv/bitblast/aig_bitblaster.h	[deleted file]	blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp	[deleted file]	blob \| history
src/theory/bv/bitblast/eager_bitblaster.h	[deleted file]	blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp	[deleted file]	blob \| history
src/theory/bv/bitblast/lazy_bitblaster.h	[deleted file]	blob \| history
src/theory/bv/bv_eager_solver.cpp	[deleted file]	blob \| history
src/theory/bv/bv_eager_solver.h	[deleted file]	blob \| history
src/theory/bv/bv_inequality_graph.cpp	[deleted file]	blob \| history
src/theory/bv/bv_inequality_graph.h	[deleted file]	blob \| history
src/theory/bv/bv_quick_check.cpp	[deleted file]	blob \| history
src/theory/bv/bv_quick_check.h	[deleted file]	blob \| history
src/theory/bv/bv_solver.h		diff \| blob \| history
src/theory/bv/bv_solver_layered.cpp	[deleted file]	blob \| history
src/theory/bv/bv_solver_layered.h	[deleted file]	blob \| history
src/theory/bv/bv_subtheory.h	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_algebraic.h	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_bitblast.h	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_core.cpp	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_core.h	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_inequality.cpp	[deleted file]	blob \| history
src/theory/bv/bv_subtheory_inequality.h	[deleted file]	blob \| history
src/theory/bv/slicer.cpp	[deleted file]	blob \| history
src/theory/bv/slicer.h	[deleted file]	blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/bv/bv-abstr-bug.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/test-bv_intro_pow2.smt2		diff \| blob \| history
test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2		diff \| blob \| history
test/regress/regress1/bv/test-bv-abstraction.smt2	[deleted file]	blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history

RSS Atom