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	881	log plain
-rw-r--r--	arith_priority_queue.cpp	9139	log plain
-rw-r--r--	arith_priority_queue.h	9089	log plain
-rw-r--r--	arith_rewriter.cpp	9010	log plain
-rw-r--r--	arith_rewriter.h	2379	log plain
-rw-r--r--	arith_static_learner.cpp	14671	log plain
-rw-r--r--	arith_static_learner.h	3194	log plain
-rw-r--r--	arith_utilities.h	7055	log plain
-rw-r--r--	arithvar.h	1926	log plain
-rw-r--r--	arithvar_node_map.h	2186	log plain
-rw-r--r--	congruence_manager.cpp	9640	log plain
-rw-r--r--	congruence_manager.h	6413	log plain
-rw-r--r--	constraint.cpp	30908	log plain
-rw-r--r--	constraint.h	23801	log plain
-rw-r--r--	constraint_forward.h	1374	log plain
-rw-r--r--	delta_rational.cpp	1098	log plain
-rw-r--r--	delta_rational.h	4522	log plain
-rw-r--r--	dio_solver.cpp	24847	log plain
-rw-r--r--	dio_solver.h	12210	log plain
-rw-r--r--	kinds	3101	log plain
-rw-r--r--	linear_equality.cpp	10004	log plain
-rw-r--r--	linear_equality.h	4862	log plain
-rw-r--r--	matrix.cpp	16152	log plain
-rw-r--r--	matrix.h	22444	log plain
-rw-r--r--	normal_form.cpp	34858	log plain
-rw-r--r--	normal_form.h	34842	log plain
-rw-r--r--	partial_model.cpp	8115	log plain
-rw-r--r--	partial_model.h	5755	log plain
-rw-r--r--	simplex.cpp	18214	log plain
-rw-r--r--	simplex.h	10150	log plain
-rw-r--r--	theory_arith.cpp	59285	log plain
-rw-r--r--	theory_arith.h	13751	log plain
-rw-r--r--	theory_arith_type_rules.h	4154	log plain