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	32497	log plain
-rw-r--r--	abstraction.h	7517	log plain
d---------	bitblast	604	log plain
-rw-r--r--	bv_eager_solver.cpp	3466	log plain
-rw-r--r--	bv_eager_solver.h	1692	log plain
-rw-r--r--	bv_inequality_graph.cpp	16957	log plain
-rw-r--r--	bv_inequality_graph.h	7898	log plain
-rw-r--r--	bv_quick_check.cpp	10108	log plain
-rw-r--r--	bv_quick_check.h	4850	log plain
-rw-r--r--	bv_solver.h	3757	log plain
-rw-r--r--	bv_solver_bitblast.cpp	12230	log plain
-rw-r--r--	bv_solver_bitblast.h	4239	log plain
-rw-r--r--	bv_solver_bitblast_internal.cpp	4993	log plain
-rw-r--r--	bv_solver_bitblast_internal.h	2566	log plain
-rw-r--r--	bv_solver_layered.cpp	20318	log plain
-rw-r--r--	bv_solver_layered.h	6154	log plain
-rw-r--r--	bv_subtheory.h	3097	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	29810	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6739	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8220	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2368	log plain
-rw-r--r--	bv_subtheory_core.cpp	13630	log plain
-rw-r--r--	bv_subtheory_core.h	3358	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8271	log plain
-rw-r--r--	bv_subtheory_inequality.h	2775	log plain
-rw-r--r--	int_blaster.cpp	26584	log plain
-rw-r--r--	int_blaster.h	14063	log plain
-rw-r--r--	kinds	13042	log plain
-rw-r--r--	proof_checker.cpp	1737	log plain
-rw-r--r--	proof_checker.h	1464	log plain
-rw-r--r--	slicer.cpp	1887	log plain
-rw-r--r--	slicer.h	1359	log plain
-rw-r--r--	theory_bv.cpp	11751	log plain
-rw-r--r--	theory_bv.h	4194	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	30256	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14857	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	10037	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	42302	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	23664	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	60813	log plain
-rw-r--r--	theory_bv_rewriter.cpp	25285	log plain
-rw-r--r--	theory_bv_rewriter.h	5346	log plain
-rw-r--r--	theory_bv_type_rules.cpp	10677	log plain
-rw-r--r--	theory_bv_type_rules.h	4580	log plain
-rw-r--r--	theory_bv_utils.cpp	12363	log plain
-rw-r--r--	theory_bv_utils.h	7804	log plain
-rw-r--r--	type_enumerator.h	1733	log plain