#include <stdio.h>
#include <stdint.h>
#include <zlib.h>

#if defined(__GNUC__)
# define DD_INLINE __inline__
# if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
#   define DD_UNUSED __attribute__ ((__unused__))
# else
#   define DD_UNUSED
# endif
#else
# if defined(__cplusplus)
#   define DD_INLINE inline
# else
#   define DD_INLINE
# endif
# define DD_UNUSED
#endif


typedef struct satManagerStruct satManager_t;
typedef struct satClauseStruct satClause_t;
typedef struct satArrayStruct satArray_t;
typedef struct satHeapStruct satHeap_t;
typedef struct satSmtManagerStruct satSmtManager_t; /** sateen: smt manager **/ 
typedef struct satSmtVarStruct satSmtVar_t; 	    /** sateen: smt variable **/ 
typedef struct satTernaryStruct satTernary_t; 	    /** alembic: ternary structure **/
typedef struct satTrieStruct satTrie_t;		    /** alembic: trie structure **/
typedef struct satQueueStruct satQueue_t;           /** varelim: queue structure **/

typedef struct satStackStruct satStack_t;	    /** standard stack structure **/
typedef struct satSCCStruct satSCC_t;	    	    /** SCC structure **/

#define SMT_ADD_THEORY
#define OPTIMIZE_CLAUSE
#define LUBY_RESTART

struct satHeapStruct {
        long size;
        int (*compare)(void *, const void *, const void *);
	long *heap;
	long *indices;
};

struct satArrayStruct {
	long total;
	long size;
	long space[0];
};

struct satQueueStruct {
	long max;         	/* max size of queue */
        long size;		/* The number of entries */
  	long first;		/* The front index of entries */
	long last;		/* The last index of entries */
	long elems[0];		/* The location to save entries */ 
};

struct satStackStruct {
	long max;         	/* max size of queue */
        /*long size;*/		/* The number of entries */
  	long top;		/* The top index of entries */
	long elems[0];		/* The location to save entries */ 
};

struct satSCCStruct {
  	unsigned idx;
	unsigned min;
	int done;
};

struct satTernaryStruct {
	satTernary_t *lokid;		/* lower child */
	union { satTernary_t *eqkid[2];	/* equal child */ 
	        satClause_t *c; }eqleaf;/* pointer of a clause */ 
	satTernary_t *hikid;		/* higher child */
	int valid;			/* valid mark */ 
	long id;			/* node id */
};

struct satTrieStruct{
 	long id; 			/* node id or clause index */
 	long depth;			/* depth in a tree */
	satArray_t *child[2];		/* children */
	satTrie_t *parent;		/* parent */
	int valid;			/* valid mark */
};


struct satClauseStruct {
	long size; 
	union { double activity; long abstract; } info;
	satArray_t *dependent;
	long lits[0];
};

struct satManagerStruct {
        long status;
        long nVars;
	long nClauses;
	satArray_t *clauses; /*array of satClause_t * */
	satArray_t *learned; /*array of satClause_t * */
	satArray_t *blocking; /*array of satClause_t * */
	satArray_t *theory; /*array of satClause_t * */
	satArray_t *deleted; /*array of satClause_t * */
	satArray_t *shortClauses; /*array of satClause_t * */
	satHeap_t *variableHeap;
	satArray_t *decisionStackSeperator; /* array of long */
	satArray_t *previousDecisionHistory; /* array of long */

	char 	*values; 
	char 	*marks; 
	char 	*visits; 
	long    *dominator; 
	long    *dominator2; 
	char 	*dummy; 
	char    *equi;
	char    *pure;
	char    *bvars;  /** HH: boolean variables marked by Sateen **/
	satArray_t **wls; 
	satClause_t **antes; 

	
	long *levels; 
	long *decisionStack; /* array of long */
	long *maps;
	long curPos; /* first unimplicated variable  */
	long curBinPos; /* first unimplicated variable  */
	long stackPos; /* position of last assigned variable */
        long nCurConflicts;
	long preLevelZeroStackPos;
	long polarityChangeLimit;

