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	32469	log plain
-rw-r--r--	abstraction.h	7517	log plain
d---------	bitblast	608	log plain
-rw-r--r--	bv_eager_solver.cpp	3388	log plain
-rw-r--r--	bv_eager_solver.h	1683	log plain
-rw-r--r--	bv_inequality_graph.cpp	16957	log plain
-rw-r--r--	bv_inequality_graph.h	7870	log plain
-rw-r--r--	bv_quick_check.cpp	10102	log plain
-rw-r--r--	bv_quick_check.h	4844	log plain
-rw-r--r--	bv_solver.h	3371	log plain
-rw-r--r--	bv_solver_bitblast.cpp	11722	log plain
-rw-r--r--	bv_solver_bitblast.h	4605	log plain
-rw-r--r--	bv_solver_lazy.cpp	20901	log plain
-rw-r--r--	bv_solver_lazy.h	6148	log plain
-rw-r--r--	bv_solver_simple.cpp	4359	log plain
-rw-r--r--	bv_solver_simple.h	2360	log plain
-rw-r--r--	bv_subtheory.h	3088	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	29776	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6736	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8214	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2365	log plain
-rw-r--r--	bv_subtheory_core.cpp	20095	log plain
-rw-r--r--	bv_subtheory_core.h	5708	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8269	log plain
-rw-r--r--	bv_subtheory_inequality.h	2734	log plain
-rw-r--r--	int_blaster.h	13052	log plain
-rw-r--r--	kinds	12987	log plain
-rw-r--r--	proof_checker.cpp	5531	log plain
-rw-r--r--	proof_checker.h	1512	log plain
-rw-r--r--	slicer.cpp	1887	log plain
-rw-r--r--	slicer.h	1359	log plain
-rw-r--r--	theory_bv.cpp	9541	log plain
-rw-r--r--	theory_bv.h	3897	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	30948	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14841	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	10037	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	42300	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	23651	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	60799	log plain
-rw-r--r--	theory_bv_rewriter.cpp	25146	log plain
-rw-r--r--	theory_bv_rewriter.h	5347	log plain
-rw-r--r--	theory_bv_type_rules.cpp	10619	log plain
-rw-r--r--	theory_bv_type_rules.h	4580	log plain
-rw-r--r--	theory_bv_utils.cpp	12309	log plain
-rw-r--r--	theory_bv_utils.h	7779	log plain
-rw-r--r--	type_enumerator.h	1733	log plain