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	3008	log plain
-rw-r--r--	Makefile.subdirs	502	log plain
d---------	arith	2943	log plain
d---------	arrays	646	log plain
-rw-r--r--	atom_requests.cpp	1928	log plain
-rw-r--r--	atom_requests.h	2472	log plain
d---------	booleans	688	log plain
d---------	builtin	441	log plain
d---------	bv	1689	log plain
d---------	datatypes	387	log plain
-rw-r--r--	decision_attributes.h	1026	log plain
d---------	example	237	log plain
d---------	idl	487	log plain
-rw-r--r--	interrupted.h	1560	log plain
-rw-r--r--	ite_simplifier.cpp	13237	log plain
-rw-r--r--	ite_simplifier.h	4832	log plain
-rw-r--r--	logic_info.cpp	10232	log plain
-rw-r--r--	logic_info.h	12532	log plain
-rw-r--r--	logic_info.i	533	log plain
-rwxr-xr-x	mkrewriter	6381	log plain
-rwxr-xr-x	mktheorytraits	10965	log plain
-rw-r--r--	model.cpp	30096	log plain
-rw-r--r--	model.h	7945	log plain
-rw-r--r--	options	745	log plain
-rw-r--r--	options_handlers.h	2106	log plain
-rw-r--r--	output_channel.h	7824	log plain
d---------	quantifiers	2362	log plain
-rw-r--r--	quantifiers_engine.cpp	28159	log plain
-rw-r--r--	quantifiers_engine.h	11444	log plain
-rw-r--r--	rep_set.cpp	12690	log plain
-rw-r--r--	rep_set.h	3946	log plain
-rw-r--r--	rewriter.cpp	8671	log plain
-rw-r--r--	rewriter.h	3219	log plain
-rw-r--r--	rewriter_attributes.h	2546	log plain
-rw-r--r--	rewriter_tables_template.h	1957	log plain
d---------	rewriterules	1015	log plain
-rw-r--r--	shared_terms_database.cpp	8917	log plain
-rw-r--r--	shared_terms_database.h	7587	log plain
d---------	strings	441	log plain
-rw-r--r--	substitutions.cpp	11643	log plain
-rw-r--r--	substitutions.h	5957	log plain
-rw-r--r--	term_registration_visitor.cpp	10808	log plain
-rw-r--r--	term_registration_visitor.h	3999	log plain
-rw-r--r--	theory.cpp	6439	log plain
-rw-r--r--	theory.h	23432	log plain
-rw-r--r--	theory_engine.cpp	52907	log plain
-rw-r--r--	theory_engine.h	25094	log plain
-rw-r--r--	theory_registrar.h	1441	log plain
-rw-r--r--	theory_test_utils.h	3648	log plain
-rw-r--r--	theory_traits_template.h	1321	log plain
-rw-r--r--	theoryof_mode.h	1413	log plain
-rw-r--r--	type_enumerator.h	4591	log plain
-rw-r--r--	type_enumerator_template.cpp	1437	log plain
d---------	uf	804	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24270	log plain
-rw-r--r--	unconstrained_simplifier.h	1814	log plain
-rw-r--r--	valuation.cpp	2996	log plain
-rw-r--r--	valuation.h	4082	log plain