	char 	*removable; 
	char 	*unremovable; 
        int	minimizeConflictLimit;
	double  *activity;
        int 	minimizeAssert;
        int     minimizeAssertLimit;
        int     implydepth;
        long    minimizeAssertTry;

	long    nRestarts;
	double  progress;

	double	varDecay;
	double  clauseDecay;
	double	varInc;
 	double  clauseInc;
	double  learnedSizeFactor;
	double  learnedSizeInc;

	double	restartFirst;
#ifdef LUBY_RESTART
	long	restartInc;
#endif
#ifndef LUBY_RESTART
	double	restartInc;
#endif
	long	restartIndex;
	double  randomSeed;
	double  randomFrequency;

	long  reduceClausesThresh;

	satArray_t *clearned;
	satArray_t *elearned;
	satArray_t *cclearned;
	satArray_t *redundant;
	satArray_t *tlearned;
	satArray_t *dependent;
	satArray_t *temp;
	satArray_t *tempUnitClauses;
	satArray_t *seen;
	satArray_t *subsumedClauseArray;
	satArray_t *mdominatorClause;

	double nStarts, nDecisions, nRandomDecisions;
	double nHistoryDecisions, nTHistoryDecisions;
        double nImplications, nConflicts;
        double nCurClauseLits, nCurLearnedLits;
        double nTotalClauseLits, nTotalLearnedLits;
        double nTotalLearnedClauses, nCurLearnedClauses;
        double preTotalLearnedCl, preTotalLearnedLit;
        double nCurBlockingClauses, nCurBlockingLits;
        double nTotalBlockingClauses, nTotalBlockingLits;
        double nSubsumedClauses, nSubsumedDeletedLiterals;
	int    nSimplify;

        double preJumpCl;
        double nForceRestart;
        double nPolarityChange;

	long nReduceClauses;
	long nFirstUip;
        long simpDBAssigns;
        long simpDBProps;
	long n2LitClauses;
	long nJump;
	long nLevel;
        long bsAssigns;
        long nLearnedDom;
        long nLearnedMDom;

	double	readTime;
	double	solveTime;
	double  preJump;
	double  preLit;

        int enableFrequentRestart;
	int buildBridge;
	int useRandom;
	int defaultSign;
	int polarityMode;
	int changeDirection;
	int allSat;
	int coreGeneration;
	int includeLevelZero;
	int enableSimplify;
	int usePreviousDecisionHistory;
        int checkSubsumption;
        int printModel;
        int enableAddTheoryClause; /* Hyondeuk Kim */
        int enableOptimizeClause; /* Hyondeuk Kim */

	satClause_t *nullClause;

        void *SMTManager; /* sateen pointer */
	satArray_t *explanation; /*array of int */

        /** HHJ: Elements for Alembic/distillation **/
	long tempInt;			/* Temporary usage */
	int verbosity;			/* Verbose level */
	char *cnfFileName;		/* Name of cnf file */
	FILE *LGF;			/* Name of log file */
	char *outfile;			/* Name of output cnf file */
	long *scores;			/* Scores of literals */
	long *clausesList;		/* Clauses list of literals */
	long *clausesLearnedList;	/* Clauses learned list of literals */
 	satArray_t *candidates;		/* candidates for simplification */
	satTernary_t *ternary;  	/* Ternary root */
	 	
	/** Options **/
	char *simpCnf;			/* Simplified CNF */
	int substitute;                 /* turn on equivalent variables substitution */ 
	int writeCnf;			/* Writing simplified CNF */
 	int simplify;			/* Simplification mode */
	int eliminateVar;		/* Variable elimination only mode */ 
	int distill;			/* Distillation mode */
	int computeSCC;			/* Computation of strongly connected component */
	int nIteratePreprocess;		/* N interations of preprocessing */ 
	int subsumeInConflict;		/* Subsumption check in conflict analysis */
	int minimizeConflict;		/* Conflict clause minimization */
	int writeSimplifiedCNF;		/* Exit after writing a simplified CNF file */
	int periodicDistill;		/* Periodic distillation */
	int writeStatistics;		/* Write a statistics file */
        int limitDistill; 
	long distillMin;		/* Minimum length of clause to distill */
	long distillMax;		/* Maximum length of clause to distill */
        long preLearnedPos;		/* Index of the array of new conflicts */
	
