/*
 *  mtss.h
 *  mtss Library
 *
 *  Created by Gilles Dequen on 08/07/09 -- :D
 *  Healed by Pascal Vander-Swalmen on 2009/11/20 -- ;)
 *
 */

#ifndef MTSS_H
#define MTSS_H

/// Useful Includes
#include <stdlib.h>
#include <unistd.h>
#include <stdio.h>
#include <sys/resource.h>

/// Constants used
#define MTSS_CLAUSES -10
#define MTSS_RESULT -20
#define MTSS_MAX_BUFFER_SIZE 1000000
#define MTSS_MAX_CLAUSE_SIZE 9

/// Results
#define MTSS_RESULT_SAT 1
#define MTSS_RESULT_UNSAT -1
#define MTSS_RESULT_UNDEF 0

/// Status Values
#define MTSS_SUCCESS 0
#define MTSS_UNDEF -1
#define MTSS_OVERFLOW -2
#define MTSS_PIPE_CLOSED -3
#define MTSS_PIPE_ERROR -4

/// Structure Used to Share Informations
typedef struct mtss_share_struct {
	/// Values Buffer
	int *mtss_share;
	/// Values Index
	int *mtss_share_index;
	/// Values Sizes
	int *mtss_share_size;
	/// Maximum number of Values in the Buffer
	int mtss_max_shared;
	/// Current Index Buffer
	int mtss_share_current;
	/// Index of Previous Block
	int mtss_share_previous;
	/// Number of Blocks of separated Values (Clauses)
	int mtss_blocks;
} mtss_share_t;

#endif

/// --------------------------------------------------
/// File Descriptor Functions
/// --------------------------------------------------

/// Return MTSS_WRITE file descriptor index
int mtss_fd_write(void);
/// Return MTSS_READ file descriptor index
int mtss_fd_read(void);

/// --------------------------------------------------
/// Printing Functions
/// --------------------------------------------------

/// Print an MTSS Sharing Structure (screen)
void mtss_share_print(mtss_share_t *, char *);
/// Log an MTSS Sharing Structure in a File
void mtss_share_log(FILE *, mtss_share_t *, char *);

/// --------------------------------------------------
/// 'Maximum Size of Object' Functions
/// --------------------------------------------------

/// Update Variable of Maximum Size of MTSS Sharing Structure
void mtss_share_set_default_max_size(int);
/// Return Maximum Size of an MTSS Sharing Structure
int mtss_share_get_maxsize(mtss_share_t *);

/// --------------------------------------------------
/// Memory Management Functions
/// --------------------------------------------------

/// Init an MTSS Sharing Structure (call it only one time before use)
void mtss_share_init(mtss_share_t *, int);
/// Destroy an MTSS Sharing Structure (call it one time before exit)
void mtss_share_destroy(mtss_share_t *);

/// --------------------------------------------------
/// Sharing Object Management Functions
/// --------------------------------------------------

/// Reset MTSS Sharing Structure Indexes between 2 utilizations
void mtss_share_reset(mtss_share_t *);
/// reBuilding of an MTSS Sharing Structure
void mtss_share_build(mtss_share_t *);
/// Add a Literal in the Clauses Buffer
int mtss_share_add_literal(mtss_share_t *, int);
/// Finish Clause in an MTSS Sharing Structure
int mtss_share_end_clause(mtss_share_t *);
/// Add a Clause in an MTSS Sharing Structure
/// You can use this function if you know the size of the added clause or not
int mtss_share_add_clause(mtss_share_t *, int *, int);

/// --------------------------------------------------
/// Guiding Path Functions
/// --------------------------------------------------

/// Add an Assigned Variable (~ literal) in an MTSS Sharing Structure to be used like a Guiding Path
int mtss_share_extend_guiding_path(mtss_share_t *, int);

/// --------------------------------------------------
/// Miscellanous Functions
/// --------------------------------------------------

/// Return Size of the Clause 'i' in the MTSS Sharing Structure
int mtss_share_get_clause_size(mtss_share_t *, int);
/// Return Index of the Clause 'i' in the MTSS Sharing Structure
int mtss_share_get_clause_start(mtss_share_t *, int);
/// Copy the Clause 'i' from the MTSS Sharing Structure to an Array of Integers
// not yet tested!
int mtss_share_get_clause(mtss_share_t *, int, int *);
/// Return the Literal 'j' from the Clause 'i' in the MTSS Sharing Structure
int mtss_share_get_literal(mtss_share_t *, int, int);
/// Return Result stored in an MTSS Sharing Structure
int mtss_share_get_result(mtss_share_t *);
/// Return Number of Decisions stored in an MTSS Sharing Structure
int mtss_share_get_decisions(mtss_share_t *);
/// Return Decision of the Guiding Path in an MTSS Sharing Structure
int mtss_share_extract_guiding_path(mtss_share_t *, int);

/// --------------------------------------------------
/// Send Informations
/// --------------------------------------------------

/// Send Clauses from External Solvers to MTSS
int mtss_share_send_clauses(mtss_share_t *);
/// Send Result and Number of Decisions from External Solvers to MTSS
int mtss_share_send_result(mtss_share_t *, const int, int);
/// Send Guiding Path from MTSS to External Solvers
int mtss_share_send_guiding_path(int private_write, mtss_share_t *);
/// Send Clauses from MTSS to External Solvers
int mtss_share_send_clauses_thread_safe(int private_write, mtss_share_t *);

/// --------------------------------------------------
/// Receive Informations
/// --------------------------------------------------

/// Receive Clauses in External Solvers from MTSS
int mtss_share_receive_clauses(mtss_share_t *);
/// Receive Guiding Path in External Solvers from MTSS
int mtss_share_receive_guiding_path(mtss_share_t *);
/// Receive Clauses or Result or Number of Decisions in MTSS from External Solvers
int mtss_share_receive_informations(int private_read, mtss_share_t *);