git.unchartedbackwaters.co.uk Git - francis/stp.git/commit

]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit

author	trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
	Fri, 20 Aug 2010 12:07:42 +0000 (12:07 +0000)
committer	trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
	Fri, 20 Aug 2010 12:07:42 +0000 (12:07 +0000)
commit	6658ff2018f070628582b738710422c656723789
tree	3279d9fdaf97ceecb38be8154d5be995059b3016	tree \| snapshot
parent	e4c1fb7756e8219987330c848cd67edfa458e5dd	commit \| diff

* Replace minisat 2 with minisat 2.2.
* Replace simplifying-minisat 2 with simplifying-minisat 2.2
* It's no longer necessary to compile cryptominisat separately. The choice of solver is controlled by a command line flag now.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@992 e59a4935-1847-0410-ae03-e826735625c1

55 files changed:

scripts/Makefile.common		diff \| blob \| history
scripts/Makefile.in		diff \| blob \| history
src/AST/ASTSymbol.cpp		diff \| blob \| history
src/AST/UsefulDefs.h		diff \| blob \| history
src/STPManager/STP.cpp		diff \| blob \| history
src/STPManager/STP.h		diff \| blob \| history
src/STPManager/STPManager.cpp		diff \| blob \| history
src/STPManager/STPManager.h		diff \| blob \| history
src/STPManager/UserDefinedFlags.h		diff \| blob \| history
src/absrefine_counterexample/AbsRefine_CounterExample.h		diff \| blob \| history
src/absrefine_counterexample/AbstractionRefinement.cpp		diff \| blob \| history
src/absrefine_counterexample/CounterExample.cpp		diff \| blob \| history
src/absrefine_counterexample/Makefile		diff \| blob \| history
src/main/Globals.h		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/printer/AssortedPrinters.cpp		diff \| blob \| history
src/sat/CryptoMinisat.cpp	[new file with mode: 0644]	blob
src/sat/CryptoMinisat.h	[new file with mode: 0644]	blob
src/sat/Makefile		diff \| blob \| history
src/sat/MinisatCore.cpp	[new file with mode: 0644]	blob
src/sat/MinisatCore.h	[new file with mode: 0644]	blob
src/sat/SATSolver.h	[new file with mode: 0644]	blob
src/sat/SimplifyingMinisat.cpp	[new file with mode: 0644]	blob
src/sat/SimplifyingMinisat.h	[new file with mode: 0644]	blob
src/sat/core/Dimacs.h	[new file with mode: 0644]	blob
src/sat/core/Main.cc	[new file with mode: 0644]	blob
src/sat/core/Makefile		diff \| blob \| history
src/sat/core/Solver.C	[deleted file]	blob \| history
src/sat/core/Solver.cc	[new file with mode: 0644]	blob
src/sat/core/Solver.h		diff \| blob \| history
src/sat/core/SolverTypes.h		diff \| blob \| history
src/sat/mtl/Alg.h		diff \| blob \| history
src/sat/mtl/Alloc.h	[new file with mode: 0644]	blob
src/sat/mtl/BasicHeap.h		diff \| blob \| history
src/sat/mtl/BoxedVec.h		diff \| blob \| history
src/sat/mtl/Heap.h		diff \| blob \| history
src/sat/mtl/IntTypes.h	[new file with mode: 0644]	blob
src/sat/mtl/Map.h		diff \| blob \| history
src/sat/mtl/Queue.h		diff \| blob \| history
src/sat/mtl/Sort.h		diff \| blob \| history
src/sat/mtl/Vec.h		diff \| blob \| history
src/sat/mtl/XAlloc.h	[new file with mode: 0644]	blob
src/sat/mtl/template.mk	[new file with mode: 0644]	blob
src/sat/sat.h	[deleted file]	blob \| history
src/sat/simp/Main.cc	[new file with mode: 0644]	blob
src/sat/simp/Makefile		diff \| blob \| history
src/sat/simp/SimpSolver.C	[deleted file]	blob \| history
src/sat/simp/SimpSolver.cc	[new file with mode: 0644]	blob
src/sat/simp/SimpSolver.h		diff \| blob \| history
src/to-sat/AIG/ToSATAIG.cpp		diff \| blob \| history
src/to-sat/AIG/ToSATAIG.h		diff \| blob \| history
src/to-sat/ToCNF.cpp		diff \| blob \| history
src/to-sat/ToSAT.cpp		diff \| blob \| history
src/to-sat/ToSAT.h		diff \| blob \| history
src/to-sat/ToSATBase.h		diff \| blob \| history

STP Constraint Solver.

RSS Atom