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	741	log plain
-rw-r--r--	arith_priority_queue.cpp	8245	log plain
-rw-r--r--	arith_priority_queue.h	8438	log plain
-rw-r--r--	arith_rewriter.cpp	9795	log plain
-rw-r--r--	arith_rewriter.h	2384	log plain
-rw-r--r--	arith_static_learner.cpp	9528	log plain
-rw-r--r--	arith_static_learner.h	1570	log plain
-rw-r--r--	arith_utilities.h	6068	log plain
-rw-r--r--	arithvar_set.h	4223	log plain
-rw-r--r--	delta_rational.cpp	1092	log plain
-rw-r--r--	delta_rational.h	2966	log plain
-rw-r--r--	kinds	1171	log plain
-rw-r--r--	normal_form.cpp	8279	log plain
-rw-r--r--	normal_form.h	19418	log plain
-rw-r--r--	ordered_set.h	474	log plain
-rw-r--r--	partial_model.cpp	7767	log plain
-rw-r--r--	partial_model.h	4591	log plain
-rw-r--r--	simplex.cpp	26140	log plain
-rw-r--r--	simplex.h	9543	log plain
-rw-r--r--	tableau.cpp	15512	log plain
-rw-r--r--	tableau.h	9610	log plain
-rw-r--r--	theory_arith.cpp	22530	log plain
-rw-r--r--	theory_arith.h	7419	log plain
-rw-r--r--	theory_arith_type_rules.h	2962	log plain
-rw-r--r--	unate_propagator.cpp	12560	log plain
-rw-r--r--	unate_propagator.h	5063	log plain