/* author: Tomas Balyo, KIT, Karlsruhe */
#include <stdio.h>
#include "pblib/pb2cnf.h"
#include "pblib/clausedatabase.h"
#include <vector>

using namespace std;
using namespace PBLib;

// The linked SAT solver might be written in C
extern "C" {
#include "ipasir.h"
}

/**
 * Read a partial maxsat problem from the specified file and add it to the solver
 * with activation literals for the soft clauses. The names of the activation
 * literals are *startVar, ..., *endVar. Returns false if the reading was not
 * successful.
 */
bool readMaxSatProblem(const char* filename, void* solver, int* startActVar, int* endActVar) {
	FILE* f = fopen(filename, "r");
	if (f == NULL) {
		return false;
	}
	int vars, cls, top;
	int c = 0;
	bool neg = false;
	bool first = true;

	while (c != EOF) {
		c = fgetc(f);

		// problem definition line
		if (c == 'p') {
			char pline[512];
			int i = 0;
			while (c != '\n') {
				pline[i++] = c;
				c = fgetc(f);
			}
			pline[i] = 0;
			if (3 != sscanf(pline, "p wcnf %d %d %d", &vars, &cls, &top)) {
				printf("Failed to parse the problem definition line (%s)\n", pline);
				return false;
			}
			vars++;
			*startActVar = vars;
			continue;
		}
		// comment
		if (c == 'c') {
			// skip this line
			while(c != '\n') {
				c = fgetc(f);
			}
			continue;
		}
		// whitespace
		if (isspace(c)) {
			continue;
		}
		// negative
		if (c == '-') {
			neg = true;
			continue;
		}
		// number
		if (isdigit(c)) {
			int num = c - '0';
			c = fgetc(f);
			while (isdigit(c)) {
				num = num*10 + (c-'0');
				c = fgetc(f);
			}
			if (neg) {
				num *= -1;
			}
			neg = false;
			// the first number is the weight
			if (first) {
				first = false;
				// this is a soft clause
				if (num == 1) {
					// will add the next activation literal instead of num
					ipasir_add(solver, vars++);
				}
				continue;
			}
			if (num == 0) {
				first = true;
			}
			// add to the solver
			ipasir_add(solver, num);
		}
	}
	fclose(f);
	*endActVar = vars;
	return true;
}

/**
 * This class is used by the PBLib library to add clauses 
 * of the cardinality constraint to the solver. See the PBLib
 * documentation for more details.
 */
class IpasirClauseDatabase : public ClauseDatabase {
public:
	IpasirClauseDatabase(PBConfig config, void* solver):ClauseDatabase(config),solver(solver) {
	}
protected:
	void* solver;
	void addClauseIntern(const vector<int>& clause) {
		for (size_t i = 0; i < clause.size(); i++) {
			ipasir_add(solver, clause[i]);
		}
		ipasir_add(solver, 0);
	}
};


int main(int argc, char **argv) {
	void * solver = ipasir_init();
	int startActVar, endActVar;

	if (!readMaxSatProblem(argv[1], solver, &startActVar, &endActVar)) {
		puts("Input could not be parsed");
		return 0;
	}

	printf("c The input problem has %d soft clauses.\n", endActVar - startActVar);

	// find an initial solution
	int res = ipasir_solve(solver);
	if (res == 20) {
		puts("Hard clauses are UNSAT");
		return 20;
	}

	// count the number of unsat soft clauses in the initial solution
	// and start constructing a cardinality constraint on the activation
	// literals of all soft clauses.
	int unsatisfiedSoft = 0;
	vector<WeightedLit> lits;
	for (int i = startActVar; i < endActVar; i++) {
		lits.push_back(WeightedLit(i,1));
		if (ipasir_val(solver, i) > 0) {
			unsatisfiedSoft++;
		}
	}
	printf("c initial bound\no %d\n", unsatisfiedSoft);
	int bestResult = unsatisfiedSoft;

	// PBLib initialization code
	AuxVarManager avm(endActVar);
	PBConfig config = make_shared<PBConfigClass>();
	PB2CNF convertor(config);
	IpasirClauseDatabase icd(config, solver);

	// create the first cardinality constraint stating
	// that the number of unsat soft clauses must be smaller than
	// in the initial solution.
	unsatisfiedSoft--;
	IncPBConstraint pbc(lits, LEQ, unsatisfiedSoft);
	convertor.encodeIncInital(pbc, icd, avm);

	// keep strengthening the bound and solving
	// until we reach an unsat formula.
	res = ipasir_solve(solver);
	while (res != 20) {
		// count the unsat soft clauses in the last solution
		unsatisfiedSoft = 0;
		for (int i = startActVar; i < endActVar; i++) {
			if (ipasir_val(solver, i) > 0) {
				unsatisfiedSoft++;
			}
		}
		printf("o %d\n", unsatisfiedSoft);
		bestResult = unsatisfiedSoft;
		// strenghten the cardinality constraint
		unsatisfiedSoft--;
		pbc.encodeNewLeq(unsatisfiedSoft, icd, avm);
		res = ipasir_solve(solver);
	}
	puts("s OPTIMUM FOUND");
	printf("c final-result %d\n", bestResult);
}