	double distillInc;		/* Periode of distillation */
      
	double reductionWithDistill;	/* Threshold for periodic distillation */
	long boundPeriodicDistill;	/* Value to bound periodic distillation */
        long nRejectDistill;		/* The number of rejects to distill */ 
	double distillTime; 		/* Time spent for distillations */
	double elimTime; 		/* Time spent for eliminations */
	double nImplicationsInDistill;   /* The number of implications in distillation */
 
	long nTernaryNodes;		/* The number of built trie node */
	long nVisitedTernaryNodes;		/* The number of visited tries nodes */
	long nInClForDistill;		/* The number of input clauses for distillation */
	long nInLitForDistill;		/* The number of input literals for distillation */
	long nInLearnedClForDistill;	/* The number of input learned clauses for distillation */
	long nInLearnedLitForDistill;	/* The number of input learned literals for distillation */
	long nOutClForDistill;	 	/* The number of output clauses for distillation */
	long nOutLitForDistill;		/* The number of output literals for distillation */
        long nOutLearnedClForDistill;   /* The number of output learned clauses for distillation */
        long nOutLearnedLitForDistill;  /* The number of output learned literals for distillation */
	long nDeletedVar;		/* The number of delete variables */
	long nOldLearnedInDistill;	/* The number of old conflicts in distillation */
	long nLearnedInDistill;		/* The number of conflicts in distillation */
	long nResolvedInDistill;	/* The number of resolvents in distillation */
	long nDistill;			/* The number of distillation */
	long nSATCl;			/* The number of clauses satisfied */
	long nLearnedClInDistill;	/* The number of learned clauses in distillation */
	long nLearnedLitInDistill;	/* The number of learned literals in distillation */
	long nLearnedUnitClInDistill;	/* The number of learned unit clauses in distillation */
        long nUIPConflictClauses;	
	long nUIPConflictLits;

        /** HH : On-the-fly clause improvement **/
        long nExtraSubsumes;
	long depthOfConflict;
	long depthOfStrong;
	long depthOfOTS;
        long nDistillInConflict; 	/* The number of subsumptions with OCI */
	long nEliminatedClsInConflict;  /* The number of clauses eliminated in OCI */
	long nEliminatedLitsInConflict; /* The number of literals eliminated in OCI */
	long nOmittedConflictClauses;   /* The number of omitted conflict clauses */
	long nOmittedConflictLits; 	/* The number of omitted conflict literals */

	long nAuxLearnedClauses;	/* The number of auxilary learned clauses */
	long nAuxLearnedLits;	 	/* The number of auxilary learned literals */
        long nAuxConflictAnalysis;	/* The number of auxilary conflict analysis */ 

	/** HHJ : Variable Elimination **/
	satHeap_t *varElimHeap; 	/* Heap for variable elimination */
	satQueue_t *satQueue;		/* Queue for sat */
	satStack_t *satStack;		/* Stack for sat */
	satArray_t *resolvents;		/* Literal pool of resolvent created by variable elimination */
	satArray_t *elimtable;		/* Array of the elimtable variables */
	char *litMarks;			/* Array of the marks of the literals */
	long majorityClauseLength;      /* Majority clause length */
        long minorityClauseLength;	/* Non majority clause length */
	long *clausesHistogram;         /* Statistics of clause sizes */
	long grow;			/* Bound of the number of clauses increases */
	long nInputVars;
	long nInputClauses;
	long nInputLiterals;
        long nEquiVars;			/* The number of variables in equivalent relation */
        long nVarElimTry;		/* The number of variables check in elimination */	
        long nVarElimReject;    	/* The number of variables declined in elimination */	
        long nSubsumeTry; 		/* The number of calls of backward subsumption */
	long nLits;			/* The number of original literals */
        long nResolvents;		/* The number of resolvents generated */
	long nResolventLits;		/* The number of resolvent literals */
	long nEliminatedCls;		/* The number of eliminated original clauses */
	long nEliminatedLits;		/* The number of eliminated literals */
	long nEliminatedVars; 		/* The number of eliminated variables */
	long nSelfsubsume;		/* The number of selfsubsumptions in resolution */
	long nBackwardSelfsubsume;  	/* The number of selfsubsumptions in backward check */
	long nLitStrengthened;		/* The number of literals removed by slefsubsumption */
	long nNewUnitLits;		/* The number of unit literals generated */
	long nDuplicates;		/* The number of duplicate literals by substitution */
	long nNewTautologies;           /* The number of additional tautology cases by substitution */

