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	92130	log plain
-rw-r--r--	approx_simplex.h	5053	log plain
-rw-r--r--	arith_ite_utils.cpp	12886	log plain
-rw-r--r--	arith_ite_utils.h	3227	log plain
-rw-r--r--	arith_msum.cpp	7706	log plain
-rw-r--r--	arith_msum.h	6653	log plain
-rw-r--r--	arith_rewriter.cpp	26656	log plain
-rw-r--r--	arith_rewriter.h	2422	log plain
-rw-r--r--	arith_state.cpp	1075	log plain
-rw-r--r--	arith_state.h	1597	log plain
-rw-r--r--	arith_static_learner.cpp	8346	log plain
-rw-r--r--	arith_static_learner.h	2064	log plain
-rw-r--r--	arith_utilities.cpp	6194	log plain
-rw-r--r--	arith_utilities.h	9969	log plain
-rw-r--r--	arithvar.cpp	1083	log plain
-rw-r--r--	arithvar.h	1313	log plain
-rw-r--r--	arithvar_node_map.h	2474	log plain
-rw-r--r--	attempt_solution_simplex.cpp	5262	log plain
-rw-r--r--	attempt_solution_simplex.h	3752	log plain
-rw-r--r--	bound_counts.h	7926	log plain
-rw-r--r--	callbacks.cpp	5378	log plain
-rw-r--r--	callbacks.h	4874	log plain
-rw-r--r--	congruence_manager.cpp	15077	log plain
-rw-r--r--	congruence_manager.h	5747	log plain
-rw-r--r--	constraint.cpp	60784	log plain
-rw-r--r--	constraint.h	38044	log plain
-rw-r--r--	constraint_forward.h	1657	log plain
-rw-r--r--	cut_log.cpp	16999	log plain
-rw-r--r--	cut_log.h	7119	log plain
-rw-r--r--	delta_rational.cpp	3195	log plain
-rw-r--r--	delta_rational.h	7721	log plain
-rw-r--r--	dio_solver.cpp	25702	log plain
-rw-r--r--	dio_solver.h	12820	log plain
-rw-r--r--	dual_simplex.cpp	9349	log plain
-rw-r--r--	dual_simplex.h	4279	log plain
-rw-r--r--	error_set.cpp	13834	log plain
-rw-r--r--	error_set.h	10650	log plain
-rw-r--r--	fc_simplex.cpp	27841	log plain
-rw-r--r--	fc_simplex.h	8825	log plain
-rw-r--r--	infer_bounds.cpp	6903	log plain
-rw-r--r--	infer_bounds.h	3956	log plain
-rw-r--r--	kinds	6194	log plain
-rw-r--r--	linear_equality.cpp	46894	log plain
-rw-r--r--	linear_equality.h	23805	log plain
-rw-r--r--	matrix.cpp	1033	log plain
-rw-r--r--	matrix.h	25408	log plain
d---------	nl	1064	log plain
-rw-r--r--	normal_form.cpp	36883	log plain
-rw-r--r--	normal_form.h	36884	log plain
-rw-r--r--	operator_elim.cpp	16670	log plain
-rw-r--r--	operator_elim.h	4909	log plain
-rw-r--r--	partial_model.cpp	18045	log plain
-rw-r--r--	partial_model.h	12158	log plain
-rw-r--r--	proof_checker.cpp	8652	log plain
-rw-r--r--	proof_checker.h	1461	log plain
-rw-r--r--	proof_macros.h	1316	log plain
-rw-r--r--	simplex.cpp	9175	log plain
-rw-r--r--	simplex.h	7990	log plain
-rw-r--r--	simplex_update.cpp	5125	log plain
-rw-r--r--	simplex_update.h	10551	log plain
-rw-r--r--	soi_simplex.cpp	34103	log plain
-rw-r--r--	soi_simplex.h	8707	log plain
-rw-r--r--	tableau.cpp	5565	log plain
-rw-r--r--	tableau.h	4615	log plain
-rw-r--r--	tableau_sizes.cpp	1065	log plain
-rw-r--r--	tableau_sizes.h	1113	log plain
-rw-r--r--	theory_arith.cpp	4884	log plain
-rw-r--r--	theory_arith.h	3606	log plain
-rw-r--r--	theory_arith_private.cpp	191553	log plain
-rw-r--r--	theory_arith_private.h	27738	log plain
-rw-r--r--	theory_arith_private_forward.h	858	log plain
-rw-r--r--	theory_arith_type_rules.h	4169	log plain
-rw-r--r--	type_enumerator.h	3031	log plain