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	96716	log plain
-rw-r--r--	approx_simplex.h	6077	log plain
-rw-r--r--	arith_ite_utils.cpp	13203	log plain
-rw-r--r--	arith_ite_utils.h	3162	log plain
-rw-r--r--	arith_rewriter.cpp	17102	log plain
-rw-r--r--	arith_rewriter.h	2274	log plain
-rw-r--r--	arith_static_learner.cpp	8321	log plain
-rw-r--r--	arith_static_learner.h	2079	log plain
-rw-r--r--	arith_utilities.h	7482	log plain
-rw-r--r--	arithvar.cpp	1098	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	5233	log plain
-rw-r--r--	attempt_solution_simplex.h	3730	log plain
-rw-r--r--	bound_counts.h	7949	log plain
-rw-r--r--	callbacks.cpp	5270	log plain
-rw-r--r--	callbacks.h	4827	log plain
-rw-r--r--	congruence_manager.cpp	15016	log plain
-rw-r--r--	congruence_manager.h	5162	log plain
-rw-r--r--	constraint.cpp	55759	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	17016	log plain
-rw-r--r--	cut_log.h	7122	log plain
-rw-r--r--	delta_rational.cpp	3188	log plain
-rw-r--r--	delta_rational.h	7652	log plain
-rw-r--r--	dio_solver.cpp	25474	log plain
-rw-r--r--	dio_solver.h	12800	log plain
-rw-r--r--	dual_simplex.cpp	9250	log plain
-rw-r--r--	dual_simplex.h	4251	log plain
-rw-r--r--	error_set.cpp	13276	log plain
-rw-r--r--	error_set.h	10560	log plain
-rw-r--r--	fc_simplex.cpp	27780	log plain
-rw-r--r--	fc_simplex.h	8845	log plain
-rw-r--r--	infer_bounds.cpp	8269	log plain
-rw-r--r--	infer_bounds.h	4024	log plain
-rw-r--r--	kinds	4826	log plain
-rw-r--r--	linear_equality.cpp	46838	log plain
-rw-r--r--	linear_equality.h	23750	log plain
-rw-r--r--	matrix.cpp	1033	log plain
-rw-r--r--	matrix.h	25385	log plain
-rw-r--r--	normal_form.cpp	36110	log plain
-rw-r--r--	normal_form.h	37915	log plain
-rw-r--r--	partial_model.cpp	17939	log plain
-rw-r--r--	partial_model.h	11747	log plain
-rw-r--r--	pseudoboolean_proc.cpp	9083	log plain
-rw-r--r--	pseudoboolean_proc.h	2914	log plain
-rw-r--r--	simplex.cpp	9164	log plain
-rw-r--r--	simplex.h	7948	log plain
-rw-r--r--	simplex_update.cpp	5125	log plain
-rw-r--r--	simplex_update.h	10445	log plain
-rw-r--r--	soi_simplex.cpp	34072	log plain
-rw-r--r--	soi_simplex.h	8681	log plain
-rw-r--r--	tableau.cpp	5581	log plain
-rw-r--r--	tableau.h	4615	log plain
-rw-r--r--	tableau_sizes.cpp	1080	log plain
-rw-r--r--	tableau_sizes.h	1128	log plain
-rw-r--r--	theory_arith.cpp	4410	log plain
-rw-r--r--	theory_arith.h	2512	log plain
-rw-r--r--	theory_arith_private.cpp	197329	log plain
-rw-r--r--	theory_arith_private.h	27462	log plain
-rw-r--r--	theory_arith_private_forward.h	873	log plain
-rw-r--r--	theory_arith_type_rules.h	5750	log plain
-rw-r--r--	type_enumerator.h	4481	log plain