        int conflictLevels[5];
        int *mcla;
        int mclaSize;
        int mclaTotal;
        int maxContiguousLevel;
        int maxContiguousLevelTotal;
        int maxContiguousLevelCount;
        int maxContiguousLimit;
        double preThickTail;
        int maxContiguousDataCollect;
        int maxContiguousData[6];
        int nStrongConflictClauses;
        int nSupplementalConflictClauses;

	/** HH: Dominator based learning **/
#ifdef HH_BINARY
        long *binWls;          /** HH: the number of binary clauses in each watched literal list **/
#endif
	long nBinImplications;  /** HH: the number of binary implications **/
	long nDomSubsumes;      /** HH: the number of subsuming dominator clauses **/
	long nDomStrengthened;  /** HH: the number of subsuming dominator clauses **/
	long nMDomStrengthened;  /** HH: the number of subsuming multiple dominator clauses **/
	long nDomEliminated;  /** HH: the number of eliminated dominator
				clauses **/
	long nMergeUnit;      /** HH: the number of unit clauses by merging
				two literal clauses **/
	long simplimit;      /** HH: limit of simplification **/ 


	long nCurImps;      	/** HH: the number of implications at the current level **/
        long nPerSimVars;
        long nPerSimCls;
        long nPerSimLearnd; 
	long nPerSimLits;
        long nPerSimLearnedLits;
        long nPerSim;

	long *repr;
	long equiv;
	long mergedv;
	long nSCCs;
        long nMerged;
	long nDuplicateLits;
};

/** HHJ : The number of flag bits of clause 
 *        has been changed from 4.
 **/
#define SATCsizeShift           5 
#define SATCLearned             1
#define SATCBlocking            2
#define SATCTheory              4
#define SATCVisited             8
#define SATCIrredundant	 	16	
#define SATCMask                31 
#define SATCTypeMask            7
#define SATSizeClause(c) 	(c->size >> SATCsizeShift)
#define SATVar(l)		(l >> 1)
#define SATSign(l)		(l & 1)
#define SATValue(m, l)		((m->values(SATVar(l))) ^ SATsign(l))
#define SATCurLevel(m)		(m->decisionStackSeperator->size)
#define SATClauseLearned(c)	(c->size & 1)
#define SATClauseBlock(c)	(c->size & 2)

/** HHJ : New macros **/
#define SATClauseOriginal(c)    ((c->size & 15) == 0)
#define SATClauseIrredundant(c)	(c->size & SATCIrredundant)
#define SATClauseVisited(c)	(c->size & SATCVisited)
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#ifndef CUR_DATE
#define CUR_DATE	"<compile date not supplied>"
#endif

#ifndef CUR_VER
#define CUR_VER         "U of Colorado/Boulder, CirCUs Release 2.0"
#endif


void TimeOutHandle(void);
void MemOutHandle(void);
char * DateReadFromDateString( char * datestr);
long sat_mem_used(int field);

satArray_t *sat_array_alloc(long num);
satArray_t *sat_array_insert(satArray_t *arr, long datum);
satArray_t *sat_array_alloc_insert(satArray_t *arr, long datum);
satArray_t *sat_array_copy(satArray_t *arr1, satArray_t *arr2);
satArray_t *sat_array_realloc(satArray_t *arr, long size);
satQueue_t *sat_queue_alloc(long num);

int sat_main(char * filename, int timeout, satArray_t* options);

