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	5548	log plain
-rw-r--r--	array.h	802	log plain
-rw-r--r--	array_store_all.cpp	3600	log plain
-rw-r--r--	array_store_all.h	2199	log plain
-rw-r--r--	ascription_type.h	1952	log plain
-rw-r--r--	attribute.cpp	3481	log plain
-rw-r--r--	attribute.h	18224	log plain
-rw-r--r--	attribute_internals.h	15140	log plain
-rw-r--r--	attribute_unique_id.h	1738	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	27466	log plain
-rw-r--r--	dtype.h	26271	log plain
-rw-r--r--	dtype_cons.cpp	19481	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	4431	log plain
-rw-r--r--	expr_iomanip.h	6121	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	24294	log plain
-rw-r--r--	expr_template.h	18452	log plain
-rw-r--r--	kind_map.h	6517	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	10058	log plain
-rw-r--r--	lazy_proof_chain.h	5501	log plain
-rw-r--r--	lazy_proof_set.cpp	1202	log plain
-rw-r--r--	lazy_proof_set.h	2003	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	50265	log plain
-rw-r--r--	node_algorithm.cpp	17593	log plain
-rw-r--r--	node_algorithm.h	7440	log plain
-rw-r--r--	node_builder.h	48204	log plain
-rw-r--r--	node_manager.cpp	33916	log plain
-rw-r--r--	node_manager.h	56415	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	4759	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	2923	log plain
-rw-r--r--	node_value.h	15221	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	9166	log plain
-rw-r--r--	proof_checker.h	7509	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	10674	log plain
-rw-r--r--	proof_node_manager.h	7980	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	8097	log plain
-rw-r--r--	proof_rule.h	36629	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--	sygus_datatype.cpp	3334	log plain
-rw-r--r--	sygus_datatype.h	4646	log plain
-rw-r--r--	symbol_table.cpp	22168	log plain
-rw-r--r--	symbol_table.h	6997	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	18585	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	17902	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	19043	log plain
-rw-r--r--	type_node.h	32883	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