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	33289	log plain
-rw-r--r--	abstraction.h	7573	log plain
-rw-r--r--	aig_bitblaster.cpp	17047	log plain
-rw-r--r--	bitblast_strategies_template.h	25467	log plain
-rw-r--r--	bitblast_utils.h	7037	log plain
-rw-r--r--	bitblaster_template.h	16193	log plain
-rw-r--r--	bv_eager_solver.cpp	3401	log plain
-rw-r--r--	bv_eager_solver.h	1513	log plain
-rw-r--r--	bv_inequality_graph.cpp	16895	log plain
-rw-r--r--	bv_inequality_graph.h	7765	log plain
-rw-r--r--	bv_quick_check.cpp	10626	log plain
-rw-r--r--	bv_quick_check.h	4688	log plain
-rw-r--r--	bv_subtheory.h	3066	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	30699	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6526	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8059	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2321	log plain
-rw-r--r--	bv_subtheory_core.cpp	15811	log plain
-rw-r--r--	bv_subtheory_core.h	3831	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	7837	log plain
-rw-r--r--	bv_subtheory_inequality.h	2487	log plain
-rw-r--r--	bv_to_bool.cpp	8233	log plain
-rw-r--r--	bv_to_bool.h	1940	log plain
-rw-r--r--	bvintropow2.cpp	2263	log plain
-rw-r--r--	bvintropow2.h	1224	log plain
-rw-r--r--	cd_set_collection.h	12439	log plain
-rw-r--r--	eager_bitblaster.cpp	6951	log plain
-rw-r--r--	kinds	11388	log plain
-rw-r--r--	lazy_bitblaster.cpp	18043	log plain
-rw-r--r--	slicer.cpp	17597	log plain
-rw-r--r--	slicer.h	6267	log plain
-rw-r--r--	theory_bv.cpp	28694	log plain
-rw-r--r--	theory_bv.h	6352	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	25534	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	12585	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	9181	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	38623	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	15967	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	33327	log plain
-rw-r--r--	theory_bv_rewriter.cpp	22338	log plain
-rw-r--r--	theory_bv_rewriter.h	4958	log plain
-rw-r--r--	theory_bv_type_rules.h	10773	log plain
-rw-r--r--	theory_bv_utils.cpp	3042	log plain
-rw-r--r--	theory_bv_utils.h	13637	log plain
-rw-r--r--	type_enumerator.h	1766	log plain