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	762	log plain
-rw-r--r--	arith_constants.h	1720	log plain
-rw-r--r--	arith_rewriter.cpp	9451	log plain
-rw-r--r--	arith_rewriter.h	2581	log plain
-rw-r--r--	arith_utilities.h	5957	log plain
-rw-r--r--	arithvar_dense_set.h	1607	log plain
-rw-r--r--	arithvar_set.h	3216	log plain
-rw-r--r--	delta_rational.cpp	1092	log plain
-rw-r--r--	delta_rational.h	2974	log plain
-rw-r--r--	kinds	1171	log plain
-rw-r--r--	normal_form.cpp	8279	log plain
-rw-r--r--	normal_form.h	19460	log plain
-rw-r--r--	normal_form_notes.txt	14880	log plain
-rw-r--r--	ordered_bounds_list.h	6261	log plain
-rw-r--r--	ordered_set.h	715	log plain
-rw-r--r--	partial_model.cpp	7767	log plain
-rw-r--r--	partial_model.h	4591	log plain
-rw-r--r--	row_vector.cpp	4741	log plain
-rw-r--r--	row_vector.h	4511	log plain
-rw-r--r--	simplex.cpp	24294	log plain
-rw-r--r--	simplex.h	7440	log plain
-rw-r--r--	tableau.cpp	3691	log plain
-rw-r--r--	tableau.h	3227	log plain
-rw-r--r--	theory_arith.cpp	23139	log plain
-rw-r--r--	theory_arith.h	5342	log plain
-rw-r--r--	theory_arith_type_rules.h	2962	log plain
-rw-r--r--	unate_propagator.cpp	12236	log plain
-rw-r--r--	unate_propagator.h	4568	log plain