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	32670	log plain
-rw-r--r--	abstraction.h	7619	log plain
d---------	bitblast	608	log plain
-rw-r--r--	bv_eager_solver.cpp	3428	log plain
-rw-r--r--	bv_eager_solver.h	1740	log plain
-rw-r--r--	bv_inequality_graph.cpp	17025	log plain
-rw-r--r--	bv_inequality_graph.h	7956	log plain
-rw-r--r--	bv_quick_check.cpp	10720	log plain
-rw-r--r--	bv_quick_check.h	4955	log plain
-rw-r--r--	bv_solver.h	3448	log plain
-rw-r--r--	bv_solver_bitblast.cpp	8153	log plain
-rw-r--r--	bv_solver_bitblast.h	4331	log plain
-rw-r--r--	bv_solver_lazy.cpp	24543	log plain
-rw-r--r--	bv_solver_lazy.h	6421	log plain
-rw-r--r--	bv_solver_simple.cpp	3911	log plain
-rw-r--r--	bv_solver_simple.h	2513	log plain
-rw-r--r--	bv_subtheory.h	3118	log plain
-rw-r--r--	bv_subtheory_algebraic.cpp	30449	log plain
-rw-r--r--	bv_subtheory_algebraic.h	6896	log plain
-rw-r--r--	bv_subtheory_bitblast.cpp	8467	log plain
-rw-r--r--	bv_subtheory_bitblast.h	2422	log plain
-rw-r--r--	bv_subtheory_core.cpp	20165	log plain
-rw-r--r--	bv_subtheory_core.h	5834	log plain
-rw-r--r--	bv_subtheory_inequality.cpp	8500	log plain
-rw-r--r--	bv_subtheory_inequality.h	2827	log plain
-rw-r--r--	int_blaster.h	13088	log plain
-rw-r--r--	kinds	12751	log plain
-rw-r--r--	proof_checker.cpp	1546	log plain
-rw-r--r--	proof_checker.h	1495	log plain
-rw-r--r--	slicer.cpp	1893	log plain
-rw-r--r--	slicer.h	1386	log plain
-rw-r--r--	theory_bv.cpp	7151	log plain
-rw-r--r--	theory_bv.h	3688	log plain
-rw-r--r--	theory_bv_rewrite_rules.h	30874	log plain
-rw-r--r--	theory_bv_rewrite_rules_constant_evaluation.h	14513	log plain
-rw-r--r--	theory_bv_rewrite_rules_core.h	10022	log plain
-rw-r--r--	theory_bv_rewrite_rules_normalization.h	42422	log plain
-rw-r--r--	theory_bv_rewrite_rules_operator_elimination.h	23652	log plain
-rw-r--r--	theory_bv_rewrite_rules_simplification.h	60825	log plain
-rw-r--r--	theory_bv_rewriter.cpp	24354	log plain
-rw-r--r--	theory_bv_rewriter.h	5229	log plain
-rw-r--r--	theory_bv_type_rules.h	13684	log plain
-rw-r--r--	theory_bv_utils.cpp	12307	log plain
-rw-r--r--	theory_bv_utils.h	7869	log plain
-rw-r--r--	type_enumerator.h	1779	log plain