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	92133	log plain
-rw-r--r--	approx_simplex.h	5002	log plain
-rw-r--r--	arith_ite_utils.cpp	12865	log plain
-rw-r--r--	arith_ite_utils.h	3146	log plain
-rw-r--r--	arith_msum.cpp	7770	log plain
-rw-r--r--	arith_msum.h	6696	log plain
-rw-r--r--	arith_preprocess.cpp	2433	log plain
-rw-r--r--	arith_preprocess.h	3075	log plain
-rw-r--r--	arith_rewriter.cpp	30686	log plain
-rw-r--r--	arith_rewriter.h	2883	log plain
-rw-r--r--	arith_state.cpp	1029	log plain
-rw-r--r--	arith_state.h	1585	log plain
-rw-r--r--	arith_static_learner.cpp	8181	log plain
-rw-r--r--	arith_static_learner.h	2039	log plain
-rw-r--r--	arith_utilities.cpp	7100	log plain
-rw-r--r--	arith_utilities.h	9510	log plain
-rw-r--r--	arithvar.cpp	1074	log plain
-rw-r--r--	arithvar.h	1307	log plain
-rw-r--r--	arithvar_node_map.h	2458	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5140	log plain
-rw-r--r--	attempt_solution_simplex.h	3682	log plain
-rw-r--r--	bound_counts.h	7895	log plain
-rw-r--r--	bound_inference.cpp	7608	log plain
-rw-r--r--	bound_inference.h	3750	log plain
-rw-r--r--	branch_and_bound.cpp	5118	log plain
-rw-r--r--	branch_and_bound.h	2150	log plain
-rw-r--r--	callbacks.cpp	5621	log plain
-rw-r--r--	callbacks.h	4999	log plain
-rw-r--r--	congruence_manager.cpp	23637	log plain
-rw-r--r--	congruence_manager.h	9527	log plain
-rw-r--r--	constraint.cpp	73724	log plain
-rw-r--r--	constraint.h	40080	log plain
-rw-r--r--	constraint_forward.h	1646	log plain
-rw-r--r--	cut_log.cpp	17014	log plain
-rw-r--r--	cut_log.h	7047	log plain
-rw-r--r--	delta_rational.cpp	3222	log plain
-rw-r--r--	delta_rational.h	7743	log plain
-rw-r--r--	dio_solver.cpp	25435	log plain
-rw-r--r--	dio_solver.h	12687	log plain
-rw-r--r--	dual_simplex.cpp	9017	log plain
-rw-r--r--	dual_simplex.h	4222	log plain
-rw-r--r--	equality_solver.cpp	3880	log plain
-rw-r--r--	equality_solver.h	3470	log plain
-rw-r--r--	error_set.cpp	13272	log plain
-rw-r--r--	error_set.h	10600	log plain
-rw-r--r--	fc_simplex.cpp	27255	log plain
-rw-r--r--	fc_simplex.h	8892	log plain
-rw-r--r--	infer_bounds.cpp	6966	log plain
-rw-r--r--	infer_bounds.h	3985	log plain
-rw-r--r--	inference_manager.cpp	4841	log plain
-rw-r--r--	inference_manager.h	4457	log plain
-rw-r--r--	kinds	7663	log plain
-rw-r--r--	linear_equality.cpp	46119	log plain
-rw-r--r--	linear_equality.h	23755	log plain
-rw-r--r--	matrix.cpp	964	log plain
-rw-r--r--	matrix.h	25398	log plain
d---------	nl	1073	log plain
-rw-r--r--	normal_form.cpp	38588	log plain
-rw-r--r--	normal_form.h	37826	log plain
-rw-r--r--	operator_elim.cpp	14729	log plain
-rw-r--r--	operator_elim.h	5081	log plain
-rw-r--r--	partial_model.cpp	18032	log plain
-rw-r--r--	partial_model.h	12137	log plain
-rw-r--r--	pp_rewrite_eq.cpp	1869	log plain
-rw-r--r--	pp_rewrite_eq.h	1664	log plain
-rw-r--r--	proof_checker.cpp	12374	log plain
-rw-r--r--	proof_checker.h	1449	log plain
-rw-r--r--	proof_macros.h	1134	log plain
-rw-r--r--	rewrites.cpp	1567	log plain
-rw-r--r--	rewrites.h	2233	log plain
-rw-r--r--	simplex.cpp	9366	log plain
-rw-r--r--	simplex.h	7936	log plain
-rw-r--r--	simplex_update.cpp	5557	log plain
-rw-r--r--	simplex_update.h	10522	log plain
-rw-r--r--	soi_simplex.cpp	33414	log plain
-rw-r--r--	soi_simplex.h	8738	log plain
-rw-r--r--	tableau.cpp	5558	log plain
-rw-r--r--	tableau.h	4608	log plain
-rw-r--r--	tableau_sizes.cpp	1052	log plain
-rw-r--r--	tableau_sizes.h	1080	log plain
-rw-r--r--	theory_arith.cpp	11367	log plain
-rw-r--r--	theory_arith.h	5456	log plain
-rw-r--r--	theory_arith_private.cpp	168769	log plain
-rw-r--r--	theory_arith_private.h	29382	log plain
-rw-r--r--	theory_arith_type_rules.cpp	5130	log plain
-rw-r--r--	theory_arith_type_rules.h	1827	log plain
-rw-r--r--	type_enumerator.h	2974	log plain