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	92523	log plain
-rw-r--r--	approx_simplex.h	5038	log plain
-rw-r--r--	arith_ite_utils.cpp	12861	log plain
-rw-r--r--	arith_ite_utils.h	3203	log plain
-rw-r--r--	arith_msum.cpp	7695	log plain
-rw-r--r--	arith_msum.h	6642	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	29172	log plain
-rw-r--r--	arith_rewriter.h	2563	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	8299	log plain
-rw-r--r--	arith_static_learner.h	2073	log plain
-rw-r--r--	arith_utilities.cpp	7126	log plain
-rw-r--r--	arith_utilities.h	10099	log plain
-rw-r--r--	arithvar.cpp	1058	log plain
-rw-r--r--	arithvar.h	1291	log plain
-rw-r--r--	arithvar_node_map.h	2450	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5374	log plain
-rw-r--r--	attempt_solution_simplex.h	3737	log plain
-rw-r--r--	bound_counts.h	7881	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	5459	log plain
-rw-r--r--	callbacks.h	4982	log plain
-rw-r--r--	congruence_manager.cpp	23573	log plain
-rw-r--r--	congruence_manager.h	9432	log plain
-rw-r--r--	constraint.cpp	74039	log plain
-rw-r--r--	constraint.h	40177	log plain
-rw-r--r--	constraint_forward.h	1640	log plain
-rw-r--r--	cut_log.cpp	16994	log plain
-rw-r--r--	cut_log.h	7010	log plain
-rw-r--r--	delta_rational.cpp	3212	log plain
-rw-r--r--	delta_rational.h	7732	log plain
-rw-r--r--	dio_solver.cpp	25734	log plain
-rw-r--r--	dio_solver.h	12769	log plain
-rw-r--r--	dual_simplex.cpp	9520	log plain
-rw-r--r--	dual_simplex.h	4265	log plain
-rw-r--r--	error_set.cpp	13810	log plain
-rw-r--r--	error_set.h	10605	log plain
-rw-r--r--	fc_simplex.cpp	28062	log plain
-rw-r--r--	fc_simplex.h	8908	log plain
-rw-r--r--	infer_bounds.cpp	6916	log plain
-rw-r--r--	infer_bounds.h	3941	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	46878	log plain
-rw-r--r--	linear_equality.h	23814	log plain
-rw-r--r--	matrix.cpp	1008	log plain
-rw-r--r--	matrix.h	25381	log plain
d---------	nl	989	log plain
-rw-r--r--	normal_form.cpp	38468	log plain
-rw-r--r--	normal_form.h	37731	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	18021	log plain
-rw-r--r--	partial_model.h	12125	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	1121	log plain
-rw-r--r--	rewrites.cpp	1548	log plain
-rw-r--r--	rewrites.h	2212	log plain
-rw-r--r--	simplex.cpp	9313	log plain
-rw-r--r--	simplex.h	7985	log plain
-rw-r--r--	simplex_update.cpp	5100	log plain
-rw-r--r--	simplex_update.h	10526	log plain
-rw-r--r--	soi_simplex.cpp	34373	log plain
-rw-r--r--	soi_simplex.h	8755	log plain
-rw-r--r--	tableau.cpp	5541	log plain
-rw-r--r--	tableau.h	4589	log plain
-rw-r--r--	tableau_sizes.cpp	1041	log plain
-rw-r--r--	tableau_sizes.h	1067	log plain
-rw-r--r--	theory_arith.cpp	10172	log plain
-rw-r--r--	theory_arith.h	5517	log plain
-rw-r--r--	theory_arith_private.cpp	196344	log plain
-rw-r--r--	theory_arith_private.h	29807	log plain
-rw-r--r--	theory_arith_type_rules.h	4865	log plain
-rw-r--r--	type_enumerator.h	3007	log plain