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	33356	log plain
-rw-r--r--	abstraction.h	7616	log plain
-rw-r--r--	aig_bitblaster.cpp	17726	log plain
-rw-r--r--	bitblast_strategies_template.h	25515	log plain
-rw-r--r--	bitblast_utils.h	7089	log plain
-rw-r--r--	bitblaster_template.h	16235	log plain
-rw-r--r--	bv_eager_solver.cpp	3453	log plain
-rw-r--r--	bv_eager_solver.h	1565	log plain
-rw-r--r--	bv_inequality_graph.cpp	16953	log plain
-rw-r--r--	bv_inequality_graph.h	7817	log plain
-rw-r--r--	bv_quick_check.cpp	10693	log plain
-rw-r--r--	bv_quick_check.h	4746	log plain
-rw-r--r--	bv_subtheory.h	3114	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	30766	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6593	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8060	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2338	log plain
-rw-r--r--	bv_subtheory_core.cpp	15860	log plain
-rw-r--r--	bv_subtheory_core.h	3863	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	7886	log plain
-rw-r--r--	bv_subtheory_inequality.h	2550	log plain
-rw-r--r--	bv_to_bool.cpp	8276	log plain
-rw-r--r--	bv_to_bool.h	1992	log plain
-rw-r--r--	bvintropow2.cpp	2330	log plain
-rw-r--r--	bvintropow2.h	1291	log plain
-rw-r--r--	cd_set_collection.h	12487	log plain
-rw-r--r--	eager_bitblaster.cpp	7555	log plain
-rw-r--r--	kinds	11388	log plain
-rw-r--r--	lazy_bitblaster.cpp	18096	log plain
-rw-r--r--	slicer.cpp	17655	log plain
-rw-r--r--	slicer.h	6319	log plain
-rw-r--r--	theory_bv.cpp	28151	log plain
-rw-r--r--	theory_bv.h	6384	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	25563	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	12624	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	9204	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	38645	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	16144	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	33343	log plain
-rw-r--r--	theory_bv_rewriter.cpp	22365	log plain
-rw-r--r--	theory_bv_rewriter.h	5002	log plain
-rw-r--r--	theory_bv_type_rules.h	10798	log plain
-rw-r--r--	theory_bv_utils.cpp	3094	log plain
-rw-r--r--	theory_bv_utils.h	13660	log plain
-rw-r--r--	type_enumerator.h	1824	log plain