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	892	log plain
-rw-r--r--	arith_priority_queue.cpp	8923	log plain
-rw-r--r--	arith_priority_queue.h	9114	log plain
-rw-r--r--	arith_prop_manager.cpp	5371	log plain
-rw-r--r--	arith_prop_manager.h	5210	log plain
-rw-r--r--	arith_rewriter.cpp	9865	log plain
-rw-r--r--	arith_rewriter.h	2533	log plain
-rw-r--r--	arith_static_learner.cpp	15883	log plain
-rw-r--r--	arith_static_learner.h	3194	log plain
-rw-r--r--	arith_utilities.h	7534	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	16104	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	3134	log plain
-rw-r--r--	difference_manager.cpp	2561	log plain
-rw-r--r--	difference_manager.h	2241	log plain
-rw-r--r--	dio_solver.cpp	4058	log plain
-rw-r--r--	dio_solver.h	1893	log plain
-rw-r--r--	kinds	2633	log plain
-rw-r--r--	normal_form.cpp	9496	log plain
-rw-r--r--	normal_form.h	20540	log plain
-rw-r--r--	ordered_set.h	3163	log plain
-rw-r--r--	partial_model.cpp	9418	log plain
-rw-r--r--	partial_model.h	5386	log plain
-rw-r--r--	simplex.cpp	34468	log plain
-rw-r--r--	simplex.h	11915	log plain
-rw-r--r--	tableau.cpp	15542	log plain
-rw-r--r--	tableau.h	9727	log plain
-rw-r--r--	theory_arith.cpp	40636	log plain
-rw-r--r--	theory_arith.h	10211	log plain
-rw-r--r--	theory_arith_type_rules.h	2968	log plain