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--	bitblast_strategies.cpp	28106	log plain
-rw-r--r--	bitblast_strategies.h	3981	log plain
-rw-r--r--	bitblaster.cpp	16236	log plain
-rw-r--r--	bitblaster.h	5258	log plain
-rw-r--r--	bv_inequality_graph.cpp	16543	log plain
-rw-r--r--	bv_inequality_graph.h	7855	log plain
-rw-r--r--	bv_subtheory.h	2674	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	5899	log plain
-rw-r--r--	bv_subtheory_bitblast.h	1698	log plain
-rw-r--r--	bv_subtheory_core.cpp	14776	log plain
-rw-r--r--	bv_subtheory_core.h	3473	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	6796	log plain
-rw-r--r--	bv_subtheory_inequality.h	2008	log plain
-rw-r--r--	bv_to_bool.cpp	10320	log plain
-rw-r--r--	bv_to_bool.h	2222	log plain
-rw-r--r--	cd_set_collection.h	12439	log plain
-rw-r--r--	kinds	8397	log plain
-rw-r--r--	options	1020	log plain
-rw-r--r--	slicer.cpp	17470	log plain
-rw-r--r--	slicer.h	6266	log plain
-rw-r--r--	theory_bv.cpp	12376	log plain
-rw-r--r--	theory_bv.h	4511	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	24422	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	35633	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	15034	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	25966	log plain
-rw-r--r--	theory_bv_rewriter.cpp	22302	log plain
-rw-r--r--	theory_bv_rewriter.h	4805	log plain
-rw-r--r--	theory_bv_type_rules.h	8488	log plain
-rw-r--r--	theory_bv_utils.h	13307	log plain
-rw-r--r--	type_enumerator.h	1716	log plain