/*!
 * Copyright (c) <2023> <Andreas Niskanen, University of Helsinki>
 * 
 * 
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 
 * 
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 * 
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

#ifdef DEBUG
#include <iostream>
#endif

#include "Encodings.h"
#include "ipasir.h"

using namespace std;

namespace Encodings {

void add_clause(const DynamicAF & af, void * solver, const vector<int> & clause)
{
#ifdef DEBUG
	cout << "ipasir_add ";
#endif
	for (uint32_t i = 0; i < clause.size(); i++) {
		ipasir_add(solver, clause[i]);
#ifdef DEBUG
		cout << (clause[i] > 0 ? "+" : "-") << af.var_to_str.at(abs(clause[i])) << " ";
#endif
	}
	ipasir_add(solver, 0);
#ifdef DEBUG
	cout << "\n";
#endif
}

void assume_lit(const DynamicAF & af, void * solver, const int32_t lit)
{
	ipasir_assume(solver, lit);
#ifdef DEBUG
	cout << "ipasir_assume " << (lit > 0 ? "+" : "-") << af.var_to_str.at(abs(lit)) << "\n";
#endif
}

void add_rejected_clauses(const DynamicAF & af, void * solver)
{
#ifdef DEBUG
	cout << "c Adding rejected clauses to solver\n";
#endif
	if (af.static_mode) {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			vector<int> clause = { -af.rejected_var[i], -af.accepted_var[i] };
			add_clause(af, solver, clause);
		}
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			for (const int32_t & j : af.attackers[i]) {
				vector<int> clause = { af.rejected_var[i], -af.accepted_var[j] };
				add_clause(af, solver, clause);
			}
		}
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			vector<int> clause = { -af.rejected_var[i] };
			for (const int32_t & j : af.attackers[i]) {
				clause.push_back(af.accepted_var[j]);
			}
			add_clause(af, solver, clause);
		}
	} else {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.arg_encoded[i]) continue;
			vector<int> clause = { -af.arg_exists_var[i], -af.rejected_var[i], -af.accepted_var[i] };
			add_clause(af, solver, clause);
		}
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.atts_encoded[i]) continue;
			for (const int32_t & j : af.attackers[i]) {
				vector<int> clause = { -af.attackers_var[i], af.rejected_var[i], -af.accepted_var[j] };
				add_clause(af, solver, clause);
			}
		}
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.atts_encoded[i]) continue;
			vector<int> clause = { -af.attackers_var[i], -af.rejected_var[i] };
			for (const int32_t & j : af.attackers[i]) {
				clause.push_back(af.accepted_var[j]);
			}
			add_clause(af, solver, clause);
		}
	}
}

void add_range(const DynamicAF & af, void * solver)
{
#ifdef DEBUG
	cout << "c Adding range clauses to solver\n";
#endif
	if (af.static_mode) {
		if (af.sem == STG) {
			for (uint32_t i = 0; i < af.args; i++) {
				if (!af.arg_exists[i]) continue;
				vector<int> clause = { af.range_var[i], -af.accepted_var[i] };
				add_clause(af, solver, clause);
			}
			for (uint32_t i = 0; i < af.args; i++) {
				if (!af.arg_exists[i]) continue;
				for (const int32_t & j : af.attackers[i]) {
					vector<int> clause = { af.range_var[i], -af.accepted_var[j] };
					add_clause(af, solver, clause);
				}
			}
			for (uint32_t i = 0; i < af.args; i++) {
				if (!af.arg_exists[i]) continue;
				vector<int> clause = { -af.range_var[i], af.accepted_var[i] };
				for (const int32_t & j : af.attackers[i]) {
					clause.push_back(af.accepted_var[j]);
				}
				add_clause(af, solver, clause);
			}
		} else {
			for (uint32_t i = 0; i < af.args; i++) {
				if (!af.arg_exists[i]) continue;
				vector<int> clause = { af.range_var[i], -af.accepted_var[i] };
				add_clause(af, solver, clause);
			}
			for (uint32_t i = 0; i < af.args; i++) {
				if (!af.arg_exists[i]) continue;
				vector<int> clause = { af.range_var[i], -af.rejected_var[i] };
				add_clause(af, solver, clause);
			}
			for (uint32_t i = 0; i < af.args; i++) {
				if (!af.arg_exists[i]) continue;
				vector<int> clause = { -af.range_var[i], af.accepted_var[i], af.rejected_var[i] };
				add_clause(af, solver, clause);
			}
		}
	} else {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.arg_encoded[i]) continue;
			vector<int> clause = { af.range_var[i], -af.accepted_var[i] };
			add_clause(af, solver, clause);
		}
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.arg_encoded[i]) continue;
			vector<int> clause = { af.range_var[i], -af.rejected_var[i] };
			add_clause(af, solver, clause);
		}
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.arg_encoded[i]) continue;
			vector<int> clause = { -af.range_var[i], af.accepted_var[i], af.rejected_var[i] };
			add_clause(af, solver, clause);
		}
	}
}

void add_conflict_free(const DynamicAF & af, void * solver)
{
#ifdef DEBUG
	cout << "c Adding conflict-free clauses to solver\n";
#endif
	if (af.static_mode) {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			for (const int32_t & j : af.attackers[i]) {
				vector<int> clause;
				if ((int32_t)i != j) {
					clause = { -af.accepted_var[i], -af.accepted_var[j] };
				} else {
					clause = { -af.accepted_var[i] };
				}
				add_clause(af, solver, clause);
			}
		}
	} else {
		add_rejected_clauses(af, solver);
	}
}

void add_admissible(const DynamicAF & af, void * solver)
{
	add_conflict_free(af, solver);
	if (af.static_mode) add_rejected_clauses(af, solver);
#ifdef DEBUG
	cout << "c Adding admissible clauses to solver\n";
#endif
	if (af.static_mode) {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.attackers[i].contains(i)) continue;
			for (const int32_t & j : af.attackers[i]) {
				if (af.attackers[j].contains(i)) continue;
				vector<int> clause = { -af.accepted_var[i], af.rejected_var[j] };
				add_clause(af, solver, clause);
			}
		}
	} else {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			//if (af.attackers[i].contains(i)) continue;
			if (af.atts_encoded[i]) continue;
			for (const int32_t & j : af.attackers[i]) {
				//if (af.attackers[j].contains(i)) continue;
				vector<int> clause = { -af.attackers_var[i], -af.accepted_var[i], af.rejected_var[j] };
				add_clause(af, solver, clause);
			}
		}
	}
}

void add_complete(const DynamicAF & af, void * solver)
{
	add_admissible(af, solver);
#ifdef DEBUG
	cout << "c Adding complete clauses to solver\n";
#endif
	if (af.static_mode) {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			vector<int> clause = { af.accepted_var[i] };
			for (const int32_t & j : af.attackers[i]) {
				clause.push_back(-af.rejected_var[j]);
			}
			add_clause(af, solver, clause);
		}
	} else {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.atts_encoded[i]) continue;
			vector<int> clause = { -af.attackers_var[i], af.accepted_var[i] };
			for (const int32_t & j : af.attackers[i]) {
				clause.push_back(-af.rejected_var[j]);
			}
			add_clause(af, solver, clause);
		}
	}
}

void add_stable(const DynamicAF & af, void * solver)
{
#if defined(AD_IN_ST)
	add_admissible(af, solver);
#elif defined(CO_IN_ST)
	add_complete(af, solver);
#else
	add_conflict_free(af, solver);
	if (af.static_mode) add_rejected_clauses(af, solver);
#endif
#ifdef DEBUG
	cout << "c Adding stable clauses to solver\n";
#endif
	if (af.static_mode) {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			vector<int> clause = { af.accepted_var[i], af.rejected_var[i] };
			add_clause(af, solver, clause);
		}
	} else {
		for (uint32_t i = 0; i < af.args; i++) {
			if (!af.arg_exists[i]) continue;
			if (af.arg_encoded[i]) continue;
			vector<int> clause = { -af.arg_exists_var[i], af.accepted_var[i], af.rejected_var[i] };
			add_clause(af, solver, clause);
		}
	}
}

int32_t add_target(DynamicAF & af, const vector<int32_t> & assumptions, void * solver)
{
	if (assumptions.size() == 0) return 0;
	if (assumptions.size() == 1) return assumptions[0];
	int32_t target_var = ++af.count;
#ifdef DEBUG
	af.var_to_str[target_var] = "target";
#endif
	for (uint32_t i = 0; i < assumptions.size(); i++) {
		vector<int> clause = { -target_var, assumptions[i] };
		add_clause(af, solver, clause);
	}
	vector<int> clause(assumptions.size()+1);
	clause[0] = target_var;
	for (uint32_t i = 0; i < assumptions.size(); i++) {
		clause[i+1] = -assumptions[i];
	}
	add_clause(af, solver, clause);
	return target_var;
}

}