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--	.gitignore	18	log plain
-rw-r--r--	Makefile	70	log plain
-rw-r--r--	Makefile.am	2318	log plain
-rw-r--r--	Makefile.subdirs	502	log plain
d---------	arith	1398	log plain
d---------	arrays	566	log plain
d---------	booleans	444	log plain
d---------	builtin	361	log plain
d---------	bv	674	log plain
d---------	datatypes	489	log plain
d---------	example	237	log plain
-rw-r--r--	interrupted.h	1634	log plain
-rwxr-xr-x	mkrewriter	5882	log plain
-rwxr-xr-x	mktheorytraits	8403	log plain
-rw-r--r--	output_channel.h	3350	log plain
-rw-r--r--	registrar.h	1399	log plain
-rw-r--r--	rewriter.cpp	6863	log plain
-rw-r--r--	rewriter.h	3037	log plain
-rw-r--r--	rewriter_attributes.h	2583	log plain
-rw-r--r--	rewriter_tables_template.h	1994	log plain
-rw-r--r--	shared_terms_database.cpp	3547	log plain
-rw-r--r--	shared_terms_database.h	3842	log plain
-rw-r--r--	substitutions.cpp	5399	log plain
-rw-r--r--	substitutions.h	2807	log plain
-rw-r--r--	term_registration_visitor.cpp	7316	log plain
-rw-r--r--	term_registration_visitor.h	3536	log plain
-rw-r--r--	theory.cpp	2265	log plain
-rw-r--r--	theory.h	17950	log plain
-rw-r--r--	theory_engine.cpp	18576	log plain
-rw-r--r--	theory_engine.h	14836	log plain
-rw-r--r--	theory_test_utils.h	2998	log plain
-rw-r--r--	theory_traits_template.h	1106	log plain
d---------	uf	475	log plain
-rw-r--r--	valuation.cpp	1522	log plain
-rw-r--r--	valuation.h	2140	log plain