int sat_read_cnf(satManager_t *m, char *filename);
satHeap_t *sat_heap_init(satManager_t *m, int (*compare_heap)(void *, const void *, const void *));
void sat_heap_free(satHeap_t *h);
void sat_heap_insert(satManager_t *m, satHeap_t *h, long n);
void sat_heap_remove_var_assigned_level_zero(satManager_t *m, satHeap_t *h);
long sat_heap_remove_min(satManager_t *m, satHeap_t *h);
int sat_heap_check(satManager_t *m, satHeap_t *h, long i);
void sat_heap_update(satManager_t *m, satHeap_t *h, long n);
void sat_heap_resize(satManager_t *m, satHeap_t *h, long prenVars);
int compare_sort_learned(const void *x1, const void *y1);
int compare_sort_variable_id(const void *x1, const void *y1);
int compare_sort_learned(const void *x1, const void *y1);
int compare_sort_theory(const void *x1, const void *y1);
int compare_sort_block(const void *x1, const void *y1);
void sat_generate_next_restart_bound(satManager_t *m);
void sat_print_clause_array(satManager_t *m, satArray_t *learned);
void sat_decide_polarity_new(satManager_t *m);
void sat_reduce_blocking_clauses(satManager_t *m);
int sat_compare_activity(void *activity, const void *x, const void *y);
int sat_print_unsat_core(satManager_t *m, char *cnfFilename);
void sat_print_assignment(satManager_t *m);

satArray_t *sat_optimize_clause_with_implication_graph(satManager_t *m, satArray_t *clearned);
void sat_array_delete_elem(satArray_t *arr, long elem);
void sat_enqueue_check(satManager_t *m, long lit, satClause_t *ante);
void sat_circus_solve(satManager_t *m);
void sat_dpll(satManager_t *m, long nConflicts);
int sat_backward_subsumption_check(satManager_t *m);
void sat_enqueue(satManager_t *m, long lit, satClause_t *ante);
void sat_add_watched_literal(satManager_t *m, satClause_t *c);
void sat_delete_watched_literal(satManager_t *m, satClause_t *c);
void sat_delete_clause(satManager_t *m, satClause_t *c);
void sat_simplify(satManager_t *m);
void sat_undo(satManager_t *m, long level);
void sat_reduce_learned_clauses(satManager_t *m);
void sat_update_clause_activity(satManager_t *m, satClause_t *c);
void sat_update_variable_activity(satManager_t *m, long v);
void sat_update_clause_decay(satManager_t *m);
void sat_update_variable_decay(satManager_t *m);
void sat_print_literal(satManager_t *m, long lit, FILE *fp);
void sat_print_clause(satManager_t *m, satClause_t *c);
void sat_verify(satManager_t *m);
int sat_verify_original_cnf(satManager_t *m, char *filename);
void sat_remove_satisfied_clauses(satManager_t *m, satArray_t *arr);
void sat_report_result(satManager_t *m);
void sat_free_manager(satManager_t *m);
void sat_conflict_analysis_for_literal(satManager_t *m, long tLit);
void sat_conflict_analysis_strong(satManager_t *m, satClause_t *conflicting, long sLimit, long implLimit);
void sat_conflict_analysis_supplemental(satManager_t *m, satClause_t *conflicting, long refV, long sLimit);
long sat_conflict_analysis_empowerment(satManager_t *m, satClause_t *conflicting, long rLevel);
void sat_init_variable_activity(satManager_t *m, satClause_t *c);
void sat_check_equivalent_relation(satManager_t *m);
void sat_print_dot_for_implication_graph( satManager_t *m, satClause_t *c, long level, int iAllLevel);
void sat_print_clause_simple(satManager_t *m, satClause_t *c);
void sat_print_clauses(satManager_t *m, satArray_t *learned);
void sat_print_cnf(satManager_t *m, long iter);
void sat_clean_up_equi_job(satManager_t *m, satArray_t *save0);
void sat_update_equivalent_class(satManager_t *m, satArray_t *arr, long leanred);
void sat_decide_polarity(satManager_t *m);


satClause_t *sat_implication(satManager_t *m);
satClause_t *sat_add_clause(satManager_t *m, satArray_t *arr, long learned);
satClause_t *sat_add_clause_only(satManager_t *m, satArray_t *arr, long learned);
satClause_t *sat_new_clause(satArray_t *arr, long learned);
satClause_t *sat_check_equivalent_relation_aux(satManager_t *m);

