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	9432	log plain
-rw-r--r--	arith_rewriter.h	2379	log plain
-rw-r--r--	arith_static_learner.cpp	15927	log plain
-rw-r--r--	arith_static_learner.h	3194	log plain
-rw-r--r--	arith_utilities.h	7832	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	9822	log plain
-rw-r--r--	congruence_manager.h	5667	log plain
-rw-r--r--	constraint.cpp	30823	log plain
-rw-r--r--	constraint.h	23573	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	24765	log plain
-rw-r--r--	dio_solver.h	12210	log plain
-rw-r--r--	kinds	3315	log plain
-rw-r--r--	linear_equality.cpp	10694	log plain
-rw-r--r--	linear_equality.h	4862	log plain
-rw-r--r--	matrix.cpp	16116	log plain
-rw-r--r--	matrix.h	22333	log plain
-rw-r--r--	normal_form.cpp	34858	log plain
-rw-r--r--	normal_form.h	34873	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	17840	log plain
-rw-r--r--	simplex.h	10095	log plain
-rw-r--r--	theory_arith.cpp	59603	log plain
-rw-r--r--	theory_arith.h	13664	log plain
-rw-r--r--	theory_arith_type_rules.h	4059	log plain