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	96747	log plain
-rw-r--r--	approx_simplex.h	6088	log plain
-rw-r--r--	arith_ite_utils.cpp	13198	log plain
-rw-r--r--	arith_ite_utils.h	3156	log plain
-rw-r--r--	arith_msum.cpp	7680	log plain
-rw-r--r--	arith_msum.h	6642	log plain
-rw-r--r--	arith_rewriter.cpp	23858	log plain
-rw-r--r--	arith_rewriter.h	2397	log plain
-rw-r--r--	arith_static_learner.cpp	8277	log plain
-rw-r--r--	arith_static_learner.h	2073	log plain
-rw-r--r--	arith_utilities.h	8534	log plain
-rw-r--r--	arithvar.cpp	1109	log plain
-rw-r--r--	arithvar.h	1324	log plain
-rw-r--r--	arithvar_node_map.h	2489	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5244	log plain
-rw-r--r--	attempt_solution_simplex.h	3741	log plain
-rw-r--r--	bound_counts.h	7945	log plain
-rw-r--r--	callbacks.cpp	5281	log plain
-rw-r--r--	callbacks.h	4823	log plain
-rw-r--r--	congruence_manager.cpp	17629	log plain
-rw-r--r--	congruence_manager.h	5698	log plain
-rw-r--r--	constraint.cpp	55715	log plain
-rw-r--r--	constraint.h	36535	log plain
-rw-r--r--	constraint_forward.h	1657	log plain
-rw-r--r--	cut_log.cpp	17027	log plain
-rw-r--r--	cut_log.h	7086	log plain
-rw-r--r--	delta_rational.cpp	3199	log plain
-rw-r--r--	delta_rational.h	7652	log plain
-rw-r--r--	dio_solver.cpp	25513	log plain
-rw-r--r--	dio_solver.h	12809	log plain
-rw-r--r--	dual_simplex.cpp	9283	log plain
-rw-r--r--	dual_simplex.h	4262	log plain
-rw-r--r--	error_set.cpp	13287	log plain
-rw-r--r--	error_set.h	10571	log plain
-rw-r--r--	fc_simplex.cpp	27813	log plain
-rw-r--r--	fc_simplex.h	8856	log plain
-rw-r--r--	infer_bounds.cpp	8280	log plain
-rw-r--r--	infer_bounds.h	4035	log plain
-rw-r--r--	kinds	4807	log plain
-rw-r--r--	linear_equality.cpp	46849	log plain
-rw-r--r--	linear_equality.h	23746	log plain
-rw-r--r--	matrix.cpp	1044	log plain
-rw-r--r--	matrix.h	25381	log plain
-rw-r--r--	nonlinear_extension.cpp	140690	log plain
-rw-r--r--	nonlinear_extension.h	28160	log plain
-rw-r--r--	normal_form.cpp	36498	log plain
-rw-r--r--	normal_form.h	36604	log plain
-rw-r--r--	partial_model.cpp	18071	log plain
-rw-r--r--	partial_model.h	12158	log plain
-rw-r--r--	pseudoboolean_proc.cpp	9094	log plain
-rw-r--r--	pseudoboolean_proc.h	2925	log plain
-rw-r--r--	simplex.cpp	9191	log plain
-rw-r--r--	simplex.h	7975	log plain
-rw-r--r--	simplex_update.cpp	5136	log plain
-rw-r--r--	simplex_update.h	10456	log plain
-rw-r--r--	soi_simplex.cpp	34105	log plain
-rw-r--r--	soi_simplex.h	8692	log plain
-rw-r--r--	tableau.cpp	5592	log plain
-rw-r--r--	tableau.h	4626	log plain
-rw-r--r--	tableau_sizes.cpp	1091	log plain
-rw-r--r--	tableau_sizes.h	1139	log plain
-rw-r--r--	theory_arith.cpp	5078	log plain
-rw-r--r--	theory_arith.h	2599	log plain
-rw-r--r--	theory_arith_private.cpp	200661	log plain
-rw-r--r--	theory_arith_private.h	28144	log plain
-rw-r--r--	theory_arith_private_forward.h	884	log plain
-rw-r--r--	theory_arith_type_rules.h	5965	log plain
-rw-r--r--	type_enumerator.h	3088	log plain