long sat_get_mapped_index(satManager_t *m, long index);
long sat_abstract_level(satManager_t *m, long v);
long sat_make_decision(satManager_t *m);
long sat_conflict_analysis(satManager_t *m, satClause_t *conflicting);
void sat_estimate_progress(satManager_t *m);
void sat_print_cnf_less_than(FILE *fp, satArray_t *arr, long limit);
void sat_print_implication_graph(satManager_t *m, long level);
void sat_print_database(satManager_t *m);
void sat_print_variables(satManager_t *m);
int sat_read_cnf(satManager_t *m, char *filename);
void sat_create_database(satManager_t *m);
int sat_check_complementary(int depth, int nLits, double avg);
void sat_change_search_direction(satManager_t *m);
int sat_is_redundant_lit(satManager_t *m, long lit, long absLevel);
void sat_check_marks(satManager_t *m);
void sat_decide_restart(satManager_t *m, long nConflicts);
satClause_t * sat_add_learned_clause(satManager_t *m, satArray_t *learned);
void sat_reduce_theory_clauses(satManager_t *m);
void sat_make_dependent_graph(satManager_t *m, satClause_t *c);
void sat_generate_unsat_core_main(satManager_t *m);
void sat_generate_unsat_core(satManager_t *m, satClause_t *cl);
void sat_free_clause_array(satArray_t *arr);

char *sat_remove_space(char *line);
char *sat_copy_word(char *lp, char *word);
double sat_drand(satManager_t *m);
satManager_t * sat_init_manager();
void sat_mark_for_pure_lits(satManager_t *m, satClause_t *c);
satArray_t * sat_generate_unsat_core_clauses_index_array(satManager_t *m);
satClause_t * sat_add_theory_clause(satManager_t *m, satArray_t *learned);
satClause_t * sat_add_blocking_clause(satManager_t *m, satArray_t *learned);
void sat_add_blocking_clause_for_theorem_prover(satManager_t *m, satArray_t *arr);

int smt_get_size_of_atomic_variable(satManager_t *m);
int smt_call_theory_solver(satManager_t *m, long bound);
void smt_theory_undo(satManager_t *m);
void sat_print_clause_in_dimacs(FILE *fp, satArray_t *arr);

void sat_init_options_for_varelim(satManager_t *m);
void sat_init_options_for_distill(satManager_t *m);

void sat_distill_clauses_array(satManager_t *m, satArray_t* clauses, long learned);
void sat_choose_candidates_for_distillation(satManager_t *m, satArray_t* clauses);
void sat_reshape_cnf_database_with_distilled_clauses(satManager_t *m, int checkSubsumption);
void sat_squeeze_clauses_array(satManager_t *m, int checkSubsumption);
void sat_build_ternary_tree(satManager_t *m, satArray_t *clauses);
void sat_ternary_tree_based_implication(satManager_t *m, satTernary_t *ternary, int depth, long learned);
void sat_distill_clauses_with_restarting(satManager_t *m);
void sat_distill_clauses_with_preprocessing(satManager_t *m);
void sat_distill_clauses(satManager_t *m);
void sat_report_result_for_distillation(satManager_t *m);
void sat_print_array_as_clause(satManager_t *m, satArray_t *arr);
void sat_add_all_watched_literal(satManager_t *m, satClause_t *c);
void sat_sort_literal_by_score(satArray_t *arr, long *scores);
void sat_sort_literal_by_score_aux(long *lits, long *scores, long size);
void sat_insert_ternary_tree(satTernary_t *root, satArray_t *clause);
void sat_free_clause(satClause_t *c);
void sat_make_decision_based_on_trie(satManager_t *m, long lit);
void sat_conflict_analysis_on_decisions(satManager_t *m, satArray_t *clearned, satClause_t *traversed, long learned);
void sat_ternary_tree_based_undo(satManager_t *m, long level);
void sat_print_scores(satManager_t *m);
void sat_assert_pure_literals(satManager_t *m);
void sat_delete_unmakred_clauses_for_simplification(satManager_t *m);
void sat_free_ternary(satTernary_t *ternary);
void sat_sort_clause_array_by_length(satArray_t *cl);
void sat_strengthen_clause_in_conflict_analysis(satManager_t *m, satClause_t *c, int marked);
int sat_check_subsumption_resolvent_and_clause(satManager_t *m, satClause_t *c, long nMarks);
long sat_conflict_analysis_with_distillation(satManager_t *m, satClause_t *conflicting, long learned);
int sat_check_subsumption_in_conflict_analysis(satManager_t *m, satClause_t *cp, satClause_t *cq);
int sat_recompute_var_score(satManager_t *m);
satClause_t* sat_resolvent_analysis(satManager_t *m, satTernary_t *t, long learned);
satClause_t * sat_implication_for_simplification(satManager_t *m);
satClause_t* sat_add_distilled_clause(satManager_t *m, satArray_t *arr, long learned);
long sat_get_decision_lit(satManager_t *m, long level);
void sat_check_marked_variables_on_decision_stack(satManager_t *m);
void sat_traverse_ternary_tree_to_print_out_dot(satManager_t *m, FILE *fp, satTernary_t *ternary, long *nNode);


