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	11440	log plain
-rw-r--r--	ackermann.h	3223	log plain
-rw-r--r--	apply_substs.cpp	2318	log plain
-rw-r--r--	apply_substs.h	1473	log plain
-rw-r--r--	bool_to_bv.cpp	12464	log plain
-rw-r--r--	bool_to_bv.h	4104	log plain
-rw-r--r--	bv_abstraction.cpp	2325	log plain
-rw-r--r--	bv_abstraction.h	1631	log plain
-rw-r--r--	bv_eager_atoms.cpp	1779	log plain
-rw-r--r--	bv_eager_atoms.h	1334	log plain
-rw-r--r--	bv_gauss.cpp	22777	log plain
-rw-r--r--	bv_gauss.h	3364	log plain
-rw-r--r--	bv_intro_pow2.cpp	3041	log plain
-rw-r--r--	bv_intro_pow2.h	1379	log plain
-rw-r--r--	bv_to_bool.cpp	9146	log plain
-rw-r--r--	bv_to_bool.h	2189	log plain
-rw-r--r--	bv_to_int.cpp	36220	log plain
-rw-r--r--	bv_to_int.h	10283	log plain
-rw-r--r--	extended_rewriter_pass.cpp	1528	log plain
-rw-r--r--	extended_rewriter_pass.h	1267	log plain
-rw-r--r--	foreign_theory_rewrite.cpp	4676	log plain
-rw-r--r--	foreign_theory_rewrite.h	2240	log plain
-rw-r--r--	fun_def_fmf.cpp	15479	log plain
-rw-r--r--	fun_def_fmf.h	3795	log plain
-rw-r--r--	global_negate.cpp	3326	log plain
-rw-r--r--	global_negate.h	1691	log plain
-rw-r--r--	ho_elim.cpp	17499	log plain
-rw-r--r--	ho_elim.h	5898	log plain
-rw-r--r--	int_to_bv.cpp	8052	log plain
-rw-r--r--	int_to_bv.h	1333	log plain
-rw-r--r--	ite_removal.cpp	2751	log plain
-rw-r--r--	ite_removal.h	1163	log plain
-rw-r--r--	ite_simp.cpp	9022	log plain
-rw-r--r--	ite_simp.h	1508	log plain
-rw-r--r--	miplib_trick.cpp	22234	log plain
-rw-r--r--	miplib_trick.h	1751	log plain
-rw-r--r--	nl_ext_purify.cpp	4027	log plain
-rw-r--r--	nl_ext_purify.h	1636	log plain
-rw-r--r--	non_clausal_simp.cpp	17644	log plain
-rw-r--r--	non_clausal_simp.h	3174	log plain
-rw-r--r--	pseudo_boolean_processor.cpp	10392	log plain
-rw-r--r--	pseudo_boolean_processor.h	3287	log plain
-rw-r--r--	quantifier_macros.cpp	20915	log plain
-rw-r--r--	quantifier_macros.h	3479	log plain
-rw-r--r--	quantifiers_preprocess.cpp	2012	log plain
-rw-r--r--	quantifiers_preprocess.h	1401	log plain
-rw-r--r--	real_to_int.cpp	7296	log plain
-rw-r--r--	real_to_int.h	1437	log plain
-rw-r--r--	rewrite.cpp	1334	log plain
-rw-r--r--	rewrite.h	1210	log plain
-rw-r--r--	sep_skolem_emp.cpp	3763	log plain
-rw-r--r--	sep_skolem_emp.h	1201	log plain
-rw-r--r--	sort_infer.cpp	3133	log plain
-rw-r--r--	sort_infer.h	1391	log plain
-rw-r--r--	static_learning.cpp	1824	log plain
-rw-r--r--	static_learning.h	1207	log plain
-rw-r--r--	strings_eager_pp.cpp	1886	log plain
-rw-r--r--	strings_eager_pp.h	1319	log plain
-rw-r--r--	sygus_inference.cpp	10783	log plain
-rw-r--r--	sygus_inference.h	2447	log plain
-rw-r--r--	synth_rew_rules.cpp	17584	log plain
-rw-r--r--	synth_rew_rules.h	3169	log plain
-rw-r--r--	theory_preprocess.cpp	2570	log plain
-rw-r--r--	theory_preprocess.h	1277	log plain
-rw-r--r--	theory_rewrite_eq.cpp	3573	log plain
-rw-r--r--	theory_rewrite_eq.h	1888	log plain
-rw-r--r--	unconstrained_simplifier.cpp	27428	log plain
-rw-r--r--	unconstrained_simplifier.h	2397	log plain