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	842	log plain
-rw-r--r--	arith_priority_queue.cpp	8245	log plain
-rw-r--r--	arith_priority_queue.h	8438	log plain
-rw-r--r--	arith_prop_manager.cpp	4691	log plain
-rw-r--r--	arith_prop_manager.h	3652	log plain
-rw-r--r--	arith_rewriter.cpp	9859	log plain
-rw-r--r--	arith_rewriter.h	2384	log plain
-rw-r--r--	arith_static_learner.cpp	15786	log plain
-rw-r--r--	arith_static_learner.h	3190	log plain
-rw-r--r--	arith_utilities.h	7337	log plain
-rw-r--r--	arithvar_node_map.h	2189	log plain
-rw-r--r--	arithvar_set.h	7784	log plain
-rw-r--r--	atom_database.cpp	16095	log plain
-rw-r--r--	atom_database.h	5706	log plain
-rw-r--r--	delta_rational.cpp	1092	log plain
-rw-r--r--	delta_rational.h	2966	log plain
-rw-r--r--	dio_solver.cpp	4058	log plain
-rw-r--r--	dio_solver.h	1893	log plain
-rw-r--r--	kinds	1812	log plain
-rw-r--r--	normal_form.cpp	9489	log plain
-rw-r--r--	normal_form.h	20162	log plain
-rw-r--r--	ordered_set.h	2330	log plain
-rw-r--r--	partial_model.cpp	8564	log plain
-rw-r--r--	partial_model.h	4962	log plain
-rw-r--r--	simplex.cpp	33799	log plain
-rw-r--r--	simplex.h	11255	log plain
-rw-r--r--	tableau.cpp	15533	log plain
-rw-r--r--	tableau.h	9660	log plain
-rw-r--r--	theory_arith.cpp	36117	log plain
-rw-r--r--	theory_arith.h	8912	log plain
-rw-r--r--	theory_arith_type_rules.h	2962	log plain