int sat_eliminate_var_main(satManager_t *m);
int sat_eliminate_var(satManager_t *m, long v);
int sat_merge_sort_literals(satManager_t *m, satClause_t *cp, satClause_t *cq, long cpindex, long cqindex, long v);
int sat_strengthen_clause(satManager_t *m, satClause_t *c, long index);
int sat_elimination_progress(satManager_t *m);
void sat_extend_model(satManager_t *m);
void sat_reset_all_watched_lists(satManager_t *m);
void sat_build_occurrence_list(satManager_t *m);
satClause_t * sat_implication_on_all_watched_literals(satManager_t *m);
int sat_backward_subsumption_check(satManager_t *m);
void sat_gather_touched_clauses(satManager_t *m);
void sat_recover_clauses_DB(satManager_t *m);
int sat_squeeze_clause(satManager_t *m, satClause_t *c);
void sat_remove_marked_clauses(satManager_t *m, satArray_t *arr);
void sat_init_clauses_statistics(satManager_t *m);
void sat_update_clauses_statistics(satManager_t *m, satClause_t *c);
long sat_check_clauses_high_density(satManager_t *m);
void sat_print_clauses_histogram(satManager_t *m);
void sat_check_duplications_in_clauses(satArray_t *clauses);
int sat_check_clauses_duplicate(satClause_t *cp, satClause_t *cq);
void sat_strengthen_clause_in_conflict_analysis(satManager_t *m, satClause_t *c, int marked);
void sat_strengthen_set_of_clauses_in_conflict_analysis(satManager_t *m);
int sat_check_subsumption_in_conflict_analysis(satManager_t *m, satClause_t *cp, satClause_t *cq);
int sat_check_subsumption_resolvent_and_clause(satManager_t *m, satClause_t *c, long nMarks);
satClause_t *sat_copy_clause(satManager_t *m, satClause_t *c);
void sat_calculate_restart_bound_new(satManager_t *m);
void sat_check_duplicate_literals(satManager_t *m, satClause_t *c);
int sat_minimize_conflict(satManager_t *m, long v, int depth);
void sat_cleanup_for_minimize_conflict(satManager_t *m, satArray_t *arr);
void sat_check_duplicate_literals(satManager_t *m, satClause_t *c);
long sat_number_of_current_implications(satManager_t *m);
satClause_t * sat_binary_implication(satManager_t *m);
satClause_t* sat_find_binary_clause(satManager_t *m, long a, long b);
void sat_print_options(satManager_t *m);
void sat_assert_pure_literals(satManager_t *m);
int sat_minimize_asserting(satManager_t *m, long v, int depth);
void sat_cleanup_for_minimize_assert(satManager_t *m, satArray_t *arr);
void sat_insert_clauses_into_subsumption_check_queue(satManager_t *m, satArray_t *clauses);
long sat_get_literal_index_of_clause(satManager_t *m, satClause_t *c, long lit);
void sat_set_clause_deleted(satManager_t *m, satClause_t *c);

