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	92617	log plain
-rw-r--r--	approx_simplex.h	5062	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	2481	log plain
-rw-r--r--	arith_preprocess.h	3048	log plain
-rw-r--r--	arith_rewriter.cpp	29195	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	2096	log plain
-rw-r--r--	arith_utilities.cpp	7126	log plain
-rw-r--r--	arith_utilities.h	10122	log plain
-rw-r--r--	arithvar.cpp	1081	log plain
-rw-r--r--	arithvar.h	1315	log plain
-rw-r--r--	arithvar_node_map.h	2473	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5397	log plain
-rw-r--r--	attempt_solution_simplex.h	3760	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	5482	log plain
-rw-r--r--	callbacks.h	5005	log plain
-rw-r--r--	congruence_manager.cpp	23596	log plain
-rw-r--r--	congruence_manager.h	9455	log plain
-rw-r--r--	constraint.cpp	74062	log plain
-rw-r--r--	constraint.h	40201	log plain
-rw-r--r--	constraint_forward.h	1663	log plain
-rw-r--r--	cut_log.cpp	17017	log plain
-rw-r--r--	cut_log.h	7035	log plain
-rw-r--r--	delta_rational.cpp	3213	log plain
-rw-r--r--	delta_rational.h	7720	log plain
-rw-r--r--	dio_solver.cpp	25757	log plain
-rw-r--r--	dio_solver.h	12792	log plain
-rw-r--r--	dual_simplex.cpp	9543	log plain
-rw-r--r--	dual_simplex.h	4288	log plain
-rw-r--r--	error_set.cpp	13833	log plain
-rw-r--r--	error_set.h	10628	log plain
-rw-r--r--	fc_simplex.cpp	28085	log plain
-rw-r--r--	fc_simplex.h	8931	log plain
-rw-r--r--	infer_bounds.cpp	6919	log plain
-rw-r--r--	infer_bounds.h	3945	log plain
-rw-r--r--	inference_manager.cpp	4359	log plain
-rw-r--r--	inference_manager.h	4034	log plain
-rw-r--r--	kinds	7575	log plain
-rw-r--r--	linear_equality.cpp	46901	log plain
-rw-r--r--	linear_equality.h	23837	log plain
-rw-r--r--	matrix.cpp	1031	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	37755	log plain
-rw-r--r--	operator_elim.cpp	15444	log plain
-rw-r--r--	operator_elim.h	5303	log plain
-rw-r--r--	partial_model.cpp	18044	log plain
-rw-r--r--	partial_model.h	12149	log plain
-rw-r--r--	proof_checker.cpp	11937	log plain
-rw-r--r--	proof_checker.h	1431	log plain
-rw-r--r--	proof_macros.h	1097	log plain
-rw-r--r--	rewrites.cpp	1548	log plain
-rw-r--r--	rewrites.h	2212	log plain
-rw-r--r--	simplex.cpp	9325	log plain
-rw-r--r--	simplex.h	8008	log plain
-rw-r--r--	simplex_update.cpp	5123	log plain
-rw-r--r--	simplex_update.h	10549	log plain
-rw-r--r--	soi_simplex.cpp	34345	log plain
-rw-r--r--	soi_simplex.h	8778	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	1091	log plain
-rw-r--r--	theory_arith.cpp	10195	log plain
-rw-r--r--	theory_arith.h	5540	log plain
-rw-r--r--	theory_arith_private.cpp	196367	log plain
-rw-r--r--	theory_arith_private.h	29830	log plain
-rw-r--r--	theory_arith_type_rules.h	4888	log plain
-rw-r--r--	type_enumerator.h	3030	log plain