#ifndef __DPLL_H__
#define __DPLL_H__

//#define DPLL_DEBUG 1

//only one of RANDOMIZED_EXPORE and GREEDY_SELECT
//#define RANDOMIZED_EXPLORE 1 
#define GREEDY_SELECT 1

//#define GREEDY_SELECT_2 1

//RANDOMIZED_DIRECTION is useless with greedy.
#define RANDOMIZED_DIRECTION 1 

#define RAND_SEED 551

#define PRINT_STATISTICS 1

struct clause_encloser{
	CLAUSE* clause;
	struct clause_encloser* next;
};

typedef struct clause_encloser CLAUSE_ENCLOSER;

typedef struct dpll_clause_struct{
	int currentLiteralCount;
	int isSatisfied;	//if the clause is satisfied
	int depthSatisfied;	//the min depth at which it was labelled 
				//satisfied
	int* currentLiterals;		
	
} DPLL_CLAUSE;

typedef struct dpll_literal_struct{
	int depthSatisfied;	
	//Clauses where this literal appears as positive or negative.
	CLAUSE_ENCLOSER* positiveClauses;
	CLAUSE_ENCLOSER* negativeClauses;
} DPLL_LITERAL;

typedef struct dpll_stats{
	int maxDepthExplored;
	int nodesExplored;
	int backTracks;
} DPLL_STATS;

CLAUSE_ENCLOSER* emptyClauses;

CLAUSE_ENCLOSER* singleVariableClauses;

DPLL_STATS statistics;

int unsatisfiedClauses;

/* Build data structures for execution of dpll algorithm */
void buildSupportStructures();

/* Run the complete algorithm with the results stored */
void runDPLL();

/* Satisfy the clauses containing the given literal at this depth */
void satisfyClauses(int literal, int depth);

/* Return 1 if all the clauses are satisfied */
int allSatisfed();

/* shorten all clauses containing this literal at a given depth */
void shortenClauses(int literal, int depth);
	
/* Are there empty clauses. Returns 1 if there are and 0 otherwise */
int hasEmptyClauses();

/* Gets unit literal, or returns 0 if there arent any */
int getUnitLiteral();

/* Get pure literal, or returns 0 if there arent any */
int getPureLiteral();

/* Run the dpll step and clean up if the result returned is 0 */
int dpllStepWithCleanUp(int literal, int depth);

/* Run dpll step without any cleaning of the data structure. Not
 * to be called separately without dpllStepWithCleanUp. 
 */
int dpllStep(int literal, int depth);

void printLiteralState();

void printState();

#endif