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	901	log plain
-rw-r--r--	arith_priority_queue.cpp	9139	log plain
-rw-r--r--	arith_priority_queue.h	9107	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	1896	log plain
-rw-r--r--	arithvar_node_map.h	2186	log plain
-rw-r--r--	arithvar_set.h	8493	log plain
-rw-r--r--	constraint.cpp	30853	log plain
-rw-r--r--	constraint.h	23563	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--	difference_manager.cpp	6871	log plain
-rw-r--r--	difference_manager.h	5816	log plain
-rw-r--r--	dio_solver.cpp	24701	log plain
-rw-r--r--	dio_solver.h	12211	log plain
-rw-r--r--	kinds	3315	log plain
-rw-r--r--	linear_equality.cpp	10834	log plain
-rw-r--r--	linear_equality.h	4863	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	17834	log plain
-rw-r--r--	simplex.h	10110	log plain
-rw-r--r--	tableau.cpp	15493	log plain
-rw-r--r--	tableau.h	9720	log plain
-rw-r--r--	theory_arith.cpp	58608	log plain
-rw-r--r--	theory_arith.h	13882	log plain
-rw-r--r--	theory_arith_type_rules.h	4059	log plain