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	92645	log plain
-rw-r--r--	approx_simplex.h	5052	log plain
-rw-r--r--	arith_ite_utils.cpp	12885	log plain
-rw-r--r--	arith_ite_utils.h	3226	log plain
-rw-r--r--	arith_msum.cpp	7705	log plain
-rw-r--r--	arith_msum.h	6652	log plain
-rw-r--r--	arith_preprocess.cpp	2395	log plain
-rw-r--r--	arith_preprocess.h	3099	log plain
-rw-r--r--	arith_rewriter.cpp	29176	log plain
-rw-r--r--	arith_rewriter.h	2586	log plain
-rw-r--r--	arith_state.cpp	1076	log plain
-rw-r--r--	arith_state.h	1596	log plain
-rw-r--r--	arith_static_learner.cpp	8322	log plain
-rw-r--r--	arith_static_learner.h	2063	log plain
-rw-r--r--	arith_utilities.cpp	7103	log plain
-rw-r--r--	arith_utilities.h	10181	log plain
-rw-r--r--	arithvar.cpp	1082	log plain
-rw-r--r--	arithvar.h	1312	log plain
-rw-r--r--	arithvar_node_map.h	2473	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5321	log plain
-rw-r--r--	attempt_solution_simplex.h	3751	log plain
-rw-r--r--	bound_counts.h	7904	log plain
-rw-r--r--	bound_inference.cpp	7549	log plain
-rw-r--r--	bound_inference.h	3735	log plain
-rw-r--r--	callbacks.cpp	5433	log plain
-rw-r--r--	callbacks.h	4967	log plain
-rw-r--r--	congruence_manager.cpp	23343	log plain
-rw-r--r--	congruence_manager.h	9375	log plain
-rw-r--r--	constraint.cpp	73847	log plain
-rw-r--r--	constraint.h	40197	log plain
-rw-r--r--	constraint_forward.h	1656	log plain
-rw-r--r--	cut_log.cpp	16998	log plain
-rw-r--r--	cut_log.h	7118	log plain
-rw-r--r--	delta_rational.cpp	3214	log plain
-rw-r--r--	delta_rational.h	7720	log plain
-rw-r--r--	dio_solver.cpp	25717	log plain
-rw-r--r--	dio_solver.h	12819	log plain
-rw-r--r--	dual_simplex.cpp	9501	log plain
-rw-r--r--	dual_simplex.h	4278	log plain
-rw-r--r--	error_set.cpp	13833	log plain
-rw-r--r--	error_set.h	10649	log plain
-rw-r--r--	fc_simplex.cpp	28085	log plain
-rw-r--r--	fc_simplex.h	8839	log plain
-rw-r--r--	infer_bounds.cpp	6919	log plain
-rw-r--r--	infer_bounds.h	3972	log plain
-rw-r--r--	inference_manager.cpp	4309	log plain
-rw-r--r--	inference_manager.h	4101	log plain
-rw-r--r--	kinds	7575	log plain
-rw-r--r--	linear_equality.cpp	46901	log plain
-rw-r--r--	linear_equality.h	23804	log plain
-rw-r--r--	matrix.cpp	1032	log plain
-rw-r--r--	matrix.h	25407	log plain
d---------	nl	989	log plain
-rw-r--r--	normal_form.cpp	38466	log plain
-rw-r--r--	normal_form.h	37771	log plain
-rw-r--r--	operator_elim.cpp	15148	log plain
-rw-r--r--	operator_elim.h	5324	log plain
-rw-r--r--	partial_model.cpp	18044	log plain
-rw-r--r--	partial_model.h	12157	log plain
-rw-r--r--	proof_checker.cpp	9224	log plain
-rw-r--r--	proof_checker.h	1460	log plain
-rw-r--r--	proof_macros.h	1056	log plain
-rw-r--r--	rewrites.cpp	1548	log plain
-rw-r--r--	rewrites.h	2212	log plain
-rw-r--r--	simplex.cpp	9210	log plain
-rw-r--r--	simplex.h	7970	log plain
-rw-r--r--	simplex_update.cpp	5124	log plain
-rw-r--r--	simplex_update.h	10550	log plain
-rw-r--r--	soi_simplex.cpp	34289	log plain
-rw-r--r--	soi_simplex.h	8685	log plain
-rw-r--r--	tableau.cpp	5564	log plain
-rw-r--r--	tableau.h	4614	log plain
-rw-r--r--	tableau_sizes.cpp	1064	log plain
-rw-r--r--	tableau_sizes.h	1092	log plain
-rw-r--r--	theory_arith.cpp	10078	log plain
-rw-r--r--	theory_arith.h	5576	log plain
-rw-r--r--	theory_arith_private.cpp	197434	log plain
-rw-r--r--	theory_arith_private.h	29913	log plain
-rw-r--r--	theory_arith_type_rules.h	4896	log plain
-rw-r--r--	type_enumerator.h	3030	log plain