expr « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	CMakeLists.txt	4512	log plain
-rw-r--r--	array_store_all.cpp	3737	log plain
-rw-r--r--	array_store_all.h	2137	log plain
-rw-r--r--	ascription_type.cpp	1540	log plain
-rw-r--r--	ascription_type.h	1929	log plain
-rw-r--r--	attribute.cpp	3460	log plain
-rw-r--r--	attribute.h	19758	log plain
-rw-r--r--	attribute_internals.h	15061	log plain
-rw-r--r--	attribute_unique_id.h	1697	log plain
-rw-r--r--	bound_var_manager.cpp	1493	log plain
-rw-r--r--	bound_var_manager.h	3368	log plain
-rw-r--r--	buffered_proof_generator.cpp	2513	log plain
-rw-r--r--	buffered_proof_generator.h	2035	log plain
-rw-r--r--	datatype_index.cpp	1140	log plain
-rw-r--r--	datatype_index.h	1854	log plain
-rw-r--r--	dtype.cpp	27965	log plain
-rw-r--r--	dtype.h	26200	log plain
-rw-r--r--	dtype_cons.cpp	20388	log plain
-rw-r--r--	dtype_cons.h	13276	log plain
-rw-r--r--	dtype_selector.cpp	2092	log plain
-rw-r--r--	dtype_selector.h	2421	log plain
-rw-r--r--	emptybag.cpp	1901	log plain
-rw-r--r--	emptybag.h	1698	log plain
-rw-r--r--	emptyset.cpp	2018	log plain
-rw-r--r--	emptyset.h	1743	log plain
-rw-r--r--	expr_iomanip.cpp	3575	log plain
-rw-r--r--	expr_iomanip.h	4487	log plain
-rw-r--r--	kind_map.h	1600	log plain
-rw-r--r--	kind_template.cpp	2447	log plain
-rw-r--r--	kind_template.h	2823	log plain
-rw-r--r--	lazy_proof.cpp	7510	log plain
-rw-r--r--	lazy_proof.h	4399	log plain
-rw-r--r--	lazy_proof_chain.cpp	11427	log plain
-rw-r--r--	lazy_proof_chain.h	6122	log plain
-rw-r--r--	match_trie.cpp	5656	log plain
-rw-r--r--	match_trie.h	2526	log plain
-rw-r--r--	metakind_template.cpp	5567	log plain
-rw-r--r--	metakind_template.h	6078	log plain
-rwxr-xr-x	mkexpr	7231	log plain
-rwxr-xr-x	mkkind	9809	log plain
-rwxr-xr-x	mkmetakind	10363	log plain
-rw-r--r--	node.cpp	3878	log plain
-rw-r--r--	node.h	47752	log plain
-rw-r--r--	node_algorithm.cpp	18726	log plain
-rw-r--r--	node_algorithm.h	8602	log plain
-rw-r--r--	node_builder.cpp	22059	log plain
-rw-r--r--	node_builder.h	14877	log plain
-rw-r--r--	node_manager.cpp	37446	log plain
-rw-r--r--	node_manager.h	54306	log plain
-rw-r--r--	node_manager_attributes.h	1288	log plain
-rw-r--r--	node_self_iterator.h	3291	log plain
-rw-r--r--	node_traversal.cpp	4092	log plain
-rw-r--r--	node_traversal.h	4718	log plain
-rw-r--r--	node_trie.cpp	2970	log plain
-rw-r--r--	node_trie.h	3961	log plain
-rw-r--r--	node_value.cpp	2902	log plain
-rw-r--r--	node_value.h	14867	log plain
-rw-r--r--	node_visitor.h	3280	log plain
-rw-r--r--	proof.cpp	13648	log plain
-rw-r--r--	proof.h	12399	log plain
-rw-r--r--	proof_checker.cpp	10279	log plain
-rw-r--r--	proof_checker.h	7774	log plain
-rw-r--r--	proof_ensure_closed.cpp	5256	log plain
-rw-r--r--	proof_ensure_closed.h	2578	log plain
-rw-r--r--	proof_generator.cpp	2254	log plain
-rw-r--r--	proof_generator.h	4060	log plain
-rw-r--r--	proof_node.cpp	1792	log plain
-rw-r--r--	proof_node.h	5161	log plain
-rw-r--r--	proof_node_algorithm.cpp	5409	log plain
-rw-r--r--	proof_node_algorithm.h	2401	log plain
-rw-r--r--	proof_node_manager.cpp	12434	log plain
-rw-r--r--	proof_node_manager.h	8431	log plain
-rw-r--r--	proof_node_to_sexpr.cpp	4345	log plain
-rw-r--r--	proof_node_to_sexpr.h	2112	log plain
-rw-r--r--	proof_node_updater.cpp	8895	log plain
-rw-r--r--	proof_node_updater.h	6099	log plain
-rw-r--r--	proof_rule.cpp	10614	log plain
-rw-r--r--	proof_rule.h	51175	log plain
-rw-r--r--	proof_set.h	2191	log plain
-rw-r--r--	proof_step_buffer.cpp	2957	log plain
-rw-r--r--	proof_step_buffer.h	2879	log plain
-rw-r--r--	record.cpp	830	log plain
-rw-r--r--	record.h	1756	log plain
-rw-r--r--	sequence.cpp	7950	log plain
-rw-r--r--	sequence.h	5748	log plain
-rw-r--r--	skolem_manager.cpp	10519	log plain
-rw-r--r--	skolem_manager.h	13888	log plain
-rw-r--r--	subs.cpp	3626	log plain
-rw-r--r--	subs.h	2946	log plain
-rw-r--r--	sygus_datatype.cpp	3438	log plain
-rw-r--r--	sygus_datatype.h	4646	log plain
-rw-r--r--	symbol_manager.cpp	10723	log plain
-rw-r--r--	symbol_manager.h	5290	log plain
-rw-r--r--	symbol_table.cpp	22028	log plain
-rw-r--r--	symbol_table.h	7110	log plain
-rw-r--r--	tconv_seq_proof_generator.cpp	5293	log plain
-rw-r--r--	tconv_seq_proof_generator.h	4894	log plain
-rw-r--r--	term_canonize.cpp	5911	log plain
-rw-r--r--	term_canonize.h	3658	log plain
-rw-r--r--	term_context.cpp	3413	log plain
-rw-r--r--	term_context.h	6058	log plain
-rw-r--r--	term_context_node.cpp	2368	log plain
-rw-r--r--	term_context_node.h	2467	log plain
-rw-r--r--	term_context_stack.cpp	2304	log plain
-rw-r--r--	term_context_stack.h	2152	log plain
-rw-r--r--	term_conversion_proof_generator.cpp	19592	log plain
-rw-r--r--	term_conversion_proof_generator.h	10457	log plain
-rw-r--r--	type_checker.h	1110	log plain
-rw-r--r--	type_checker_template.cpp	1958	log plain
-rw-r--r--	type_checker_util.h	5156	log plain
-rw-r--r--	type_matcher.cpp	3180	log plain
-rw-r--r--	type_matcher.h	2300	log plain
-rw-r--r--	type_node.cpp	19545	log plain
-rw-r--r--	type_node.h	31272	log plain
-rw-r--r--	type_properties_template.h	3645	log plain
-rw-r--r--	uninterpreted_constant.cpp	3213	log plain
-rw-r--r--	uninterpreted_constant.h	1939	log plain