Solver « cryptominisat « prop « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	BitArray.h	3913	log plain
-rw-r--r--	BothCache.cpp	3941	log plain
-rw-r--r--	BothCache.h	236	log plain
-rw-r--r--	BoundedQueue.h	2826	log plain
-rw-r--r--	CSet.h	5818	log plain
-rw-r--r--	Clause.h	7459	log plain
-rw-r--r--	ClauseAllocator.cpp	19307	log plain
-rw-r--r--	ClauseAllocator.h	5297	log plain
-rw-r--r--	ClauseCleaner.cpp	7997	log plain
-rw-r--r--	ClauseCleaner.h	3219	log plain
-rw-r--r--	ClauseOffset.h	211	log plain
-rw-r--r--	ClauseVivifier.cpp	11608	log plain
-rw-r--r--	ClauseVivifier.h	1831	log plain
-rw-r--r--	CompleteDetachReattacher.cpp	5502	log plain
-rw-r--r--	CompleteDetachReattacher.h	2760	log plain
-rw-r--r--	DataSync.cpp	6754	log plain
-rw-r--r--	DataSync.h	2711	log plain
-rw-r--r--	DimacsParser.cpp	13621	log plain
-rw-r--r--	DimacsParser.h	2802	log plain
-rw-r--r--	DoublePackedRow.h	5306	log plain
-rw-r--r--	FailedLitSearcher.cpp	26712	log plain
-rw-r--r--	FailedLitSearcher.h	8659	log plain
-rw-r--r--	Gaussian.cpp	38012	log plain
-rw-r--r--	Gaussian.h	9488	log plain
-rw-r--r--	GaussianConfig.h	2001	log plain
-rw-r--r--	Main.cpp	40579	log plain
-rw-r--r--	Main.h	1809	log plain
-rw-r--r--	Makefile.am	1531	log plain
-rw-r--r--	Makefile.in	24098	log plain
-rw-r--r--	MatrixFinder.cpp	8943	log plain
-rw-r--r--	MatrixFinder.h	1954	log plain
-rw-r--r--	OnlyNonLearntBins.cpp	2724	log plain
-rw-r--r--	OnlyNonLearntBins.h	2058	log plain
-rw-r--r--	PackedMatrix.h	5000	log plain
-rw-r--r--	PackedRow.cpp	3096	log plain
-rw-r--r--	PackedRow.h	5960	log plain
-rw-r--r--	PropBy.h	6043	log plain
-rw-r--r--	RestartTypeChooser.cpp	5700	log plain
-rw-r--r--	RestartTypeChooser.h	2649	log plain
-rw-r--r--	SCCFinder.cpp	5238	log plain
-rw-r--r--	SCCFinder.h	2121	log plain
-rw-r--r--	SharedData.h	1073	log plain
-rw-r--r--	Solver.cpp	97718	log plain
-rw-r--r--	Solver.h	35906	log plain
-rw-r--r--	SolverConf.cpp	3157	log plain
-rw-r--r--	SolverConf.h	7980	log plain
-rw-r--r--	SolverDebug.cpp	8075	log plain
-rw-r--r--	SolverMisc.cpp	26697	log plain
-rw-r--r--	SolverTypes.h	5986	log plain
-rw-r--r--	StateSaver.cpp	2027	log plain
-rw-r--r--	StateSaver.h	1371	log plain
-rw-r--r--	StreamBuffer.h	2467	log plain
-rw-r--r--	Subsumer.cpp	67289	log plain
-rw-r--r--	Subsumer.h	15898	log plain
-rw-r--r--	UselessBinRemover.cpp	7947	log plain
-rw-r--r--	UselessBinRemover.h	3149	log plain
-rw-r--r--	VarReplacer.cpp	23282	log plain
-rw-r--r--	VarReplacer.h	4782	log plain
-rw-r--r--	Watched.h	7064	log plain
-rw-r--r--	XSet.h	3663	log plain
-rw-r--r--	XorFinder.cpp	14071	log plain
-rw-r--r--	XorFinder.h	5356	log plain
-rw-r--r--	XorSubsumer.cpp	19840	log plain
-rw-r--r--	XorSubsumer.h	5127	log plain
-rw-r--r--	constants.h	3897	log plain
d---------	msvc	36	log plain
-rw-r--r--	time_mem.h	2914	log plain