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	33131	log plain
-rw-r--r--	abstraction.h	7613	log plain
-rw-r--r--	aig_bitblaster.cpp	14344	log plain
-rw-r--r--	bitblast_strategies_template.h	27058	log plain
-rw-r--r--	bitblast_utils.h	7109	log plain
-rw-r--r--	bitblaster_template.h	16790	log plain
-rw-r--r--	bv_eager_solver.cpp	3694	log plain
-rw-r--r--	bv_eager_solver.h	1694	log plain
-rw-r--r--	bv_inequality_graph.cpp	16954	log plain
-rw-r--r--	bv_inequality_graph.h	7936	log plain
-rw-r--r--	bv_quick_check.cpp	10700	log plain
-rw-r--r--	bv_quick_check.h	4746	log plain
-rw-r--r--	bv_subtheory.h	3249	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	30983	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6638	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8662	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2398	log plain
-rw-r--r--	bv_subtheory_core.cpp	16233	log plain
-rw-r--r--	bv_subtheory_core.h	4047	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8048	log plain
-rw-r--r--	bv_subtheory_inequality.h	2595	log plain
-rw-r--r--	bv_to_bool.cpp	12505	log plain
-rw-r--r--	bv_to_bool.h	2444	log plain
-rw-r--r--	bvgauss.cpp	19686	log plain
-rw-r--r--	bvgauss.h	5174	log plain
-rw-r--r--	bvintropow2.cpp	2331	log plain
-rw-r--r--	bvintropow2.h	1292	log plain
-rw-r--r--	cd_set_collection.h	12488	log plain
-rw-r--r--	eager_bitblaster.cpp	7697	log plain
-rw-r--r--	kinds	11979	log plain
-rw-r--r--	lazy_bitblaster.cpp	18399	log plain
-rw-r--r--	slicer.cpp	17651	log plain
-rw-r--r--	slicer.h	6327	log plain
-rw-r--r--	theory_bv.cpp	36089	log plain
-rw-r--r--	theory_bv.h	7264	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	26278	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14695	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	9204	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	38644	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	16322	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	42679	log plain
-rw-r--r--	theory_bv_rewriter.cpp	23776	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	16849	log plain
-rw-r--r--	theory_bv_utils.h	7567	log plain
-rw-r--r--	type_enumerator.h	1751	log plain