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	2916	log plain
-rw-r--r--	Makefile.subdirs	502	log plain
d---------	arith	1597	log plain
d---------	arrays	680	log plain
d---------	booleans	444	log plain
d---------	builtin	361	log plain
d---------	bv	1241	log plain
d---------	datatypes	609	log plain
d---------	example	237	log plain
-rw-r--r--	inst_match.cpp	35579	log plain
-rw-r--r--	inst_match.h	16864	log plain
-rw-r--r--	inst_match_impl.h	4178	log plain
-rw-r--r--	instantiator_default.cpp	1975	log plain
-rw-r--r--	instantiator_default.h	1506	log plain
-rw-r--r--	instantiator_tables_template.cpp	1155	log plain
-rw-r--r--	interrupted.h	1634	log plain
-rw-r--r--	ite_simplifier.cpp	13431	log plain
-rw-r--r--	ite_simplifier.h	4783	log plain
-rw-r--r--	logic_info.cpp	8602	log plain
-rw-r--r--	logic_info.h	7895	log plain
-rwxr-xr-x	mkinstantiator	5476	log plain
-rwxr-xr-x	mkrewriter	6157	log plain
-rwxr-xr-x	mktheorytraits	8992	log plain
-rw-r--r--	output_channel.h	8070	log plain
d---------	quantifiers	679	log plain
-rw-r--r--	quantifiers_engine.cpp	29523	log plain
-rw-r--r--	quantifiers_engine.h	14829	log plain
-rw-r--r--	rewriter.cpp	7579	log plain
-rw-r--r--	rewriter.h	3423	log plain
-rw-r--r--	rewriter_attributes.h	2610	log plain
-rw-r--r--	rewriter_tables_template.h	2181	log plain
d---------	rewriterules	599	log plain
-rw-r--r--	shared_terms_database.cpp	8354	log plain
-rw-r--r--	shared_terms_database.h	7436	log plain
-rw-r--r--	substitutions.cpp	6529	log plain
-rw-r--r--	substitutions.h	4819	log plain
-rw-r--r--	term_registration_visitor.cpp	9804	log plain
-rw-r--r--	term_registration_visitor.h	4065	log plain
-rw-r--r--	theory.cpp	6715	log plain
-rw-r--r--	theory.h	26269	log plain
-rw-r--r--	theory_engine.cpp	43842	log plain
-rw-r--r--	theory_engine.h	20904	log plain
-rw-r--r--	theory_registrar.h	1490	log plain
-rw-r--r--	theory_test_utils.h	3438	log plain
-rw-r--r--	theory_traits_template.h	1106	log plain
-rw-r--r--	trigger.cpp	17588	log plain
-rw-r--r--	trigger.h	6503	log plain
d---------	uf	945	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24123	log plain
-rw-r--r--	unconstrained_simplifier.h	1870	log plain
-rw-r--r--	valuation.cpp	2920	log plain
-rw-r--r--	valuation.h	3973	log plain