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--	ackermann.cpp	11301	log plain
-rw-r--r--	ackermann.h	3212	log plain
-rw-r--r--	apply_substs.cpp	2306	log plain
-rw-r--r--	apply_substs.h	1459	log plain
-rw-r--r--	bool_to_bv.cpp	12447	log plain
-rw-r--r--	bool_to_bv.h	4085	log plain
-rw-r--r--	bv_abstraction.cpp	2289	log plain
-rw-r--r--	bv_abstraction.h	1624	log plain
-rw-r--r--	bv_eager_atoms.cpp	1769	log plain
-rw-r--r--	bv_eager_atoms.h	1322	log plain
-rw-r--r--	bv_gauss.cpp	22763	log plain
-rw-r--r--	bv_gauss.h	3346	log plain
-rw-r--r--	bv_intro_pow2.cpp	3016	log plain
-rw-r--r--	bv_intro_pow2.h	1366	log plain
-rw-r--r--	bv_to_bool.cpp	9200	log plain
-rw-r--r--	bv_to_bool.h	2243	log plain
-rw-r--r--	bv_to_int.cpp	36058	log plain
-rw-r--r--	bv_to_int.h	10314	log plain
-rw-r--r--	extended_rewriter_pass.cpp	1523	log plain
-rw-r--r--	extended_rewriter_pass.h	1260	log plain
-rw-r--r--	foreign_theory_rewrite.cpp	4642	log plain
-rw-r--r--	foreign_theory_rewrite.h	2234	log plain
-rw-r--r--	fun_def_fmf.cpp	15381	log plain
-rw-r--r--	fun_def_fmf.h	3776	log plain
-rw-r--r--	global_negate.cpp	3297	log plain
-rw-r--r--	global_negate.h	1683	log plain
-rw-r--r--	ho_elim.cpp	17295	log plain
-rw-r--r--	ho_elim.h	5877	log plain
-rw-r--r--	int_to_bv.cpp	7945	log plain
-rw-r--r--	int_to_bv.h	1316	log plain
-rw-r--r--	ite_removal.cpp	2737	log plain
-rw-r--r--	ite_removal.h	1218	log plain
-rw-r--r--	ite_simp.cpp	9003	log plain
-rw-r--r--	ite_simp.h	1487	log plain
-rw-r--r--	miplib_trick.cpp	22135	log plain
-rw-r--r--	miplib_trick.h	1737	log plain
-rw-r--r--	nl_ext_purify.cpp	3900	log plain
-rw-r--r--	nl_ext_purify.h	1621	log plain
-rw-r--r--	non_clausal_simp.cpp	17635	log plain
-rw-r--r--	non_clausal_simp.h	3161	log plain
-rw-r--r--	pseudo_boolean_processor.cpp	10378	log plain
-rw-r--r--	pseudo_boolean_processor.h	3285	log plain
-rw-r--r--	quantifier_macros.cpp	20686	log plain
-rw-r--r--	quantifier_macros.h	3466	log plain
-rw-r--r--	quantifiers_preprocess.cpp	2015	log plain
-rw-r--r--	quantifiers_preprocess.h	1402	log plain
-rw-r--r--	real_to_int.cpp	7205	log plain
-rw-r--r--	real_to_int.h	1419	log plain
-rw-r--r--	rewrite.cpp	1300	log plain
-rw-r--r--	rewrite.h	1189	log plain
-rw-r--r--	sep_skolem_emp.cpp	3760	log plain
-rw-r--r--	sep_skolem_emp.h	1189	log plain
-rw-r--r--	sort_infer.cpp	3115	log plain
-rw-r--r--	sort_infer.h	1371	log plain
-rw-r--r--	static_learning.cpp	1815	log plain
-rw-r--r--	static_learning.h	1196	log plain
-rw-r--r--	strings_eager_pp.cpp	1860	log plain
-rw-r--r--	strings_eager_pp.h	1305	log plain
-rw-r--r--	sygus_inference.cpp	10772	log plain
-rw-r--r--	sygus_inference.h	2432	log plain
-rw-r--r--	synth_rew_rules.cpp	17559	log plain
-rw-r--r--	synth_rew_rules.h	3156	log plain
-rw-r--r--	theory_preprocess.cpp	2561	log plain
-rw-r--r--	theory_preprocess.h	1266	log plain
-rw-r--r--	theory_rewrite_eq.cpp	3548	log plain
-rw-r--r--	theory_rewrite_eq.h	1875	log plain
-rw-r--r--	unconstrained_simplifier.cpp	27344	log plain
-rw-r--r--	unconstrained_simplifier.h	2396	log plain