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	945	log plain
-rw-r--r--	arith_priority_queue.cpp	10489	log plain
-rw-r--r--	arith_priority_queue.h	9606	log plain
-rw-r--r--	arith_rewriter.cpp	9010	log plain
-rw-r--r--	arith_rewriter.h	2230	log plain
-rw-r--r--	arith_static_learner.cpp	13022	log plain
-rw-r--r--	arith_static_learner.h	3094	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	9997	log plain
-rw-r--r--	congruence_manager.h	7114	log plain
-rw-r--r--	constraint.cpp	39439	log plain
-rw-r--r--	constraint.h	25265	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	4596	log plain
-rw-r--r--	dio_solver.cpp	25000	log plain
-rw-r--r--	dio_solver.h	12210	log plain
-rw-r--r--	kinds	2870	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	22637	log plain
-rw-r--r--	normal_form.cpp	28294	log plain
-rw-r--r--	normal_form.h	35016	log plain
-rw-r--r--	partial_model.cpp	8141	log plain
-rw-r--r--	partial_model.h	5755	log plain
-rw-r--r--	simplex.cpp	20761	log plain
-rw-r--r--	simplex.h	10619	log plain
-rw-r--r--	theory_arith.cpp	78109	log plain
-rw-r--r--	theory_arith.h	15914	log plain
-rw-r--r--	theory_arith_instantiator.cpp	18745	log plain
-rw-r--r--	theory_arith_instantiator.h	4219	log plain
-rw-r--r--	theory_arith_type_rules.h	4088	log plain