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	2139	log plain
-rw-r--r--	abstract_value.cpp	1123	log plain
-rw-r--r--	abstract_value.h	1723	log plain
-rw-r--r--	bin_heap.h	9762	log plain
-rw-r--r--	bitvector.cpp	9456	log plain
-rw-r--r--	bitvector.h	14292	log plain
-rw-r--r--	bool.h	835	log plain
-rw-r--r--	cardinality.cpp	7088	log plain
-rw-r--r--	cardinality.h	6760	log plain
-rw-r--r--	cardinality_class.cpp	1874	log plain
-rw-r--r--	cardinality_class.h	3247	log plain
-rw-r--r--	dense_map.h	8433	log plain
-rw-r--r--	didyoumean.cpp	4229	log plain
-rw-r--r--	didyoumean.h	1420	log plain
-rw-r--r--	divisible.cpp	943	log plain
-rw-r--r--	divisible.h	1599	log plain
-rw-r--r--	floatingpoint.cpp	15600	log plain
-rw-r--r--	floatingpoint.h	17227	log plain
-rw-r--r--	floatingpoint_literal_symfpu.cpp	11156	log plain
-rw-r--r--	floatingpoint_literal_symfpu.h	8802	log plain
-rw-r--r--	floatingpoint_literal_symfpu_traits.cpp	9856	log plain
-rw-r--r--	floatingpoint_literal_symfpu_traits.h	9584	log plain
-rw-r--r--	floatingpoint_size.cpp	1124	log plain
-rw-r--r--	floatingpoint_size.h	3134	log plain
-rw-r--r--	gmp_util.h	1158	log plain
-rw-r--r--	hash.h	1985	log plain
-rw-r--r--	iand.h	1310	log plain
-rw-r--r--	index.cpp	1298	log plain
-rw-r--r--	index.h	835	log plain
-rw-r--r--	indexed_root_predicate.h	2338	log plain
-rw-r--r--	integer.h.in	1095	log plain
-rw-r--r--	integer_cln_imp.cpp	15556	log plain
-rw-r--r--	integer_cln_imp.h	12489	log plain
-rw-r--r--	integer_gmp_imp.cpp	13255	log plain
-rw-r--r--	integer_gmp_imp.h	10908	log plain
-rw-r--r--	ostream_util.cpp	894	log plain
-rw-r--r--	ostream_util.h	1324	log plain
-rw-r--r--	poly_util.cpp	10083	log plain
-rw-r--r--	poly_util.h	5181	log plain
-rw-r--r--	random.cpp	1864	log plain
-rw-r--r--	random.h	2025	log plain
-rw-r--r--	rational.h.in	1098	log plain
-rw-r--r--	rational_cln_imp.cpp	4218	log plain
-rw-r--r--	rational_cln_imp.h	8591	log plain
-rw-r--r--	rational_gmp_imp.cpp	2851	log plain
-rw-r--r--	rational_gmp_imp.h	9307	log plain
-rw-r--r--	real_algebraic_number.h.in	852	log plain
-rw-r--r--	real_algebraic_number_poly_imp.cpp	5384	log plain
-rw-r--r--	real_algebraic_number_poly_imp.h	6131	log plain
-rw-r--r--	regexp.cpp	1575	log plain
-rw-r--r--	regexp.h	2061	log plain
-rw-r--r--	resource_manager.cpp	9127	log plain
-rw-r--r--	resource_manager.h	6009	log plain
-rw-r--r--	result.cpp	9564	log plain
-rw-r--r--	result.h	4015	log plain
-rw-r--r--	roundingmode.cpp	1295	log plain
-rw-r--r--	roundingmode.h	1558	log plain
-rw-r--r--	safe_print.cpp	4961	log plain
-rw-r--r--	safe_print.h	4858	log plain
-rw-r--r--	sampler.cpp	4635	log plain
-rw-r--r--	sampler.h	1671	log plain
-rw-r--r--	sexpr.cpp	1236	log plain
-rw-r--r--	sexpr.h	3505	log plain
-rw-r--r--	smt2_quote_string.cpp	1665	log plain
-rw-r--r--	smt2_quote_string.h	975	log plain
-rw-r--r--	statistics_public.cpp	1722	log plain
-rw-r--r--	statistics_public.h	899	log plain
-rw-r--r--	statistics_registry.cpp	4385	log plain
-rw-r--r--	statistics_registry.h	9360	log plain
-rw-r--r--	statistics_stats.cpp	2842	log plain
-rw-r--r--	statistics_stats.h	10305	log plain
-rw-r--r--	statistics_value.cpp	3328	log plain
-rw-r--r--	statistics_value.h	9880	log plain
-rw-r--r--	string.cpp	13054	log plain
-rw-r--r--	string.h	9723	log plain
-rw-r--r--	unsafe_interrupt_exception.h	1330	log plain
-rw-r--r--	utility.cpp	1444	log plain
-rw-r--r--	utility.h	3010	log plain