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	96397	log plain
-rw-r--r--	approx_simplex.h	6029	log plain
-rw-r--r--	arith_ite_utils.cpp	13140	log plain
-rw-r--r--	arith_ite_utils.h	3105	log plain
-rw-r--r--	arith_rewriter.cpp	17048	log plain
-rw-r--r--	arith_rewriter.h	2226	log plain
-rw-r--r--	arith_static_learner.cpp	8206	log plain
-rw-r--r--	arith_static_learner.h	2025	log plain
-rw-r--r--	arith_utilities.h	7434	log plain
-rw-r--r--	arithvar.cpp	1050	log plain
-rw-r--r--	arithvar.h	1280	log plain
-rw-r--r--	arithvar_node_map.h	2441	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5105	log plain
-rw-r--r--	attempt_solution_simplex.h	3683	log plain
-rw-r--r--	bound_counts.h	7886	log plain
-rw-r--r--	callbacks.cpp	5213	log plain
-rw-r--r--	callbacks.h	4755	log plain
-rw-r--r--	congruence_manager.cpp	14236	log plain
-rw-r--r--	congruence_manager.h	5114	log plain
-rw-r--r--	constraint.cpp	55649	log plain
-rw-r--r--	constraint.h	36480	log plain
-rw-r--r--	constraint_forward.h	1613	log plain
-rw-r--r--	cut_log.cpp	16959	log plain
-rw-r--r--	cut_log.h	7074	log plain
-rw-r--r--	delta_rational.cpp	3140	log plain
-rw-r--r--	delta_rational.h	7574	log plain
-rw-r--r--	dio_solver.cpp	25319	log plain
-rw-r--r--	dio_solver.h	12752	log plain
-rw-r--r--	dual_simplex.cpp	9100	log plain
-rw-r--r--	dual_simplex.h	4204	log plain
-rw-r--r--	error_set.cpp	13127	log plain
-rw-r--r--	error_set.h	10512	log plain
-rw-r--r--	fc_simplex.cpp	27591	log plain
-rw-r--r--	fc_simplex.h	8798	log plain
-rw-r--r--	infer_bounds.cpp	8227	log plain
-rw-r--r--	infer_bounds.h	3982	log plain
-rw-r--r--	kinds	4826	log plain
-rw-r--r--	linear_equality.cpp	46674	log plain
-rw-r--r--	linear_equality.h	23687	log plain
-rw-r--r--	matrix.cpp	1000	log plain
-rw-r--r--	matrix.h	25322	log plain
-rw-r--r--	normal_form.cpp	36062	log plain
-rw-r--r--	normal_form.h	37867	log plain
-rw-r--r--	partial_model.cpp	17891	log plain
-rw-r--r--	partial_model.h	11699	log plain
-rw-r--r--	pseudoboolean_proc.cpp	9041	log plain
-rw-r--r--	pseudoboolean_proc.h	2872	log plain
-rw-r--r--	simplex.cpp	9116	log plain
-rw-r--r--	simplex.h	7885	log plain
-rw-r--r--	simplex_update.cpp	5092	log plain
-rw-r--r--	simplex_update.h	10397	log plain
-rw-r--r--	soi_simplex.cpp	33854	log plain
-rw-r--r--	soi_simplex.h	8634	log plain
-rw-r--r--	tableau.cpp	5524	log plain
-rw-r--r--	tableau.h	4558	log plain
-rw-r--r--	tableau_sizes.cpp	1023	log plain
-rw-r--r--	tableau_sizes.h	1071	log plain
-rw-r--r--	theory_arith.cpp	4130	log plain
-rw-r--r--	theory_arith.h	2542	log plain
-rw-r--r--	theory_arith_private.cpp	196560	log plain
-rw-r--r--	theory_arith_private.h	27448	log plain
-rw-r--r--	theory_arith_private_forward.h	816	log plain
-rw-r--r--	theory_arith_type_rules.h	5706	log plain
-rw-r--r--	type_enumerator.h	4295	log plain