======================Code structure of RSat======================This file contains brief information about the structure ofthe source code of RSat. Function summary is also provided inthe header of every file.We structure the code such that high-level and low-level functions are in different files. The hope is that if you are not planning on optimizing any low-level details, you should not need to touch those low-level files.For example, all the core solving functions are in solver.cpp.By looking at this relatively short file, you can already seethe whole structure of the solver.Note that we have also privided a relatively extensive amount of comments for all files.============Header files============structures.h : All data structures are defined here. **Study this file first before any serious modification**constants.h : All constants are defined here.flags.h : All compilation flags are defined here.==========.cpp files==========main.cpp [main function is here]- main - parse_option- print_usage- signal_handlers- print_flagssolver.cpp [the core solving functions]- solve (main solving function)- bcp- analyze_conflict- derive_conflict_clause- assert_conflict_clause- select_variable- backtrack- use_saved_phase- set_decision- get_luby- removable- process_unit_literal_queueparse_input.cpp [input reading functions]- read_cnf- sort_literals- parse_int- read_line- enqueue- read_partial_orderutils.cpp [printing+debugging functions]- print_progress_header- print_progress_footer- print_progress- print_stack- print_stats- print_clause- print_location- check_partial_orderheap.cpp [variable ordering heap]- all heap-related functionskb_management.cpp [adding/deleting learned clauses]- simplify_KB- reduce_KB- locked- simplify- remove_clause- add_conflict_driven_clause- check_sorted_clauses_array- sort_clauses_by_activity- add_base_clausewatched_list.cpp [funcions related to watched list management]- add_watched_clause- remove_watched_clause- double_watched_len- half_watched_len- double_decision_lit_len- half_decision_lit_len- init_watched_literals- declare_watched_literals- other debugging functions related to watched listmanager.cpp [dealing with manager]- init_manager- init_clause- finish_up_init_manager- free_managermem_alloc.cpp [memory allocation]- my_malloc- my_callocexperimental_code.cpp [illustrative/less stable code]- solve_recursively- count_models- at_assertion_level- bcp2- decide- undo_decide- assert_cd_literal