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	950	log plain
-rw-r--r--	arith_priority_queue.cpp	9139	log plain
-rw-r--r--	arith_priority_queue.h	9107	log plain
-rw-r--r--	arith_prop_manager.cpp	5417	log plain
-rw-r--r--	arith_prop_manager.h	5211	log plain
-rw-r--r--	arith_rewriter.cpp	11048	log plain
-rw-r--r--	arith_rewriter.h	2441	log plain
-rw-r--r--	arith_static_learner.cpp	15924	log plain
-rw-r--r--	arith_static_learner.h	3194	log plain
-rw-r--r--	arith_utilities.h	7259	log plain
-rw-r--r--	arithvar.h	1748	log plain
-rw-r--r--	arithvar_node_map.h	2186	log plain
-rw-r--r--	arithvar_set.h	8827	log plain
-rw-r--r--	atom_database.cpp	16144	log plain
-rw-r--r--	atom_database.h	5714	log plain
-rw-r--r--	delta_rational.cpp	1098	log plain
-rw-r--r--	delta_rational.h	4140	log plain
-rw-r--r--	difference_manager.cpp	3002	log plain
-rw-r--r--	difference_manager.h	3477	log plain
-rw-r--r--	dio_solver.cpp	24179	log plain
-rw-r--r--	dio_solver.h	12673	log plain
-rw-r--r--	kinds	3315	log plain
-rw-r--r--	linear_equality.cpp	10005	log plain
-rw-r--r--	linear_equality.h	4791	log plain
-rw-r--r--	normal_form.cpp	17218	log plain
-rw-r--r--	normal_form.h	31480	log plain
-rw-r--r--	ordered_set.h	3004	log plain
-rw-r--r--	partial_model.cpp	10197	log plain
-rw-r--r--	partial_model.h	6216	log plain
-rw-r--r--	simplex.cpp	17585	log plain
-rw-r--r--	simplex.h	10677	log plain
-rw-r--r--	tableau.cpp	15542	log plain
-rw-r--r--	tableau.h	9720	log plain
-rw-r--r--	theory_arith.cpp	48543	log plain
-rw-r--r--	theory_arith.h	14087	log plain
-rw-r--r--	theory_arith_type_rules.h	4059	log plain