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

Mode	Name	Size
-rw-r--r--	apply_substs.cpp	2768	log plain
-rw-r--r--	apply_substs.h	1452	log plain
-rw-r--r--	apply_to_const.cpp	3444	log plain
-rw-r--r--	apply_to_const.h	1447	log plain
-rw-r--r--	bool_to_bv.cpp	6601	log plain
-rw-r--r--	bool_to_bv.h	1856	log plain
-rw-r--r--	bv_abstraction.cpp	2515	log plain
-rw-r--r--	bv_abstraction.h	1685	log plain
-rw-r--r--	bv_ackermann.cpp	7470	log plain
-rw-r--r--	bv_ackermann.h	2358	log plain
-rw-r--r--	bv_eager_atoms.cpp	1747	log plain
-rw-r--r--	bv_eager_atoms.h	1383	log plain
-rw-r--r--	bv_gauss.cpp	23105	log plain
-rw-r--r--	bv_gauss.h	1707	log plain
-rw-r--r--	bv_intro_pow2.cpp	3022	log plain
-rw-r--r--	bv_intro_pow2.h	1427	log plain
-rw-r--r--	bv_to_bool.cpp	9078	log plain
-rw-r--r--	bv_to_bool.h	2313	log plain
-rw-r--r--	extended_rewriter_pass.cpp	1495	log plain
-rw-r--r--	extended_rewriter_pass.h	1304	log plain
-rw-r--r--	global_negate.cpp	3311	log plain
-rw-r--r--	global_negate.h	1673	log plain
-rw-r--r--	int_to_bv.cpp	10090	log plain
-rw-r--r--	int_to_bv.h	1360	log plain
-rw-r--r--	ite_removal.cpp	1600	log plain
-rw-r--r--	ite_removal.h	1311	log plain
-rw-r--r--	ite_simp.cpp	9005	log plain
-rw-r--r--	ite_simp.h	1449	log plain
-rw-r--r--	miplib_trick.cpp	21998	log plain
-rw-r--r--	miplib_trick.h	1759	log plain
-rw-r--r--	nl_ext_purify.cpp	3836	log plain
-rw-r--r--	nl_ext_purify.h	1665	log plain
-rw-r--r--	non_clausal_simp.cpp	16960	log plain
-rw-r--r--	non_clausal_simp.h	1449	log plain
-rw-r--r--	pseudo_boolean_processor.cpp	10409	log plain
-rw-r--r--	pseudo_boolean_processor.h	3358	log plain
-rw-r--r--	quantifier_macros.cpp	20260	log plain
-rw-r--r--	quantifier_macros.h	3112	log plain
-rw-r--r--	quantifiers_preprocess.cpp	2006	log plain
-rw-r--r--	quantifiers_preprocess.h	1446	log plain
-rw-r--r--	real_to_int.cpp	6597	log plain
-rw-r--r--	real_to_int.h	1488	log plain
-rw-r--r--	rewrite.cpp	1355	log plain
-rw-r--r--	rewrite.h	1233	log plain
-rw-r--r--	sep_skolem_emp.cpp	3750	log plain
-rw-r--r--	sep_skolem_emp.h	1265	log plain
-rw-r--r--	sort_infer.cpp	3022	log plain
-rw-r--r--	sort_infer.h	1474	log plain
-rw-r--r--	static_learning.cpp	1694	log plain
-rw-r--r--	static_learning.h	1240	log plain
-rw-r--r--	sygus_inference.cpp	10055	log plain
-rw-r--r--	sygus_inference.h	2503	log plain
-rw-r--r--	symmetry_breaker.cpp	5783	log plain
-rw-r--r--	symmetry_breaker.h	3499	log plain
-rw-r--r--	symmetry_detect.cpp	40466	log plain
-rw-r--r--	symmetry_detect.h	13190	log plain
-rw-r--r--	synth_rew_rules.cpp	5583	log plain
-rw-r--r--	synth_rew_rules.h	1607	log plain
-rw-r--r--	theory_preprocess.cpp	1723	log plain
-rw-r--r--	theory_preprocess.h	1327	log plain
-rw-r--r--	unconstrained_simplifier.cpp	26041	log plain
-rw-r--r--	unconstrained_simplifier.h	2314	log plain