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

Mode	Name	Size
-rw-r--r--	abstraction.cpp	33489	log plain
-rw-r--r--	abstraction.h	7583	log plain
d---------	bitblast	418	log plain
-rw-r--r--	bv_eager_solver.cpp	3583	log plain
-rw-r--r--	bv_eager_solver.h	1898	log plain
-rw-r--r--	bv_inequality_graph.cpp	17026	log plain
-rw-r--r--	bv_inequality_graph.h	7950	log plain
-rw-r--r--	bv_quick_check.cpp	10591	log plain
-rw-r--r--	bv_quick_check.h	4767	log plain
-rw-r--r--	bv_subtheory.h	3304	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	31674	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6788	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8537	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2507	log plain
-rw-r--r--	bv_subtheory_core.cpp	16351	log plain
-rw-r--r--	bv_subtheory_core.h	4313	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8390	log plain
-rw-r--r--	bv_subtheory_inequality.h	2700	log plain
-rw-r--r--	kinds	13176	log plain
-rw-r--r--	slicer.cpp	18129	log plain
-rw-r--r--	slicer.h	6309	log plain
-rw-r--r--	theory_bv.cpp	32964	log plain
-rw-r--r--	theory_bv.h	8132	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	29615	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14699	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	10024	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	41351	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	17246	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	59239	log plain
-rw-r--r--	theory_bv_rewriter.cpp	24728	log plain
-rw-r--r--	theory_bv_rewriter.h	5220	log plain
-rw-r--r--	theory_bv_type_rules.h	13399	log plain
-rw-r--r--	theory_bv_utils.cpp	11586	log plain
-rw-r--r--	theory_bv_utils.h	7514	log plain
-rw-r--r--	type_enumerator.h	1780	log plain