void sat_add_resolvents_from_lit_pool(satManager_t *m, satArray_t *pool);
void sat_report_result_for_var_elim(satManager_t *m);
long sat_get_literal_index_of_clause(satManager_t *m, satClause_t *c, long lit);
void sat_calculate_clause_abs(satClause_t *c);
void sat_clean_all_watched_lists_of_clause(satManager_t *m, satClause_t *c);
void sat_clean_all_watched_list_of_literal(satManager_t *m, long lit);
void sat_clean_all_watched_list_of_variable(satManager_t *m, long v);
long sat_get_num_assignments_of_a_level(satManager_t *m, long level);
void sat_clean_resolvents_DB(satManager_t *m, long v, long begin);
void sat_mark_clauses_of_var_deleted(satManager_t *m, long v);
void sat_mark_occur_list_to_be_deleted(satManager_t *m, long index);
void sat_find_value_of_eliminated_var_on_clauses(satManager_t *m, satArray_t *clauses, long v);
void sat_make_resolution_graph(satClause_t *c, satClause_t *ct);
void sat_delete_dependencies_of_clause_array(satArray_t *arr);
long sat_delete_redundant_resolvents(satManager_t *m, satClause_t *cp);
void sat_check_resolvent_dependencies(satManager_t *m, satClause_t *cp, satClause_t *cq, satClause_t *c);
void sat_print_clause_array_part(satManager_t *m, satArray_t *arr, long begin, long end);
void sat_print_current_DB_to_cnf(satManager_t *m, char *cnfFilename);
void sat_write_eliminated_DB(satManager_t *m, int turnOffClauses);
void sat_check_all_watched_list_of_eliminsated_variables(satManager_t *m);
long sat_check_unit_clause(satManager_t *m, satClause_t *c);
int sat_check_clause_after_merge_sort(satManager_t *m, satArray_t *arr, long begin);
int sat_check_all_clauses_sorted(satManager_t *m);
int sat_delete_clause_from_watched_list(satManager_t *m, satClause_t *c, long wlindex, long cindex);
int sat_verify_watched_literal(satManager_t *m, satClause_t *c);

inline long sat_subsume_on_sorted_clauses(satManager_t *m, satClause_t *cp, satClause_t *cq); 
inline long sat_subsume_on_clauses(satManager_t *m, satClause_t *cp, satClause_t *cq);

int sat_compress_clause(satManager_t *m, satClause_t *c);
void sat_sort_literal_aux(long *lits, long size);
void sat_sort_clause_array(satArray_t *arr, int (*compare_sort)(const void *, const void *));
void sat_sort_clause_array_aux(long *carr, long size,  int (*compare_sort)(const void *, const void *));
void sat_literal_array_sort(satArray_t *arr);
void sat_sort_clause_literal(satClause_t *c);

void sat_heap_up(satManager_t *m, satHeap_t *h, long i);
void sat_heap_down(satManager_t *m, satHeap_t *h, long i);

satQueue_t* sat_queue_init(long maxElements);
void sat_queue_clear(satQueue_t *Q);
void sat_queue_free(satQueue_t *Q);
void sat_queue_insert(satQueue_t *Q, long n);
long sat_queue_pop(satQueue_t *Q);
void sat_queue_print(satQueue_t *Q);
void vel_heap_remove_var_eliminated(satManager_t *m);
void vel_heap_up(satManager_t *m, long i);
void vel_heap_down(satManager_t *m, long i);
long vel_heap_remove_min(satManager_t *m);
void vel_heap_clear(satManager_t *m);
void vel_heap_update(satManager_t *m, long n);
void vel_heap_init(satManager_t *m, long size);
void vel_heap_print(satManager_t *m);
void vel_heap_free(satManager_t *m);
int vel_heap_check(satManager_t *m, long i);
int vel_heap_inHeap(satManager_t *m, long n);
void vel_heap_insert(satManager_t *m, long n);

satStack_t* sat_stack_init(long maxElements);
void sat_stack_clear(satStack_t *stack);
void sat_stack_free(satStack_t *stack);
satStack_t* sat_stack_push(satStack_t *stack, long n);
long sat_stack_pop(satStack_t *stack);
void sat_stack_print(satStack_t *stack);
satSCC_t * sat_scc_alloc(long size);
long sat_find_repr(satManager_t *m, long lit);
void sat_update_repr(satManager_t *m, long litp, long litq);
void sat_strongly_connected_component(satManager_t *m);