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	11095	log plain
-rw-r--r--	ackermann.h	3203	log plain
-rw-r--r--	apply_substs.cpp	2381	log plain
-rw-r--r--	apply_substs.h	1465	log plain
-rw-r--r--	bool_to_bv.cpp	12311	log plain
-rw-r--r--	bool_to_bv.h	4156	log plain
-rw-r--r--	bv_abstraction.cpp	2409	log plain
-rw-r--r--	bv_abstraction.h	1679	log plain
-rw-r--r--	bv_eager_atoms.cpp	1637	log plain
-rw-r--r--	bv_eager_atoms.h	1377	log plain
-rw-r--r--	bv_gauss.cpp	22376	log plain
-rw-r--r--	bv_gauss.h	3378	log plain
-rw-r--r--	bv_intro_pow2.cpp	2930	log plain
-rw-r--r--	bv_intro_pow2.h	1421	log plain
-rw-r--r--	bv_to_bool.cpp	9056	log plain
-rw-r--r--	bv_to_bool.h	2314	log plain
-rw-r--r--	bv_to_int.cpp	38820	log plain
-rw-r--r--	bv_to_int.h	12824	log plain
-rw-r--r--	extended_rewriter_pass.cpp	1391	log plain
-rw-r--r--	extended_rewriter_pass.h	1315	log plain
-rw-r--r--	global_negate.cpp	3218	log plain
-rw-r--r--	global_negate.h	1679	log plain
-rw-r--r--	ho_elim.cpp	17372	log plain
-rw-r--r--	ho_elim.h	5829	log plain
-rw-r--r--	int_to_bv.cpp	7867	log plain
-rw-r--r--	int_to_bv.h	1371	log plain
-rw-r--r--	ite_removal.cpp	2049	log plain
-rw-r--r--	ite_removal.h	1317	log plain
-rw-r--r--	ite_simp.cpp	8891	log plain
-rw-r--r--	ite_simp.h	1462	log plain
-rw-r--r--	miplib_trick.cpp	21980	log plain
-rw-r--r--	miplib_trick.h	1753	log plain
-rw-r--r--	nl_ext_purify.cpp	3830	log plain
-rw-r--r--	nl_ext_purify.h	1676	log plain
-rw-r--r--	non_clausal_simp.cpp	16498	log plain
-rw-r--r--	non_clausal_simp.h	1462	log plain
-rw-r--r--	pseudo_boolean_processor.cpp	10279	log plain
-rw-r--r--	pseudo_boolean_processor.h	3369	log plain
-rw-r--r--	quantifier_macros.cpp	20306	log plain
-rw-r--r--	quantifier_macros.h	3135	log plain
-rw-r--r--	quantifiers_preprocess.cpp	1917	log plain
-rw-r--r--	quantifiers_preprocess.h	1457	log plain
-rw-r--r--	real_to_int.cpp	7119	log plain
-rw-r--r--	real_to_int.h	1499	log plain
-rw-r--r--	rewrite.cpp	1257	log plain
-rw-r--r--	rewrite.h	1244	log plain
-rw-r--r--	sep_skolem_emp.cpp	3679	log plain
-rw-r--r--	sep_skolem_emp.h	1244	log plain
-rw-r--r--	sort_infer.cpp	2934	log plain
-rw-r--r--	sort_infer.h	1501	log plain
-rw-r--r--	static_learning.cpp	1586	log plain
-rw-r--r--	static_learning.h	1251	log plain
-rw-r--r--	sygus_inference.cpp	10878	log plain
-rw-r--r--	sygus_inference.h	2514	log plain
-rw-r--r--	synth_rew_rules.cpp	17778	log plain
-rw-r--r--	synth_rew_rules.h	3211	log plain
-rw-r--r--	theory_preprocess.cpp	1609	log plain
-rw-r--r--	theory_preprocess.h	1321	log plain
-rw-r--r--	unconstrained_simplifier.cpp	27099	log plain
-rw-r--r--	unconstrained_simplifier.h	2524	log plain