arith « 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--	approx_simplex.cpp	92128	log plain
-rw-r--r--	approx_simplex.h	5053	log plain
-rw-r--r--	arith_ite_utils.cpp	13165	log plain
-rw-r--r--	arith_ite_utils.h	3132	log plain
-rw-r--r--	arith_msum.cpp	7706	log plain
-rw-r--r--	arith_msum.h	6642	log plain
-rw-r--r--	arith_rewriter.cpp	24758	log plain
-rw-r--r--	arith_rewriter.h	2397	log plain
-rw-r--r--	arith_static_learner.cpp	8320	log plain
-rw-r--r--	arith_static_learner.h	2068	log plain
-rw-r--r--	arith_utilities.h	8540	log plain
-rw-r--r--	arithvar.cpp	1083	log plain
-rw-r--r--	arithvar.h	1313	log plain
-rw-r--r--	arithvar_node_map.h	2495	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5218	log plain
-rw-r--r--	attempt_solution_simplex.h	3737	log plain
-rw-r--r--	bound_counts.h	7949	log plain
-rw-r--r--	callbacks.cpp	5255	log plain
-rw-r--r--	callbacks.h	4874	log plain
-rw-r--r--	congruence_manager.cpp	17629	log plain
-rw-r--r--	congruence_manager.h	5883	log plain
-rw-r--r--	constraint.cpp	55704	log plain
-rw-r--r--	constraint.h	36524	log plain
-rw-r--r--	constraint_forward.h	1646	log plain
-rw-r--r--	cut_log.cpp	17069	log plain
-rw-r--r--	cut_log.h	7086	log plain
-rw-r--r--	delta_rational.cpp	3195	log plain
-rw-r--r--	delta_rational.h	7727	log plain
-rw-r--r--	dio_solver.cpp	25519	log plain
-rw-r--r--	dio_solver.h	12798	log plain
-rw-r--r--	dual_simplex.cpp	9246	log plain
-rw-r--r--	dual_simplex.h	4264	log plain
-rw-r--r--	error_set.cpp	13261	log plain
-rw-r--r--	error_set.h	10545	log plain
-rw-r--r--	fc_simplex.cpp	27776	log plain
-rw-r--r--	fc_simplex.h	8871	log plain
-rw-r--r--	infer_bounds.cpp	8269	log plain
-rw-r--r--	infer_bounds.h	4024	log plain
-rw-r--r--	kinds	5768	log plain
-rw-r--r--	linear_equality.cpp	46898	log plain
-rw-r--r--	linear_equality.h	23805	log plain
-rw-r--r--	matrix.cpp	1033	log plain
-rw-r--r--	matrix.h	25411	log plain
-rw-r--r--	nonlinear_extension.cpp	168203	log plain
-rw-r--r--	nonlinear_extension.h	37980	log plain
-rw-r--r--	normal_form.cpp	36735	log plain
-rw-r--r--	normal_form.h	36865	log plain
-rw-r--r--	partial_model.cpp	18060	log plain
-rw-r--r--	partial_model.h	12147	log plain
-rw-r--r--	simplex.cpp	9196	log plain
-rw-r--r--	simplex.h	7979	log plain
-rw-r--r--	simplex_update.cpp	5125	log plain
-rw-r--r--	simplex_update.h	10552	log plain
-rw-r--r--	soi_simplex.cpp	34083	log plain
-rw-r--r--	soi_simplex.h	8707	log plain
-rw-r--r--	tableau.cpp	5566	log plain
-rw-r--r--	tableau.h	4600	log plain
-rw-r--r--	tableau_sizes.cpp	1065	log plain
-rw-r--r--	tableau_sizes.h	1113	log plain
-rw-r--r--	theory_arith.cpp	5008	log plain
-rw-r--r--	theory_arith.h	2857	log plain
-rw-r--r--	theory_arith_private.cpp	204599	log plain
-rw-r--r--	theory_arith_private.h	29042	log plain
-rw-r--r--	theory_arith_private_forward.h	858	log plain
-rw-r--r--	theory_arith_type_rules.h	5477	log plain
-rw-r--r--	type_enumerator.h	3020	log plain