/* * structures.h: This file contains all important defintions. * You should study this file first if you want to modify the code * of RSat. * * Below, you will see defintions of data structures, * macro definitions, and function prototypes. * * The main structures are * - my_var      [variable] * - my_lit      [literal] * - my_clause   [clause] * - my_manager  [solving manager] *  */#ifndef STRUCTURES_DEFINED #define STRUCTURES_DEFINED #include "flags.h"//format string for printing large integers#ifdef _MSC_VERtypedef __int64  int64;#define i64d "I64d"#elsetypedef long long int64;#define i64d "lld"#endif//all allocation calls are made through these 2 wraping functions (defined in mem_alloc.cpp)#define calloc my_calloc#define malloc my_malloc//type definition for variables and literals/************************************************************ * Variables. Variables are often used as indices into arrays. * Variables ranges from 1 to # of variables. * For example, if the input problem contains 100 variables, * the variable indices will range from 1 to 100. ************************************************************/typedef int my_var;   /************************************************************ * Literals. The positive literal of the variable v is  * represented as (v<<1). The negative literal is (v<<1)|1. * There are many macros that can be used to manipulate literals. * Please see their definition below (search for 'macros'). * * For example, if l is of type my_lit * var(l) is the variable of l (type my_var). * lit_index(l) is the integer representation of l (can be * printed with %d). * neg(l) is the negation of l (type my_lit). * ************************************************************/typedef int my_lit;   //all functions related to heap are in heap.cpptypedef struct heap_t{  my_var* order;    //order[i] = variable at heap position i  int* indices;     //indices[x] = index of variable x in the (heap) order array  int size;         //current heap size (# items in heap)} heap;//type definition for the queue of implications used in bcptypedef heap implication_queue; //a clause contains an index, an array of literals and a sizetypedef struct clause_tt{    /*   * About clause index.   * Original clauses have negative indices [-1,-2,-3,...].   * Learned clauses have non-negative indices [0,1,2,...].   * This is because we keep a few information about learned clauses in arrays.   * This way, we can simply use indices of learned clauses as array indices.   * On the other hand, we do not have any array for orignal clauses.   */  int index;    //the clause index  my_lit* lits; //array of literals in this clause  int size;     //the size of this clause  } my_clause;//this is the main data structure for managing various things during the search//all functions related to initialization of this structure are in manager.cpptypedef struct manager_tt{  int vc;    //number of variables in the problem  int64 cc;  //number of original clauses (after some simplification in read_cnf)  my_clause** original_clauses;   //array of original clauses  int original_clauses_array_len; //the capacity of the original_clauses array  my_clause** learned_clauses;    //array of learned clauses  int learned_clauses_array_len;  //the capacity of the learned_clauses array    //Levels start at 1 (top level). 0 means that varaible is not yet assigned.   int* level;  //array of variables' levels. my_var-indexed.  my_lit* assign; //array of assignments. This is really the assignment stack.  my_lit* assign_top; //the top of the assignment stack.  my_lit** decision_lit; //array of decision literals. Indexed by the level of the decision.  int decision_lit_size; //the capacity of the decision_lit array.  my_lit* status;        //array of assignments of variables. my_var-indexed. status[v] is 0 if v is a free variable.或plit(var_index) 或nlit(var_index)  my_clause** reason;    //array of reasons for each implication. my_var-indexed. Decision variables have NULL reasons.  double* score;         //array of (vsids) scores of variables. my_var-inded.#if(ALLOW_PARTIAL_ORDER)  int* partial_order; //array of partial order "score". High score means high preference.                      //Scores in this array have higher priority than those in the 'score' array.#endif  my_clause*** watched;  //array of watched list for all literals. The entry of literal l is at position watched_index(l).  int* watched_size;     //the size of the watched list of each literal. Indexed by watched_index(l).  int* watched_len;      //the capacity of the watched list of each literal. Indexed by watched_index(l).  int decision_level;    //the current decision level  double restart_conflict_incr;   int64 next_restart_conflict; //the number of conflicts the solver has to reach to restart  int restart;                 //the number of restarts performed by the solver so far  int stack_offset;            //the offset into the assignment stack (assign). This is used only for enqueuing unit original clauses (see enqueue/process_unit_literal_queue).  char ok;                     //a flag used for indicating inconsistency during input reading. If ok==0, it means that the instance is trivially unsatisfiable.  my_clause* conflicting_clause;//the most recent conflicting clause.  my_clause* conflict_clause;  //the most recent conflict clause.  int assertion_level;         //the assertion level of the most recent conlict clause.  int conflict_level;          //the level of the most recent conflict.  implication_queue* imp;      //the queue of implications used in bcp.#if(VERIFY_SOLUTION)  my_lit* solution_stack;  my_lit* solution_stack_top;#endif  char save_progress;          //a flag. Whether to progress saving is ON or OFF.  my_lit* saved;               //the saved literal array. my_var-indexed. Used for progress saving implementation.  double* learned_clause_scores; //array of scores for all learned clauses. Indexed by the indices of learned clauses.  my_lit* cdc;  //a temporary array of literals (for conflict clause). Used in the function derive_conflict_clause.  int cdc_size; //the capacity of the cdc array.  int cdc_index; //the next free position in the cdc array.    char* seen;    //a temporary array used in derive_conflict_clause and removable. my_var-indexed.  my_lit* stack; //a temporary stack used in removable.   int stack_size; //the capacity of stack.  int* save;      //a temporary array used in removable.  int save_size;  //the capacity of save.  heap* var_order_heap; //the heap used for variable ordering (see heap.cpp).  double score_inc;  //the current variable score increment amount.  double score_inc_factor;  //the factor to increase score_inc by.    int64 decisions;          //the number of decisions made by the solver so far  int64 conflicts;          //the number of conflicts experienced by the solver so far  //the following variables are mostly for stats  int64 cdc_count;          //total number of learned clauses ever learned (some may have been deleted).  int64 cdl_count;          //total number of literals ever appear in learned clauses.  int64 cur_cdc_count;      //the current number of learned clauses.  int64 cur_cdl_count;      //the current number of literals in learned clauses.  int64 cur_cc;             //the current number of original clauses.  int64 cur_lit_count;      //the current number of literals in original clauses.  int64 original_literals_count; //total number of literals in the original instance that still remain  int64 original_clauses_count;  //total number of clauses in the original instance that still remain  int max_decision_level;   //the maximum decision level ever reached by the solver    int kb_reduction_count;  //number of times we have performed learned clause deletion  double clause_score_inc; //the current clause score increment amount.  double max_learned_clauses;  //the maximum number of learned clauses allowed before we need to delete some.    int kb_simplification_count; //number of times we have performed knowledge base simplification.  int num_conflicts_for_next_simplify; //number of conflicts to perform knowledge base simplification.  int next_simplify_increment;         //amount to increment num_conflicts_for_next_simplify by.  char simplify_orig_kb;               //a flag whether to perform (orig.) knowledge base simplication.  char simplify_learned_kb;            //a flag whether to perform (learned) knowledge base simplication.  double random_seed;   //a random seed used by the solver  int luby_unit;     //the number of conflicts used as the unit in our restarting policy calculation.  //these variables are for the implementation of periodic progress saving.  //they control when progress saving is turned ON or OFF. See analyze_conflict().  int on_th;         //how many conflicts to turn progress saving on for  int on_th_inc;     //increment amount for on_th every time we switch  int off_th;        //how many conflicts to turn progress saving off for  int off_th_inc;    //increment amount for off_th every time we switch  int next_sp_switch;//the next amount of conflicts to swich the state of progress saving    /*   * Result printing mode:   * 0: (default) print result line but not solution line   * 1: print nothing!   * 2: print result line AND solution line   */  char print_mode;  char verbose;  //varaibles below are for progres printing (see print_utils.cpp)  int64 previous_decision_count;  int64 previous_conflicts;  int previous_reduce_kb_count;  int previous_simplify_kb_count;  int base_unit_clause_learned;} my_manager;//Some frequently used macros.#define sign(l) (l&1)   //sign(l) is 1 if l is a negative literal#define neg(l)  (l^1)   //compute the negation of literal l#define lit_index(l) (sign(l)?-(l>>1):l>>1)  //compute the integer representation of literal l#define var(l) (l>>1)   //the variable of l#define plit(v) (v<<1)  //the positive literal of v#define nlit(v) ((v<<1)|1) //the negative literal of v#define set(l) (status[var(l)]==l) //1 iff l is set to true. *** status must point to my_m  ->status at the call location.#define watched_index(l) (2*(var(l)-1)+sign(l)) //the index of literal l in various arrays.literal的數組中的元素1 2 3 4 5 6  ,按宏計算其下標為0  1 2 3 4 5#define lit_from_int(in) (in<0?((-in)<<1)|1:in<<1) //convert integer in into a literal of type my_lit#define unresolved(l) (status[var(l)]!=neg(l)) //1 iff l is true or free.#define free_lit(l) (status[var(l)]==0)  //1 iff l is a free literal.#define resolved(l) (status[var(l)]==neg(l)) //1 iff l is set to false.#define var_ind(x) (x<0?-x:x)  //essentially abs(x)#define max(x,y) (x>y?x:y) //max of x and y#define min(x,y) (x<y?x:y) //min of x and y//operations for heap#define left(i) (i*2)#define right(i) ((i*2)+1)#define parent(i) (i/2) //this automatically rounds down//function for printing out a comment line#define rprintf(format, args...) ( printf("c "), printf(format , ## args), fflush(stdout) )//function prototypesvoid* my_calloc(size_t,size_t);void* my_malloc(size_t);//input parsingvoid read_cnf(char*);void enqueue(my_lit);#if(ALLOW_PARTIAL_ORDER)void read_po_file(char*);#endif//core functionschar process_unit_literal_queue();void add_conflict_clause();void analyze_conflict(my_clause*,int level);char set_decision(my_lit);int get_luby(int i);char assert_conflict_clause();int solve();void backtrack(int);char bcp(my_lit);//watched listvoid init_watched_literals();void remove_watched_clause(my_lit,my_clause*);void add_watched_clause(my_lit,my_clause*);void declare_watched_literals(my_clause*);//my_managerchar finish_up_init_manager();void init_clause(int*,int,int);void init_manager();void free_manager();//printingvoid print_progress_header();void print_progress();void print_progress_footer();void print_clause(my_clause*);void print_stats();void print_location();void print_solution();void print_watched_list(my_lit l);void print_indices(heap* h,int var_count);void print_order(heap* h);void print_usage();//debuggingvoid check_watched_list(char);void check_watched_literal_completeness();void check_sorted_clause_array(my_clause**,double*,int);void check_assignment_stack();void check_heap_property(heap* h,int var_count);void save_solution_to_file();#if(VERIFY_SOLUTION)void save_solution();char verify_solution();#endif//endif verif solution//kb managementvoid remove_clause(my_clause*);void sort_clauses_by_scores(my_clause***,double**,int);void simplify_kb();void simplify_original_kb();void reduce_kb();char add_base_clause(my_clause*); //added 10/11/07//heap relatedvoid init_heap(heap* h,int n);my_var get_min_element(heap* h);char empty(heap* h);void insert(heap* h,my_var v);void increase(heap* h,int v);void update(heap* h,int v);void undo(heap* h,my_var v);my_var select_variable();my_var dequeue(implication_queue* q);void rescale_variable_scores();void increment_literal_score(my_lit);void increment_clause_score(my_clause* c);void free_heap(heap* h);void reset_heap(heap*);//array size manipulationvoid double_decision_lit_len();void double_stack_len();void double_save_len();void double_cdc_len();void half_decision_lit_len();void double_learned_clauses_array();void* double_array_len(void*,int*,size_t);//functions for recursive/exhaustive SAT implementation (experimental_code.cpp)int solve_recursively(); //not used by the normal solverlong count_models();char at_assertion_level();char bcp2(my_lit);char decide(my_lit);void undo_decide();char assert_cd_literal();//time measuring function#ifdef _MSC_VER#include <ctime>static inline double get_cpu_time(void) {    return (double)clock() / CLOCKS_PER_SEC; }#else#include <sys/time.h>#include <sys/resource.h>static inline double get_cpu_time(void) {  struct rusage ru;  getrusage(RUSAGE_SELF, &ru);  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }#endif#endif//endif ifndef (topmost)