bags « 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--	bag_make_op.cpp	1264	log plain
-rw-r--r--	bag_make_op.h	1748	log plain
-rw-r--r--	bag_reduction.cpp	8646	log plain
-rw-r--r--	bag_reduction.h	3390	log plain
-rw-r--r--	bag_solver.cpp	7412	log plain
-rw-r--r--	bag_solver.h	3502	log plain
-rw-r--r--	bags_rewriter.cpp	20170	log plain
-rw-r--r--	bags_rewriter.h	8663	log plain
-rw-r--r--	bags_statistics.cpp	917	log plain
-rw-r--r--	bags_statistics.h	1142	log plain
-rw-r--r--	infer_info.cpp	2360	log plain
-rw-r--r--	infer_info.h	2630	log plain
-rw-r--r--	inference_generator.cpp	14205	log plain
-rw-r--r--	inference_generator.h	7789	log plain
-rw-r--r--	inference_manager.cpp	1421	log plain
-rw-r--r--	inference_manager.h	2192	log plain
-rw-r--r--	kinds	5009	log plain
-rw-r--r--	normal_form.cpp	23187	log plain
-rw-r--r--	normal_form.h	8129	log plain
-rw-r--r--	rewrites.cpp	3868	log plain
-rw-r--r--	rewrites.h	2520	log plain
-rw-r--r--	solver_state.cpp	3510	log plain
-rw-r--r--	solver_state.h	2933	log plain
-rw-r--r--	term_registry.cpp	1367	log plain
-rw-r--r--	term_registry.h	1766	log plain
-rw-r--r--	theory_bags.cpp	11884	log plain
-rw-r--r--	theory_bags.h	4338	log plain
-rw-r--r--	theory_bags_type_enumerator.cpp	2582	log plain
-rw-r--r--	theory_bags_type_enumerator.h	3489	log plain
-rw-r--r--	theory_bags_type_rules.cpp	12512	log plain
-rw-r--r--	theory_bags_type_rules.h	4423	log plain