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	9133	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	10135	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	7687	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	3978	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	24179	log plain
-rw-r--r--	dio_solver.h	12715	log plain
-rw-r--r--	kinds	2633	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	3163	log plain
-rw-r--r--	partial_model.cpp	9594	log plain
-rw-r--r--	partial_model.h	5420	log plain
-rw-r--r--	simplex.cpp	34486	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	40589	log plain
-rw-r--r--	theory_arith.h	12062	log plain
-rw-r--r--	theory_arith_type_rules.h	3028	log plain