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	33677	log plain
-rw-r--r--	abstraction.h	7613	log plain
d---------	bitblast	418	log plain
-rw-r--r--	bv_eager_solver.cpp	3748	log plain
-rw-r--r--	bv_eager_solver.h	1694	log plain
-rw-r--r--	bv_inequality_graph.cpp	17045	log plain
-rw-r--r--	bv_inequality_graph.h	7936	log plain
-rw-r--r--	bv_quick_check.cpp	10634	log plain
-rw-r--r--	bv_quick_check.h	4751	log plain
-rw-r--r--	bv_subtheory.h	3249	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	31708	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6765	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8593	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2391	log plain
-rw-r--r--	bv_subtheory_core.cpp	16598	log plain
-rw-r--r--	bv_subtheory_core.h	4297	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8167	log plain
-rw-r--r--	bv_subtheory_inequality.h	2676	log plain
-rw-r--r--	kinds	11983	log plain
-rw-r--r--	slicer.cpp	18146	log plain
-rw-r--r--	slicer.h	6327	log plain
-rw-r--r--	theory_bv.cpp	32965	log plain
-rw-r--r--	theory_bv.h	6915	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	26278	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14699	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	9204	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	39768	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	17312	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	44887	log plain
-rw-r--r--	theory_bv_rewriter.cpp	23840	log plain
-rw-r--r--	theory_bv_rewriter.h	5230	log plain
-rw-r--r--	theory_bv_type_rules.h	11758	log plain
-rw-r--r--	theory_bv_utils.cpp	10629	log plain
-rw-r--r--	theory_bv_utils.h	7044	log plain
-rw-r--r--	type_enumerator.h	1780	log plain