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--	Makefile	79	log plain
-rw-r--r--	Makefile.am	1513	log plain
-rw-r--r--	approx_simplex.cpp	15827	log plain
-rw-r--r--	approx_simplex.h	2625	log plain
-rw-r--r--	arith_heuristic_pivot_rule.cpp	1049	log plain
-rw-r--r--	arith_heuristic_pivot_rule.h	1063	log plain
-rw-r--r--	arith_propagation_mode.cpp	1093	log plain
-rw-r--r--	arith_propagation_mode.h	1050	log plain
-rw-r--r--	arith_rewriter.cpp	10477	log plain
-rw-r--r--	arith_rewriter.h	2226	log plain
-rw-r--r--	arith_static_learner.cpp	8771	log plain
-rw-r--r--	arith_static_learner.h	2063	log plain
-rw-r--r--	arith_unate_lemma_mode.cpp	1173	log plain
-rw-r--r--	arith_unate_lemma_mode.h	1089	log plain
-rw-r--r--	arith_utilities.h	6658	log plain
-rw-r--r--	arithvar.cpp	858	log plain
-rw-r--r--	arithvar.h	1224	log plain
-rw-r--r--	arithvar_node_map.h	2441	log plain
-rw-r--r--	bound_counts.cpp	397	log plain
-rw-r--r--	bound_counts.h	7677	log plain
-rw-r--r--	callbacks.cpp	840	log plain
-rw-r--r--	callbacks.h	1993	log plain
-rw-r--r--	congruence_manager.cpp	10749	log plain
-rw-r--r--	congruence_manager.h	7218	log plain
-rw-r--r--	constraint.cpp	41666	log plain
-rw-r--r--	constraint.h	26044	log plain
-rw-r--r--	constraint_forward.h	1305	log plain
-rw-r--r--	delta_rational.cpp	3140	log plain
-rw-r--r--	delta_rational.h	7434	log plain
-rw-r--r--	dio_solver.cpp	25057	log plain
-rw-r--r--	dio_solver.h	12638	log plain
-rw-r--r--	dual_simplex.cpp	8976	log plain
-rw-r--r--	dual_simplex.h	4203	log plain
-rw-r--r--	error_set.cpp	13127	log plain
-rw-r--r--	error_set.h	10397	log plain
-rw-r--r--	fc_simplex.cpp	27863	log plain
-rw-r--r--	fc_simplex.h	8729	log plain
-rw-r--r--	kinds	3643	log plain
-rw-r--r--	linear_equality.cpp	48829	log plain
-rw-r--r--	linear_equality.h	22735	log plain
-rw-r--r--	matrix.cpp	1000	log plain
-rw-r--r--	matrix.h	24389	log plain
-rw-r--r--	normal_form.cpp	29032	log plain
-rw-r--r--	normal_form.h	35530	log plain
-rw-r--r--	options	5396	log plain
-rw-r--r--	options_handlers.h	4052	log plain
-rw-r--r--	partial_model.cpp	14426	log plain
-rw-r--r--	partial_model.h	11888	log plain
-rw-r--r--	pure_update_simplex.cpp	9076	log plain
-rw-r--r--	pure_update_simplex.h	4263	log plain
-rw-r--r--	simplex-converge.cpp	59741	log plain
-rw-r--r--	simplex-converge.h	18035	log plain
-rw-r--r--	simplex.cpp	8154	log plain
-rw-r--r--	simplex.h	7515	log plain
-rw-r--r--	simplex_update.cpp	5076	log plain
-rw-r--r--	simplex_update.h	10383	log plain
-rw-r--r--	soi_simplex.cpp	26005	log plain
-rw-r--r--	soi_simplex.h	8227	log plain
-rw-r--r--	tableau.cpp	4884	log plain
-rw-r--r--	tableau.h	3890	log plain
-rw-r--r--	tableau_sizes.cpp	408	log plain
-rw-r--r--	tableau_sizes.h	483	log plain
-rw-r--r--	theory_arith.cpp	2465	log plain
-rw-r--r--	theory_arith.h	2093	log plain
-rw-r--r--	theory_arith_private.cpp	91225	log plain
-rw-r--r--	theory_arith_private.h	18044	log plain
-rw-r--r--	theory_arith_private_forward.h	213	log plain
-rw-r--r--	theory_arith_type_rules.h	4093	log plain
-rw-r--r--	type_enumerator.h	4295	log plain