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	8923	log plain
-rw-r--r--	arith_priority_queue.h	9114	log plain
-rw-r--r--	arith_prop_manager.cpp	5364	log plain
-rw-r--r--	arith_prop_manager.h	4323	log plain
-rw-r--r--	arith_rewriter.cpp	9865	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	3194	log plain
-rw-r--r--	arith_utilities.h	7371	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	2972	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	20177	log plain
-rw-r--r--	ordered_set.h	3163	log plain
-rw-r--r--	partial_model.cpp	8570	log plain
-rw-r--r--	partial_model.h	4994	log plain
-rw-r--r--	simplex.cpp	34461	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	36226	log plain
-rw-r--r--	theory_arith.h	8941	log plain
-rw-r--r--	theory_arith_type_rules.h	2968	log plain