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	11194	log plain
-rw-r--r--	ackermann.h	3200	log plain
-rw-r--r--	apply_substs.cpp	2207	log plain
-rw-r--r--	apply_substs.h	1464	log plain
-rw-r--r--	bool_to_bv.cpp	12310	log plain
-rw-r--r--	bool_to_bv.h	4155	log plain
-rw-r--r--	bv_abstraction.cpp	2408	log plain
-rw-r--r--	bv_abstraction.h	1678	log plain
-rw-r--r--	bv_eager_atoms.cpp	1636	log plain
-rw-r--r--	bv_eager_atoms.h	1376	log plain
-rw-r--r--	bv_gauss.cpp	22680	log plain
-rw-r--r--	bv_gauss.h	3377	log plain
-rw-r--r--	bv_intro_pow2.cpp	2929	log plain
-rw-r--r--	bv_intro_pow2.h	1420	log plain
-rw-r--r--	bv_to_bool.cpp	9055	log plain
-rw-r--r--	bv_to_bool.h	2313	log plain
-rw-r--r--	bv_to_int.cpp	36657	log plain
-rw-r--r--	bv_to_int.h	10349	log plain
-rw-r--r--	extended_rewriter_pass.cpp	1423	log plain
-rw-r--r--	extended_rewriter_pass.h	1314	log plain
-rw-r--r--	foreign_theory_rewrite.cpp	4515	log plain
-rw-r--r--	foreign_theory_rewrite.h	2300	log plain
-rw-r--r--	fun_def_fmf.cpp	15232	log plain
-rw-r--r--	fun_def_fmf.h	3820	log plain
-rw-r--r--	global_negate.cpp	3251	log plain
-rw-r--r--	global_negate.h	1701	log plain
-rw-r--r--	ho_elim.cpp	17229	log plain
-rw-r--r--	ho_elim.h	5842	log plain
-rw-r--r--	int_to_bv.cpp	7896	log plain
-rw-r--r--	int_to_bv.h	1370	log plain
-rw-r--r--	ite_removal.cpp	2566	log plain
-rw-r--r--	ite_removal.h	1316	log plain
-rw-r--r--	ite_simp.cpp	8819	log plain
-rw-r--r--	ite_simp.h	1461	log plain
-rw-r--r--	miplib_trick.cpp	22013	log plain
-rw-r--r--	miplib_trick.h	1736	log plain
-rw-r--r--	nl_ext_purify.cpp	3789	log plain
-rw-r--r--	nl_ext_purify.h	1675	log plain
-rw-r--r--	non_clausal_simp.cpp	17378	log plain
-rw-r--r--	non_clausal_simp.h	3136	log plain
-rw-r--r--	pseudo_boolean_processor.cpp	10278	log plain
-rw-r--r--	pseudo_boolean_processor.h	3368	log plain
-rw-r--r--	quantifier_macros.cpp	20493	log plain
-rw-r--r--	quantifier_macros.h	3556	log plain
-rw-r--r--	quantifiers_preprocess.cpp	1933	log plain
-rw-r--r--	quantifiers_preprocess.h	1456	log plain
-rw-r--r--	real_to_int.cpp	7088	log plain
-rw-r--r--	real_to_int.h	1498	log plain
-rw-r--r--	rewrite.cpp	1255	log plain
-rw-r--r--	rewrite.h	1243	log plain
-rw-r--r--	sep_skolem_emp.cpp	3678	log plain
-rw-r--r--	sep_skolem_emp.h	1243	log plain
-rw-r--r--	sort_infer.cpp	2947	log plain
-rw-r--r--	sort_infer.h	1500	log plain
-rw-r--r--	static_learning.cpp	1668	log plain
-rw-r--r--	static_learning.h	1250	log plain
-rw-r--r--	strings_eager_pp.cpp	1814	log plain
-rw-r--r--	strings_eager_pp.h	1359	log plain
-rw-r--r--	sygus_inference.cpp	10643	log plain
-rw-r--r--	sygus_inference.h	2519	log plain
-rw-r--r--	synth_rew_rules.cpp	17493	log plain
-rw-r--r--	synth_rew_rules.h	3210	log plain
-rw-r--r--	theory_preprocess.cpp	2376	log plain
-rw-r--r--	theory_preprocess.h	1320	log plain
-rw-r--r--	theory_rewrite_eq.cpp	3448	log plain
-rw-r--r--	theory_rewrite_eq.h	1906	log plain
-rw-r--r--	unconstrained_simplifier.cpp	27272	log plain
-rw-r--r--	unconstrained_simplifier.h	2491	log plain