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

Mode	Name	Size
-rw-r--r--	CMakeLists.txt	1845	log plain
-rw-r--r--	abstract_value.cpp	1153	log plain
-rw-r--r--	abstract_value.h	1768	log plain
-rw-r--r--	bin_heap.h	9299	log plain
-rw-r--r--	bitvector.cpp	9524	log plain
-rw-r--r--	bitvector.h	14391	log plain
-rw-r--r--	bool.h	847	log plain
-rw-r--r--	cardinality.cpp	7075	log plain
-rw-r--r--	cardinality.h	6816	log plain
-rw-r--r--	dense_map.h	8428	log plain
-rw-r--r--	divisible.cpp	929	log plain
-rw-r--r--	divisible.h	1618	log plain
-rw-r--r--	floatingpoint.cpp	23789	log plain
-rw-r--r--	floatingpoint.h	17092	log plain
-rw-r--r--	floatingpoint_literal_symfpu.cpp	10243	log plain
-rw-r--r--	floatingpoint_literal_symfpu.h.in	11515	log plain
-rw-r--r--	floatingpoint_size.cpp	1115	log plain
-rw-r--r--	floatingpoint_size.h	3164	log plain
-rw-r--r--	gmp_util.h	1141	log plain
-rw-r--r--	hash.h	1917	log plain
-rw-r--r--	iand.h	1272	log plain
-rw-r--r--	index.cpp	1345	log plain
-rw-r--r--	index.h	868	log plain
-rw-r--r--	indexed_root_predicate.h	2397	log plain
-rw-r--r--	integer.h.in	1258	log plain
-rw-r--r--	integer_cln_imp.cpp	14297	log plain
-rw-r--r--	integer_cln_imp.h	12598	log plain
-rw-r--r--	integer_gmp_imp.cpp	11932	log plain
-rw-r--r--	integer_gmp_imp.h	11036	log plain
-rw-r--r--	maybe.h	2129	log plain
-rw-r--r--	ostream_util.cpp	917	log plain
-rw-r--r--	ostream_util.h	1345	log plain
-rw-r--r--	poly_util.cpp	10398	log plain
-rw-r--r--	poly_util.h	5492	log plain
-rw-r--r--	random.cpp	1861	log plain
-rw-r--r--	random.h	2039	log plain
-rw-r--r--	rational.h.in	1265	log plain
-rw-r--r--	rational_cln_imp.cpp	2975	log plain
-rw-r--r--	rational_cln_imp.h	9688	log plain
-rw-r--r--	rational_gmp_imp.cpp	2871	log plain
-rw-r--r--	rational_gmp_imp.h	9292	log plain
-rw-r--r--	real_algebraic_number.h.in	887	log plain
-rw-r--r--	real_algebraic_number_poly_imp.cpp	5441	log plain
-rw-r--r--	real_algebraic_number_poly_imp.h	6676	log plain
-rw-r--r--	regexp.cpp	1554	log plain
-rw-r--r--	regexp.h	2081	log plain
-rw-r--r--	resource_manager.cpp	13674	log plain
-rw-r--r--	resource_manager.h	6168	log plain
-rw-r--r--	result.cpp	9714	log plain
-rw-r--r--	result.h	4334	log plain
-rw-r--r--	roundingmode.h	1472	log plain
-rw-r--r--	safe_print.cpp	4952	log plain
-rw-r--r--	safe_print.h	4706	log plain
-rw-r--r--	sampler.cpp	4618	log plain
-rw-r--r--	sampler.h	1652	log plain
-rw-r--r--	sexpr.cpp	11197	log plain
-rw-r--r--	sexpr.h	8645	log plain
-rw-r--r--	smt2_quote_string.cpp	1430	log plain
-rw-r--r--	smt2_quote_string.h	922	log plain
-rw-r--r--	statistics.cpp	3807	log plain
-rw-r--r--	statistics.h	3584	log plain
-rw-r--r--	statistics_registry.cpp	7542	log plain
-rw-r--r--	statistics_registry.h	24896	log plain
-rw-r--r--	string.cpp	12578	log plain
-rw-r--r--	string.h	9661	log plain
-rw-r--r--	tuple.h	1493	log plain
-rw-r--r--	unsafe_interrupt_exception.h	1287	log plain
-rw-r--r--	utility.cpp	1485	log plain
-rw-r--r--	utility.h	2638	log plain