/**
 * Copyright (c) 2017-2019, the Alpha Team.
 * All rights reserved.
 *
 * Additional changes made by Siemens.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * 1) Redistributions of source code must retain the above copyright notice, this
 *    list of conditions and the following disclaimer.
 *
 * 2) Redistributions in binary form must reproduce the above copyright notice,
 *    this list of conditions and the following disclaimer in the documentation
 *    and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package at.ac.tuwien.kr.alpha.core.solver;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import at.ac.tuwien.kr.alpha.core.common.NoGood;

import java.util.HashMap;

import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.*;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.*;

public class NaiveNoGoodStore implements NoGoodStore {
	private static final Logger LOGGER = LoggerFactory.getLogger(NaiveNoGoodStore.class);

	private HashMap<Integer, NoGood> delegate = new HashMap<>();
	private final WritableAssignment assignment;
	private final NoGoodCounter counter = new NoGoodCounter();

	private boolean hasInferredAssignments;

	public NaiveNoGoodStore(WritableAssignment assignment) {
		this.assignment = assignment;
	}

	void clear() {
		assignment.clear();
		delegate.clear();
	}

	@Override
	public ConflictCause add(int id, NoGood noGood, int lbd) {
		counter.add(noGood);
		if (assignment.violates(noGood)) {
			return new ConflictCause(noGood.asAntecedent());
		}

		delegate.put(id, noGood);
		return null;
	}

	@Override
	public ConflictCause add(int id, NoGood noGood) {
		return add(id, noGood, Integer.MAX_VALUE);
	}

	@Override
	public ConflictCause propagate() {
		hasInferredAssignments = false;

		boolean any = false;
		boolean retry;

		do {
			retry = false;
			ConflictCause conflictCause;
			for (NoGood noGood : delegate.values()) {
				hasInferredAssignments = false;
				conflictCause = propagateWeakly(noGood);
				if (conflictCause != null) {
					return conflictCause;
				}
				if (hasInferredAssignments) {
					any = true;
					hasInferredAssignments = false;
					retry = true;
				}
			}
			for (NoGood noGood : delegate.values()) {
				hasInferredAssignments = false;
				conflictCause = propagateStrongly(noGood);
				if (conflictCause != null) {
					return conflictCause;
				}
				if (hasInferredAssignments) {
					any = true;
					hasInferredAssignments = false;
					retry = true;
				}
			}
		} while (retry);

		for (NoGood noGood : delegate.values()) {
			if (assignment.violates(noGood)) {
				return new ConflictCause(noGood.asAntecedent());
			}
		}

		if (any) {
			hasInferredAssignments = true;
		}

		return null;
	}

	@Override
	public boolean didPropagate() {
		return hasInferredAssignments;
	}

	@Override
	public void backtrack() {
		assignment.backtrack();
	}

	@Override
	public void growForMaxAtomId(int maxAtomId) {
	}

	@Override
	public NoGoodCounter getNoGoodCounter() {
		return counter;
	}

	@Override
	public void cleanupLearnedNoGoods() {
	}

	/**
	 * Infer an assignment from a nogood if it is weakly unit.
	 *
	 * This method iterates over all literals in the given nogood
	 * in order to check whether it is weakly unit. If the nogood
	 * turns out to be unit, then an assignment is generated and
	 * {@code true} is returned. Otherwise, {@code false} is
	 * returned.
	 *
	 * @param noGood the nogood to analyze.
	 * @return {@code true} iff an assignment was inferred,
	 *         {@code false} otherwise.
	 */
	private ConflictCause propagateWeakly(NoGood noGood) {
		int index = -1;
		for (int i = 0; i < noGood.size(); i++) {
			final int literal = noGood.getLiteral(i);

			if (assignment.isAssigned(atomOf(literal))) {
				if (!assignment.isViolated(literal)) {
					// Literal is satisfied!
					return null;
				}
			} else if (index != -1) {
				// There is more than one unassigned literal!
				return null;
			} else {
				index = i;
			}
		}

		if (index == -1) {
			return null;
		}

		hasInferredAssignments = true;

		final int literal = noGood.getLiteral(index);
		return assignment.assign(atomOf(literal), isNegated(literal) ? MBT : FALSE, noGood.asAntecedent());
	}

	/**
	 * Infer an assignment from a nogood if it is strongly unit.
	 *
	 * This method iterates over all literals in the given nogood
	 * in order to check whether it is strongly unit. If the nogood
	 * turns out to be unit, then an assignment for the head is
	 * generated and {@code true} is returned. Otherwise,
	 * {@code false} is returned.
	 *
	 * @param noGood the nogood to analyze.
	 * @return {@code true} iff an assignment was inferred,
	 *         {@code false} otherwise.
	 */
	private ConflictCause propagateStrongly(NoGood noGood) {
		if (!noGood.hasHead()) {
			return null;
		}

		final int headAtom = atomOf(noGood.getHead());

		if (assignment.getTruth(headAtom) != MBT) {
			return null;
		}

		// Check that NoGood is violated except for the head
		// (i.e., without the head set it would be unit) and
		// that none of the true values are assigned MBT, but
		// instead are all TRUE.
		for (int i = 1; i < noGood.size(); i++) {
			final int literal = noGood.getLiteral(i);

			if (!assignment.isViolated(literal)) {
				return null;
			}

			// Skip if positive literal is assigned MBT.
			if (isPositive(literal) && assignment.getTruth(atomOf(literal)) != TRUE) {
				return null;
			}
		}

		hasInferredAssignments = true;

		return assignment.assign(headAtom, TRUE, noGood.asAntecedent());
	}
}
