projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: af86e5a) | patch
This fixes a one definition rule violation for reduceDB_lt in Solver.cc in minisat...
authorTim King <taking@google.com>
Fri, 23 Oct 2015 23:57:48 +0000 (16:57 -0700)
committerTim King <taking@google.com>
Mon, 26 Oct 2015 16:56:58 +0000 (09:56 -0700)
commit918b0fd9ecde048773d245eac66eba9b4306d9d2
tree218d4b5aadbebd440185dc00e4f6589287326b19tree
parentaf86e5a8dc7a64fb5f7b4ca7bd3b2bedf5e8fe32commit | diff
This fixes a one definition rule violation for reduceDB_lt in Solver.cc in minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *.
27 files changed:
src/prop/bvminisat/bvminisat.h diff | blob | history
src/prop/bvminisat/core/Dimacs.h diff | blob | history
src/prop/bvminisat/core/Main.cc diff | blob | history
src/prop/bvminisat/core/Solver.cc diff | blob | history
src/prop/bvminisat/core/Solver.h diff | blob | history
src/prop/bvminisat/core/SolverTypes.h diff | blob | history
src/prop/bvminisat/mtl/Alg.h diff | blob | history
src/prop/bvminisat/mtl/Alloc.h diff | blob | history
src/prop/bvminisat/mtl/Heap.h diff | blob | history
src/prop/bvminisat/mtl/Map.h diff | blob | history
src/prop/bvminisat/mtl/Queue.h diff | blob | history
src/prop/bvminisat/mtl/Sort.h diff | blob | history
src/prop/bvminisat/mtl/Vec.h diff | blob | history
src/prop/bvminisat/mtl/XAlloc.h diff | blob | history
src/prop/bvminisat/simp/Main.cc diff | blob | history
src/prop/bvminisat/simp/SimpSolver.cc diff | blob | history
src/prop/bvminisat/simp/SimpSolver.h diff | blob | history
src/prop/bvminisat/utils/Options.cc diff | blob | history
src/prop/bvminisat/utils/Options.h diff | blob | history
src/prop/bvminisat/utils/ParseUtils.h diff | blob | history
src/prop/bvminisat/utils/System.cc diff | blob | history
src/prop/bvminisat/utils/System.h diff | blob | history
src/prop/minisat/core/Main.cc diff | blob | history
src/prop/minisat/core/Solver.cc diff | blob | history
src/prop/minisat/core/Solver.h diff | blob | history
src/prop/minisat/simp/Main.cc diff | blob | history
src/prop/minisat/simp/SimpSolver.h diff | blob | history