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	92129	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_lemma.cpp	814	log plain
-rw-r--r--	arith_lemma.h	1699	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	2021	log plain
-rw-r--r--	arith_preprocess.h	2686	log plain
-rw-r--r--	arith_rewriter.cpp	29176	log plain
-rw-r--r--	arith_rewriter.h	2612	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	8345	log plain
-rw-r--r--	arith_static_learner.h	2063	log plain
-rw-r--r--	arith_utilities.cpp	7089	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	5261	log plain
-rw-r--r--	attempt_solution_simplex.h	3751	log plain
-rw-r--r--	bound_counts.h	7925	log plain
-rw-r--r--	bound_inference.cpp	7550	log plain
-rw-r--r--	bound_inference.h	3736	log plain
-rw-r--r--	callbacks.cpp	5433	log plain
-rw-r--r--	callbacks.h	4967	log plain
-rw-r--r--	congruence_manager.cpp	23346	log plain
-rw-r--r--	congruence_manager.h	9381	log plain
-rw-r--r--	constraint.cpp	73688	log plain
-rw-r--r--	constraint.h	39908	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	3194	log plain
-rw-r--r--	delta_rational.h	7720	log plain
-rw-r--r--	dio_solver.cpp	25701	log plain
-rw-r--r--	dio_solver.h	12819	log plain
-rw-r--r--	dual_simplex.cpp	9348	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	27840	log plain
-rw-r--r--	fc_simplex.h	8824	log plain
-rw-r--r--	infer_bounds.cpp	6919	log plain
-rw-r--r--	infer_bounds.h	3972	log plain
-rw-r--r--	inference_id.cpp	2368	log plain
-rw-r--r--	inference_id.h	3622	log plain
-rw-r--r--	inference_manager.cpp	4479	log plain
-rw-r--r--	inference_manager.h	4174	log plain
-rw-r--r--	kinds	6879	log plain
-rw-r--r--	linear_equality.cpp	46893	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	1052	log plain
-rw-r--r--	normal_form.cpp	38466	log plain
-rw-r--r--	normal_form.h	37773	log plain
-rw-r--r--	operator_elim.cpp	16675	log plain
-rw-r--r--	operator_elim.h	4938	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	1315	log plain
-rw-r--r--	rewrites.cpp	1548	log plain
-rw-r--r--	rewrites.h	2212	log plain
-rw-r--r--	simplex.cpp	9174	log plain
-rw-r--r--	simplex.h	7989	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	34102	log plain
-rw-r--r--	soi_simplex.h	8706	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	1112	log plain
-rw-r--r--	theory_arith.cpp	9574	log plain
-rw-r--r--	theory_arith.h	5195	log plain
-rw-r--r--	theory_arith_private.cpp	190710	log plain
-rw-r--r--	theory_arith_private.h	29366	log plain
-rw-r--r--	theory_arith_type_rules.h	4201	log plain
-rw-r--r--	type_enumerator.h	3030	log plain