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	5604	log plain
-rw-r--r--	array.h	802	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	1565	log plain
-rw-r--r--	ascription_type.h	1957	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--	buffered_proof_generator.cpp	2477	log plain
-rw-r--r--	buffered_proof_generator.h	2117	log plain
-rw-r--r--	datatype_index.cpp	1117	log plain
-rw-r--r--	datatype_index.h	1938	log plain
-rw-r--r--	dtype.cpp	27467	log plain
-rw-r--r--	dtype.h	26271	log plain
-rw-r--r--	dtype_cons.cpp	19472	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	1864	log plain
-rw-r--r--	emptybag.h	1735	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	34307	log plain
-rw-r--r--	expr_manager_template.h	17277	log plain
-rw-r--r--	expr_template.cpp	24315	log plain
-rw-r--r--	expr_template.h	18291	log plain
-rw-r--r--	kind_map.h	6497	log plain
-rw-r--r--	kind_template.cpp	2442	log plain
-rw-r--r--	kind_template.h	2920	log plain
-rw-r--r--	lazy_proof.cpp	7405	log plain
-rw-r--r--	lazy_proof.h	4452	log plain
-rw-r--r--	lazy_proof_chain.cpp	10932	log plain
-rw-r--r--	lazy_proof_chain.h	6128	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	3829	log plain
-rw-r--r--	node.h	49533	log plain
-rw-r--r--	node_algorithm.cpp	18298	log plain
-rw-r--r--	node_algorithm.h	7905	log plain
-rw-r--r--	node_builder.h	48184	log plain
-rw-r--r--	node_manager.cpp	35621	log plain
-rw-r--r--	node_manager.h	55438	log plain
-rw-r--r--	node_manager_attributes.h	1411	log plain
-rw-r--r--	node_self_iterator.h	3299	log plain
-rw-r--r--	node_traversal.cpp	4069	log plain
-rw-r--r--	node_traversal.h	4740	log plain
-rw-r--r--	node_trie.cpp	2951	log plain
-rw-r--r--	node_trie.h	3961	log plain
-rw-r--r--	node_value.cpp	2905	log plain
-rw-r--r--	node_value.h	15034	log plain
-rw-r--r--	node_visitor.h	3281	log plain
-rw-r--r--	proof.cpp	13228	log plain
-rw-r--r--	proof.h	12013	log plain
-rw-r--r--	proof_checker.cpp	10271	log plain
-rw-r--r--	proof_checker.h	7680	log plain
-rw-r--r--	proof_generator.cpp	6600	log plain
-rw-r--r--	proof_generator.h	5791	log plain
-rw-r--r--	proof_node.cpp	2151	log plain
-rw-r--r--	proof_node.h	5134	log plain
-rw-r--r--	proof_node_algorithm.cpp	5367	log plain
-rw-r--r--	proof_node_algorithm.h	2380	log plain
-rw-r--r--	proof_node_manager.cpp	10789	log plain
-rw-r--r--	proof_node_manager.h	8062	log plain
-rw-r--r--	proof_node_to_sexpr.cpp	4139	log plain
-rw-r--r--	proof_node_to_sexpr.h	2000	log plain
-rw-r--r--	proof_node_updater.cpp	8882	log plain
-rw-r--r--	proof_node_updater.h	5652	log plain
-rw-r--r--	proof_rule.cpp	8446	log plain
-rw-r--r--	proof_rule.h	38170	log plain
-rw-r--r--	proof_set.h	2176	log plain
-rw-r--r--	proof_step_buffer.cpp	2924	log plain
-rw-r--r--	proof_step_buffer.h	2875	log plain
-rw-r--r--	record.cpp	3447	log plain
-rw-r--r--	record.h	2739	log plain
-rw-r--r--	sequence.cpp	7931	log plain
-rw-r--r--	sequence.h	5748	log plain
-rw-r--r--	skolem_manager.cpp	11273	log plain
-rw-r--r--	skolem_manager.h	9571	log plain
-rw-r--r--	subs.cpp	3522	log plain
-rw-r--r--	subs.h	2946	log plain
-rw-r--r--	sygus_datatype.cpp	3334	log plain
-rw-r--r--	sygus_datatype.h	4646	log plain
-rw-r--r--	symbol_manager.cpp	9001	log plain
-rw-r--r--	symbol_manager.h	5092	log plain
-rw-r--r--	symbol_table.cpp	21234	log plain
-rw-r--r--	symbol_table.h	7064	log plain
-rw-r--r--	tconv_seq_proof_generator.cpp	5233	log plain
-rw-r--r--	tconv_seq_proof_generator.h	4891	log plain
-rw-r--r--	term_canonize.cpp	5891	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	2464	log plain
-rw-r--r--	term_context_stack.cpp	2272	log plain
-rw-r--r--	term_context_stack.h	2152	log plain
-rw-r--r--	term_conversion_proof_generator.cpp	18701	log plain
-rw-r--r--	term_conversion_proof_generator.h	10387	log plain
-rw-r--r--	type.cpp	17583	log plain
-rw-r--r--	type.h	17859	log plain
-rw-r--r--	type_checker.h	1118	log plain
-rw-r--r--	type_checker_template.cpp	1939	log plain
-rw-r--r--	type_checker_util.h	5136	log plain
-rw-r--r--	type_matcher.cpp	3180	log plain
-rw-r--r--	type_matcher.h	2323	log plain
-rw-r--r--	type_node.cpp	19196	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