code_structure.txt

最快速的可满足性分析工具软件

======================
Code structure of RSat
======================

This file contains brief information about the structure of
the source code of RSat. Function summary is also provided in
the 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 see
the 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_flags

solver.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_queue

parse_input.cpp [input reading functions]
- read_cnf
- sort_literals
- parse_int
- read_line
- enqueue
- read_partial_order

utils.cpp [printing+debugging functions]
- print_progress_header
- print_progress_footer
- print_progress
- print_stack
- print_stats
- print_clause
- print_location
- check_partial_order

heap.cpp [variable ordering heap]
- all heap-related functions

kb_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_clause

watched_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 list

manager.cpp [dealing with manager]
- init_manager
- init_clause
- finish_up_init_manager
- free_manager

mem_alloc.cpp [memory allocation]
- my_malloc
- my_calloc

experimental_code.cpp [illustrative/less stable code]
- solve_recursively
- count_models
- at_assertion_level
- bcp2
- decide
- undo_decide
- assert_cd_literal