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	33267	log plain
-rw-r--r--	abstraction.h	7567	log plain
-rw-r--r--	aig_bitblaster.h	16932	log plain
-rw-r--r--	bitblast_mode.cpp	1452	log plain
-rw-r--r--	bitblast_mode.h	1680	log plain
-rw-r--r--	bitblast_strategies_template.h	25516	log plain
-rw-r--r--	bitblast_utils.h	7038	log plain
-rw-r--r--	bitblaster_template.h	13246	log plain
-rw-r--r--	bv_eager_solver.cpp	2958	log plain
-rw-r--r--	bv_eager_solver.h	1266	log plain
-rw-r--r--	bv_inequality_graph.cpp	16855	log plain
-rw-r--r--	bv_inequality_graph.h	7855	log plain
-rw-r--r--	bv_quick_check.cpp	10487	log plain
-rw-r--r--	bv_quick_check.h	4745	log plain
-rw-r--r--	bv_subtheory.h	2967	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	30374	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6514	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8401	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2197	log plain
-rw-r--r--	bv_subtheory_core.cpp	15272	log plain
-rw-r--r--	bv_subtheory_core.h	3803	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	7586	log plain
-rw-r--r--	bv_subtheory_inequality.h	2216	log plain
-rw-r--r--	bv_to_bool.cpp	8152	log plain
-rw-r--r--	bv_to_bool.h	1941	log plain
-rw-r--r--	bvintropow2.cpp	1669	log plain
-rw-r--r--	bvintropow2.h	632	log plain
-rw-r--r--	cd_set_collection.h	12439	log plain
-rw-r--r--	eager_bitblaster.h	4340	log plain
-rw-r--r--	kinds	9028	log plain
-rw-r--r--	lazy_bitblaster.h	16428	log plain
-rw-r--r--	options	3429	log plain
-rw-r--r--	options_handlers.h	5271	log plain
-rw-r--r--	slicer.cpp	17504	log plain
-rw-r--r--	slicer.h	6266	log plain
-rw-r--r--	theory_bv.cpp	27567	log plain
-rw-r--r--	theory_bv.h	6031	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	25085	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	12585	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	9163	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	37337	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	15034	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	33304	log plain
-rw-r--r--	theory_bv_rewriter.cpp	21635	log plain
-rw-r--r--	theory_bv_rewriter.h	4805	log plain
-rw-r--r--	theory_bv_type_rules.h	9751	log plain
-rw-r--r--	theory_bv_utils.cpp	2831	log plain
-rw-r--r--	theory_bv_utils.h	13237	log plain
-rw-r--r--	type_enumerator.h	1716	log plain