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	5690	log plain
-rw-r--r--	array_store_all.cpp	3737	log plain
-rw-r--r--	array_store_all.h	2199	log plain
-rw-r--r--	ascription_type.cpp	1540	log plain
-rw-r--r--	ascription_type.h	1964	log plain
-rw-r--r--	attribute.cpp	3481	log plain
-rw-r--r--	attribute.h	19806	log plain
-rw-r--r--	attribute_internals.h	15121	log plain
-rw-r--r--	attribute_unique_id.h	1717	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	2020	log plain
-rw-r--r--	datatype_index.cpp	1140	log plain
-rw-r--r--	datatype_index.h	1915	log plain
-rw-r--r--	dtype.cpp	27866	log plain
-rw-r--r--	dtype.h	26200	log plain
-rw-r--r--	dtype_cons.cpp	20118	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	1734	log plain
-rw-r--r--	emptyset.cpp	2019	log plain
-rw-r--r--	emptyset.h	1779	log plain
-rw-r--r--	expr_iomanip.cpp	3584	log plain
-rw-r--r--	expr_iomanip.h	4540	log plain
-rw-r--r--	expr_manager_scope.h	2571	log plain
-rw-r--r--	expr_manager_template.cpp	34261	log plain
-rw-r--r--	expr_manager_template.h	15870	log plain
-rw-r--r--	expr_template.cpp	24089	log plain
-rw-r--r--	expr_template.h	18291	log plain
-rw-r--r--	kind_map.h	1585	log plain
-rw-r--r--	kind_template.cpp	2462	log plain
-rw-r--r--	kind_template.h	2920	log plain
-rw-r--r--	lazy_proof.cpp	7510	log plain
-rw-r--r--	lazy_proof.h	4384	log plain
-rw-r--r--	lazy_proof_chain.cpp	11048	log plain
-rw-r--r--	lazy_proof_chain.h	6107	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	5354	log plain
-rw-r--r--	metakind_template.h	6113	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	3879	log plain
-rw-r--r--	node.h	49338	log plain
-rw-r--r--	node_algorithm.cpp	18728	log plain
-rw-r--r--	node_algorithm.h	8602	log plain
-rw-r--r--	node_builder.h	48184	log plain
-rw-r--r--	node_manager.cpp	37940	log plain
-rw-r--r--	node_manager.h	57820	log plain
-rw-r--r--	node_manager_attributes.h	1323	log plain
-rw-r--r--	node_self_iterator.h	3299	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	2953	log plain
-rw-r--r--	node_trie.h	3961	log plain
-rw-r--r--	node_value.cpp	2912	log plain
-rw-r--r--	node_value.h	14978	log plain
-rw-r--r--	node_visitor.h	3281	log plain
-rw-r--r--	proof.cpp	13648	log plain
-rw-r--r--	proof.h	12384	log plain
-rw-r--r--	proof_checker.cpp	10279	log plain
-rw-r--r--	proof_checker.h	7697	log plain
-rw-r--r--	proof_ensure_closed.cpp	5248	log plain
-rw-r--r--	proof_ensure_closed.h	2563	log plain
-rw-r--r--	proof_generator.cpp	2254	log plain
-rw-r--r--	proof_generator.h	4045	log plain
-rw-r--r--	proof_node.cpp	2151	log plain
-rw-r--r--	proof_node.h	5234	log plain
-rw-r--r--	proof_node_algorithm.cpp	5409	log plain
-rw-r--r--	proof_node_algorithm.h	2386	log plain
-rw-r--r--	proof_node_manager.cpp	10865	log plain
-rw-r--r--	proof_node_manager.h	8107	log plain
-rw-r--r--	proof_node_to_sexpr.cpp	4450	log plain
-rw-r--r--	proof_node_to_sexpr.h	2081	log plain
-rw-r--r--	proof_node_updater.cpp	9093	log plain
-rw-r--r--	proof_node_updater.h	5987	log plain
-rw-r--r--	proof_rule.cpp	10615	log plain
-rw-r--r--	proof_rule.h	50770	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	2864	log plain
-rw-r--r--	record.cpp	832	log plain
-rw-r--r--	record.h	1793	log plain
-rw-r--r--	sequence.cpp	7950	log plain
-rw-r--r--	sequence.h	5748	log plain
-rw-r--r--	skolem_manager.cpp	11538	log plain
-rw-r--r--	skolem_manager.h	9146	log plain
-rw-r--r--	subs.cpp	3542	log plain
-rw-r--r--	subs.h	2946	log plain
-rw-r--r--	sygus_datatype.cpp	3354	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	5264	log plain
-rw-r--r--	symbol_table.cpp	22027	log plain
-rw-r--r--	symbol_table.h	7084	log plain
-rw-r--r--	tconv_seq_proof_generator.cpp	5293	log plain
-rw-r--r--	tconv_seq_proof_generator.h	4879	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	2452	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	19572	log plain
-rw-r--r--	term_conversion_proof_generator.h	10664	log plain
-rw-r--r--	type.cpp	17602	log plain
-rw-r--r--	type.h	17816	log plain
-rw-r--r--	type_checker.h	1118	log plain
-rw-r--r--	type_checker_template.cpp	1966	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	19304	log plain
-rw-r--r--	type_node.h	33008	log plain
-rw-r--r--	type_properties_template.h	3653	log plain
-rw-r--r--	uninterpreted_constant.cpp	3214	log plain
-rw-r--r--	uninterpreted_constant.h	1951	log plain
-rw-r--r--	variable_type_map.h	1696	log plain