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	32675	log plain
-rw-r--r--	abstraction.h	7590	log plain
d---------	bitblast	418	log plain
-rw-r--r--	bv_eager_solver.cpp	3396	log plain
-rw-r--r--	bv_eager_solver.h	1785	log plain
-rw-r--r--	bv_inequality_graph.cpp	17028	log plain
-rw-r--r--	bv_inequality_graph.h	7952	log plain
-rw-r--r--	bv_quick_check.cpp	10726	log plain
-rw-r--r--	bv_quick_check.h	4926	log plain
-rw-r--r--	bv_solver.h	3312	log plain
-rw-r--r--	bv_solver_lazy.cpp	24463	log plain
-rw-r--r--	bv_solver_lazy.h	6414	log plain
-rw-r--r--	bv_subtheory.h	3119	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	30474	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6897	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8468	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2423	log plain
-rw-r--r--	bv_subtheory_core.cpp	20144	log plain
-rw-r--r--	bv_subtheory_core.h	5859	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8472	log plain
-rw-r--r--	bv_subtheory_inequality.h	2829	log plain
-rw-r--r--	kinds	13176	log plain
-rw-r--r--	slicer.cpp	1891	log plain
-rw-r--r--	slicer.h	1380	log plain
-rw-r--r--	theory_bv.cpp	6344	log plain
-rw-r--r--	theory_bv.h	3566	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	30809	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14706	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	10024	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	42423	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	24285	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	60444	log plain
-rw-r--r--	theory_bv_rewriter.cpp	24804	log plain
-rw-r--r--	theory_bv_rewriter.h	5219	log plain
-rw-r--r--	theory_bv_type_rules.h	13685	log plain
-rw-r--r--	theory_bv_utils.cpp	12308	log plain
-rw-r--r--	theory_bv_utils.h	7901	log plain
-rw-r--r--	type_enumerator.h	1780	log plain