/**
 * Copyright (c) 2016-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 at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
import at.ac.tuwien.kr.alpha.core.common.Assignment;
import at.ac.tuwien.kr.alpha.core.common.AtomStore;
import at.ac.tuwien.kr.alpha.core.common.IntIterator;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize;
import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf;
import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral;
import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isPositive;
import static at.ac.tuwien.kr.alpha.core.solver.Atoms.isAtom;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.FALSE;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE;

/**
 * An implementation of Assignment using a trail (of literals) and arrays as underlying structures for storing
 * assignments.
 *
 * Copyright (c) 2018-2020, the Alpha Team.
 */
public class TrailAssignment implements WritableAssignment, Checkable {
	private static final Logger LOGGER = LoggerFactory.getLogger(TrailAssignment.class);
	static final Antecedent CLOSING_INDICATOR_ANTECEDENT = new Antecedent() {
		int[] literals = new int[0];

		@Override
		public int[] getReasonLiterals() {
			return literals;
		}

		@Override
		public void bumpActivity() {
		}

		@Override
		public void decreaseActivity() {
		}

		@Override
		public String toString() {
			return "ClosingIndicatorAntecedent";
		}
	};

	private final AtomStore atomStore;
	private ChoiceManager choiceManagerCallback;

	/**
	 * Contains for each known atom a value whose two least
	 * significant bits encode the atom's truth value
	 * (cf. {@link TrailAssignment#translateTruth(int)}
	 * and whose remaining bits encode the atom's weak decision level. 
	 */
	private int[] values;

	private int[] strongDecisionLevels;
	private Antecedent[] impliedBy;
	private boolean[] callbackUponChange;
	private ArrayList<OutOfOrderLiteral> outOfOrderLiterals = new ArrayList<>();
	private int highestDecisionLevelContainingOutOfOrderLiterals;
	private int[] trail = new int[0];
	private int trailSize;
	private ArrayList<Integer> trailIndicesOfDecisionLevels = new ArrayList<>();

	private int nextPositionInTrail;
	private int newAssignmentsIterator;
	private int mbtCount;
	private boolean didChange;
	private boolean checksEnabled;
	long replayCounter;

	public TrailAssignment(AtomStore atomStore, boolean checksEnabled) {
		this.checksEnabled = checksEnabled;
		this.atomStore = atomStore;
		this.values = new int[0];
		this.strongDecisionLevels = new int[0];
		this.impliedBy = new Antecedent[0];
		this.callbackUponChange = new boolean[0];
		this.trailIndicesOfDecisionLevels.add(0);
		nextPositionInTrail = 0;
		newAssignmentsIterator = 0;
	}

	public TrailAssignment(AtomStore atomStore) {
		this(atomStore, false);
	}

	@Override
	public void clear() {
		mbtCount = 0;
		Arrays.fill(values, 0);
		Arrays.fill(strongDecisionLevels, -1);
		Arrays.fill(impliedBy, null);
		Arrays.fill(callbackUponChange, false);
		outOfOrderLiterals = new ArrayList<>();
		highestDecisionLevelContainingOutOfOrderLiterals = 0;
		Arrays.fill(trail, 0);
		trailSize = 0;
		trailIndicesOfDecisionLevels = new ArrayList<>();
		trailIndicesOfDecisionLevels.add(0);
		nextPositionInTrail = 0;
		newAssignmentsIterator = 0;
	}

	@Override
	public void registerCallbackOnChange(int atom) {
		callbackUponChange[atom] = true;
	}

	@Override
	public void setCallback(ChoiceManager choiceManager) {
		choiceManagerCallback = choiceManager;
	}

	@Override
	public boolean isAssigned(int atom) {
		return values[atom] != 0;
	}

	@Override
	public int getBasicAtomAssignedMBT() {
		for (int atom = 1; atom <= atomStore.getMaxAtomId(); atom++) {
			if (getTruth(atom) == MBT && atomStore.get(atom) instanceof BasicAtom) {
				return atom;
			}
		}
		throw oops("No BasicAtom is assigned MBT.");
	}

	@Override
	public Pollable getAssignmentsToProcess() {
		return new TrailPollable();
	}

	@Override
	public int getRealWeakDecisionLevel(int atom) {
		if (getTruth(atom) == null) {
			return -1;
		}
		int lowestDecisionLevelForAtom = getWeakDecisionLevel(atom);
		for (OutOfOrderLiteral outOfOrderLiteral : outOfOrderLiterals) {
			if (outOfOrderLiteral.atom == atom && outOfOrderLiteral.decisionLevel < lowestDecisionLevelForAtom) {
				lowestDecisionLevelForAtom = outOfOrderLiteral.decisionLevel;
			}
		}
		return lowestDecisionLevelForAtom;
	}

	/**
	 * Searches out-of-order literals for the lowest decision level the atom is assigned in.
	 * @param atom the atom to check.
	 * @return Integer.MAX_VALUE if the atom is not assigned out-of-order, otherwise the lowest decision level it is assigned.
	 */
	public int getOutOfOrderDecisionLevel(int atom) {
		int lowestDecisionLevel = Integer.MAX_VALUE;
		for (OutOfOrderLiteral outOfOrderLiteral : outOfOrderLiterals) {
			if (outOfOrderLiteral.atom == atom && outOfOrderLiteral.decisionLevel < lowestDecisionLevel) {
				lowestDecisionLevel = outOfOrderLiteral.decisionLevel;
			}
		}
		return lowestDecisionLevel;
	}

	int getOutOfOrderStrongDecisionLevel(int atom) {
		int lowestDecisionLevel = Integer.MAX_VALUE;
		for (OutOfOrderLiteral outOfOrderLiteral : outOfOrderLiterals) {
			if (outOfOrderLiteral.atom == atom && outOfOrderLiteral.value == TRUE && outOfOrderLiteral.decisionLevel < lowestDecisionLevel) {
				lowestDecisionLevel = outOfOrderLiteral.decisionLevel;
			}
		}
		return lowestDecisionLevel;
	}

	private void informCallback(int atom) {
		if (callbackUponChange[atom]) {
			choiceManagerCallback.callbackOnChanged(atom);
		}
	}

	private void removeLastDecisionLevel() {
		// Remove all atoms recorded in the highest decision level.
		int start = trailIndicesOfDecisionLevels.get(getDecisionLevel());
		for (int i = start; i < trailSize; i++) {
			int backtrackAtom = atomOf(trail[i]);
			// Skip already backtracked atoms.
			if (getTruth(backtrackAtom) == null) {
				continue;
			}
			if (getWeakDecisionLevel(backtrackAtom) < getDecisionLevel()) {
				// Restore TRUE to MBT if this was assigned at a lower level.
				if (getTruth(backtrackAtom) != TRUE) {
					throw oops("Backtracking assignment with lower decision level whose value is not TRUE.");
				}
				values[backtrackAtom] = (getWeakDecisionLevel(backtrackAtom) << 2) | translateTruth(MBT);
				mbtCount++;
			} else {
				if (getTruth(backtrackAtom) == MBT) {
					mbtCount--;
				}
				values[backtrackAtom] = 0;
			}
			strongDecisionLevels[backtrackAtom] = -1;
			informCallback(backtrackAtom);
			didChange = true;
		}
		// Remove atoms from trail.
		trailSize = start;
		trailIndicesOfDecisionLevels.remove(trailIndicesOfDecisionLevels.size() - 1);
	}

	private void replayOutOfOrderLiterals() {
		// Replay out-of-order assigned literals.
		if (highestDecisionLevelContainingOutOfOrderLiterals >= getDecisionLevel()) {
			// Replay all still-valid literals and remove invalid ones.
			LOGGER.trace("Replaying out-of-order literals.");
			int k = 0; // counter for out-of-order literals to keep further.
			for (OutOfOrderLiteral outOfOrderLiteral : outOfOrderLiterals) {
				if (outOfOrderLiteral.decisionLevel <= getDecisionLevel()) {
					// Replay assignment at current decision level.
					assign(outOfOrderLiteral.atom, outOfOrderLiteral.value, outOfOrderLiteral.impliedBy);
					// If literal is actually below current decision level, keep it.
					if (outOfOrderLiteral.decisionLevel < getDecisionLevel()) {
						outOfOrderLiterals.set(k++, outOfOrderLiteral);
					}
				}
			}
			replayCounter += outOfOrderLiterals.size();
			if (LOGGER.isTraceEnabled()) {
				LOGGER.trace("Replay list contained {} literals, {} were again assigned. Overall replays: {}.", outOfOrderLiterals.size(), k, replayCounter);
			}
			// Remove remaining entries from k onwards.
			while (outOfOrderLiterals.size() > k) {
				outOfOrderLiterals.remove(outOfOrderLiterals.size() - 1);
			}
			highestDecisionLevelContainingOutOfOrderLiterals = outOfOrderLiterals.isEmpty() ? 0 : getDecisionLevel();
		}
	}

	private void resetTrailPointersAndReplayOutOfOrderLiterals() {
		nextPositionInTrail = Math.min(nextPositionInTrail, trailSize);
		newAssignmentsIterator = Math.min(newAssignmentsIterator, trailSize);
		replayOutOfOrderLiterals();
		if (checksEnabled) {
			runInternalChecks();
		}
	}

	@Override
	public void backjump(int decisionLevel) {
		// Remove everything above the target level, but keep the target level unchanged.
		while (getDecisionLevel() > decisionLevel) {
			removeLastDecisionLevel();
		}
		resetTrailPointersAndReplayOutOfOrderLiterals();
	}

	@Override
	public void backtrack() {
		removeLastDecisionLevel();
		resetTrailPointersAndReplayOutOfOrderLiterals();
	}

	@Override
	public int getMBTCount() {
		return mbtCount;
	}

	@Override
	public ConflictCause choose(int atom, ThriceTruth value) {
		if (checksEnabled) {
			runInternalChecks();
		}
		trailIndicesOfDecisionLevels.add(trailSize);
		return assign(atom, value, null);
	}

	@Override
	public ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy) {
		ConflictCause conflictCause = assignWithTrail(atom, value, impliedBy);
		if (conflictCause != null && LOGGER.isDebugEnabled()) {
			LOGGER.debug("Assign is conflicting: atom: {}, value: {}, impliedBy: {}.", atom, value, impliedBy);
		}
		return conflictCause;
	}

	@Override
	public ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy, int decisionLevel) {
		ConflictCause conflictCause = assign(atom, value, impliedBy);
		if (conflictCause == null && decisionLevel < getDecisionLevel()) {
			outOfOrderLiterals.add(new OutOfOrderLiteral(atom, value, decisionLevel, impliedBy));
			if (highestDecisionLevelContainingOutOfOrderLiterals < getDecisionLevel()) {
				highestDecisionLevelContainingOutOfOrderLiterals = getDecisionLevel();
			}
		}
		return conflictCause;
	}

	private boolean assignmentsConsistent(ThriceTruth oldTruth, ThriceTruth value) {
		return oldTruth == null || oldTruth.toBoolean() == value.toBoolean();
	}

	private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent impliedBy) {
		if (!isAtom(atom)) {
			throw new IllegalArgumentException("not an atom");
		}
		if (value == null) {
			throw new IllegalArgumentException("value must not be null");
		}
		if (LOGGER.isTraceEnabled()) {
			LOGGER.trace("Recording assignment {}={}@{} impliedBy: {}", atom, value, getDecisionLevel(), impliedBy);
			if (impliedBy != null) {
				Antecedent fullAntecedent = impliedBy;
				if (impliedBy instanceof ShallowAntecedent) {
					fullAntecedent = ((ShallowAntecedent) impliedBy).instantiateAntecedent(atomToLiteral(atom, value.toBoolean()));
				}
				for (Integer literal : fullAntecedent.getReasonLiterals()) {
					LOGGER.trace("impliedBy literal assignment: {}={}.", atomOf(literal), get(atomOf(literal)));
				}
			}
		}

		// If the atom currently is not assigned, simply record the assignment.
		final ThriceTruth currentTruth = getTruth(atom);
		if (currentTruth == null) {
			trail[trailSize++] = atomToLiteral(atom, value.toBoolean());
			values[atom] = (getDecisionLevel() << 2) | translateTruth(value);
			this.impliedBy[atom] = impliedBy;
			// Adjust MBT counter.
			if (value == MBT) {
				mbtCount++;
			}
			if (value == TRUE) {
				strongDecisionLevels[atom] = getDecisionLevel();
			}
			informCallback(atom);
			didChange = true;
			return null;
		}

		// Nothing to do if the new value is the same as the current one (or current is TRUE and new is MBT).
		if (value == currentTruth || value == MBT && currentTruth == TRUE) {
			return null;
		}

		// Check if the new assignments contradicts the current one.
		if (!assignmentsConsistent(currentTruth, value)) {
			// Assignments are inconsistent, prepare the reason.
			// Due to the conflict, the impliedBy NoGood is not the recorded one but the one this method is invoked with.stems from this assignment.
			if (impliedBy instanceof ShallowAntecedent) {
				// Instantiate Antecedent in case it is a shallow one for binary nogoods.
				return new ConflictCause(((ShallowAntecedent) impliedBy).instantiateAntecedent(atomToLiteral(atom, !value.toBoolean())));
			}
			return new ConflictCause(impliedBy);
		}
		if (value == TRUE && currentTruth != MBT) {
			throw oops("Assigning TRUE without assigning MBT before.");
		}

		// Previous assignment exists, and the new one is consistent with it.
		// There is nothing to do except if MBT becomes TRUE.
		if (currentTruth == MBT && value == TRUE) {
			// Record new truth value but keep weak decision level unchanged.
			trail[trailSize++] = atomToLiteral(atom, true);
			values[atom] = (getWeakDecisionLevel(atom) << 2) | translateTruth(TRUE);
			// Record strong decision level.
			strongDecisionLevels[atom] = getDecisionLevel();
			// Adjust MBT counter.
			mbtCount--;
			informCallback(atom);
			didChange = true;
			return null;
		}
		throw oops("Assignment conditions are not covered.");
	}

	private ThriceTruth translateTruth(int value) {
		switch (value & 0x3) {
			case 0:
				return null;
			case 1:
				return FALSE;
			case 2:
				return MBT;
			case 3:
				return TRUE;
			default:
				throw oops("Unknown truth value.");
		}
	}

	private int translateTruth(ThriceTruth value) {
		if (value == null) {
			return 0;
		}
		switch (value) {
			case FALSE:
				return 1;
			case MBT:
				return 2;
			case TRUE:
				return 3;
		}
		throw oops("Unknown truth value.");
	}

	@Override
	public ThriceTruth getTruth(int atom) {
		return translateTruth(values[atom]);
	}

	@Override
	public int getWeakDecisionLevel(int atom) {
		return values[atom] >> 2;
	}

	@Override
	public int getStrongDecisionLevel(int atom) {
		return getTruth(atom) == FALSE ? getWeakDecisionLevel(atom) : strongDecisionLevels[atom];
	}

	@Override
	public Antecedent getImpliedBy(int atom) {
		Antecedent antecedent = impliedBy[atom];
		// Check if the Antecedent is a shallow one from binary nogoods, in this case instantiate it to a full Antecedent.
		if (antecedent instanceof ShallowAntecedent) {
			return ((ShallowAntecedent) antecedent).instantiateAntecedent(atomToLiteral(atom, !getTruth(atom).toBoolean()));
		}
		return antecedent;
	}

	@Override
	public Set<Integer> getTrueAssignments() {
		Set<Integer> result = new HashSet<>();
		for (int i = 0; i < values.length; i++) {
			if (getTruth(i) == TRUE) {
				result.add(i);
			}
		}
		return result;
	}

	@Override
	public Entry get(int atom) {
		if (values[atom] == 0) {
			return null;
		}
		if (strongDecisionLevels[atom] == -1) {
			return new Entry(getTruth(atom), atom, getWeakDecisionLevel(atom), getImpliedBy(atom));
		} else {
			return new Entry(getTruth(atom), atom, strongDecisionLevels[atom], getImpliedBy(atom), getWeakDecisionLevel(atom));
		}
	}

	private void runInternalChecks() {
		// Ensure that incrementally updated values agree with actual values.
		LOGGER.trace("Checking assignment.");
		// Check that MBT counter is correct.
		if (getMBTCount() != getMBTAssignedAtoms().size()) {
			throw oops("MBT counter and amount of actually MBT-assigned atoms disagree");
		} else {
			LOGGER.trace("MBT count agrees with amount of MBT-assigned atoms.");
		}
		// Check that out of order literals are actually assigned.
		for (OutOfOrderLiteral outOfOrderLiteral : outOfOrderLiterals) {
			if (outOfOrderLiteral.decisionLevel <= getDecisionLevel()) {
				ThriceTruth atomTruth = getTruth(outOfOrderLiteral.atom);
				if (outOfOrderLiteral.value == atomTruth || outOfOrderLiteral.value == MBT && atomTruth == TRUE) {
					continue;
				}
				throw oops("Out-of-order assigned literal is not in current assignment.");
			}
		}
		LOGGER.trace("Checking assignment: all good.");
	}

	/**
	 * Debug helper collecting all atoms that are assigned MBT.
	 * @return a list of all atomIds that are assigned MBT (and not TRUE).
	 */
	private List<Integer> getMBTAssignedAtoms() {
		List<Integer> ret = new ArrayList<>();
		for (int i = 0; i < values.length; i++) {
			if (getTruth(i) == MBT) {
				ret.add(i);
			}
		}
		return ret;
	}

	@Override
	public boolean closeUnassignedAtoms() {
		boolean didAssign = false;
		for (int i = 1; i <= atomStore.getMaxAtomId(); i++) {
			if (!isAssigned(i)) {
				assign(i, FALSE, CLOSING_INDICATOR_ANTECEDENT);
				didAssign = true;
			}
		}
		return didAssign;
	}

	@Override
	public boolean didChange() {
		boolean oldDidChange = didChange;
		didChange = false;
		return oldDidChange;
	}

	@Override
	public void growForMaxAtomId() {
		int maxAtomId = atomStore.getMaxAtomId();
		// Grow arrays only if needed.
		if (values.length > maxAtomId) {
			return;
		}
		// Grow by 1.5 current size, except if bigger array is required due to maxAtomId.
		int newCapacity = arrayGrowthSize(values.length);
		if (newCapacity < maxAtomId + 1) {
			newCapacity = maxAtomId + 1;
		}
		values = Arrays.copyOf(values, newCapacity);
		int oldLength = strongDecisionLevels.length;
		strongDecisionLevels = Arrays.copyOf(strongDecisionLevels, newCapacity);
		Arrays.fill(strongDecisionLevels, oldLength, strongDecisionLevels.length, -1);
		impliedBy = Arrays.copyOf(impliedBy, newCapacity);
		callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity);
		trail = Arrays.copyOf(trail, newCapacity * 2);	// Trail has at most 2 assignments (MBT+TRUE) for each atom.
	}

	public int getNumberOfAssignedAtoms() {
		int n = 0;
		for (int value : values) {
			if (translateTruth(value) != null) {
				n++;
			}
		}
		return n;
	}

	@Override
	public int getNumberOfAtomsAssignedSinceLastDecision() {
		Set<Integer> newlyAssignedAtoms = new HashSet<>();
		int trailIndex = trailIndicesOfDecisionLevels.get(getDecisionLevel());
		for (; trailIndex < trailSize; trailIndex++) {
			newlyAssignedAtoms.add(atomOf(trail[trailIndex]));
		}
		return newlyAssignedAtoms.size();
	}

	@Override
	public int getDecisionLevel() {
		return trailIndicesOfDecisionLevels.size() - 1;
	}

	@Override
	public String toString() {
		StringBuilder sb = new StringBuilder("[");
		boolean isFirst = true;
		for (int i = 0; i < values.length; i++) {
			ThriceTruth atomTruth = getTruth(i);
			if (atomTruth == null) {
				continue;
			}
			if (!isFirst) {
				sb.append(", ");
			}
			isFirst = false;
			sb.append(atomTruth);
			sb.append("_");
			if (atomStore != null) {
				sb.append(atomStore.atomToString(i));
			} else {
				sb.append(i);
			}
			sb.append("@");
			sb.append(getWeakDecisionLevel(i));
		}
		sb.append("]");
		return sb.toString();
	}

	@Override
	public AssignmentIterator getNewPositiveAssignmentsIterator() {
		return new AssignmentIterator();
	}

	@Override
	public void setChecksEnabled(boolean checksEnabled) {
		this.checksEnabled = checksEnabled;
	}

	private class AssignmentIterator implements IntIterator {

		private void advanceCursorToNextPositiveAssignment() {
			while (newAssignmentsIterator < trailSize) {
				ThriceTruth truth = getTruth(atomOf(trail[newAssignmentsIterator]));
				if (truth != null && truth.toBoolean()) {
					return;
				}
				newAssignmentsIterator++;
			}
		}

		@Override
		public boolean hasNext() {
			advanceCursorToNextPositiveAssignment();
			return newAssignmentsIterator < trailSize;
		}

		@Override
		public int next() {
			return atomOf(trail[newAssignmentsIterator++]);

		}
	}

	private static class OutOfOrderLiteral {
		final int atom;
		final ThriceTruth value;
		final int decisionLevel;
		final Antecedent impliedBy;

		private OutOfOrderLiteral(int atom, ThriceTruth value, int decisionLevel, Antecedent impliedBy) {
			this.atom = atom;
			this.decisionLevel = decisionLevel;
			this.impliedBy = impliedBy;
			this.value = value;
		}

		@Override
		public String toString() {
			return atom + "=" + value + "@" + decisionLevel + " implied by " + impliedBy;
		}
	}

	private class TrailPollable implements Pollable {

		@Override
		public int peek() {
			return atomOf(trail[nextPositionInTrail]);
		}

		@Override
		public int remove() {
			int current = peek();
			nextPositionInTrail++;
			return current;
		}

		@Override
		public boolean isEmpty() {
			return nextPositionInTrail >= trailSize;
		}
	}

	public TrailBackwardsWalker getTrailBackwardsWalker() {
		return new TrailBackwardsWalker();
	}

	public class TrailBackwardsWalker {

		int trailPos;

		TrailBackwardsWalker() {
			trailPos = trailSize;
		}

		public int getNextLowerLiteral() {
			return trail[--trailPos];
		}

		@Override
		public String toString() {
			StringBuilder sb = new StringBuilder("[");
			for (int i = 0; i < trailSize; i++) {
				int literalOnTrail = trail[i];
				sb.append(isPositive(literalOnTrail) ? "+" + atomOf(literalOnTrail) : "-" + atomOf(literalOnTrail));
				sb.append("@");
				sb.append(TrailAssignment.this.getWeakDecisionLevel(atomOf(literalOnTrail)));
				sb.append(", ");
			}
			sb.append("]");
			return sb.toString();
		}
	}

	private static final class Entry implements Assignment.Entry {
		private final ThriceTruth value;
		private final int decisionLevel;
		private final int previousDecisionLevel;
		private final Antecedent impliedBy;
		private final int atom;

		Entry(ThriceTruth value, int atom, int decisionLevel, Antecedent noGood) {
			this(value, atom, decisionLevel, noGood, -1);
		}

		Entry(ThriceTruth value, int atom, int decisionLevel, Antecedent impliedBy, int previousDecisionLevel) {
			this.value = value;
			this.decisionLevel = decisionLevel;
			this.impliedBy = impliedBy;
			this.previousDecisionLevel = previousDecisionLevel;
			this.atom = atom;
			if (previousDecisionLevel != -1 && value != TRUE) {
				throw oops("Assignment.Entry instantiated with previous entry set and truth values other than TRUE now and MBT previous");
			}
		}

		@Override
		public ThriceTruth getTruth() {
			return value;
		}

		@Override
		public int getDecisionLevel() {
			return decisionLevel;
		}

		@Override
		public boolean hasPreviousMBT() {
			return previousDecisionLevel != -1;
		}

		@Override
		public int getMBTDecisionLevel() {
			return previousDecisionLevel;
		}

		@Override
		public Antecedent getImpliedBy() {
			return impliedBy;
		}

		@Override
		public int getAtom() {
			return atom;
		}

		@Override
		public boolean equals(Object o) {
			if (this == o) {
				return true;
			}
			if (o == null || getClass() != o.getClass()) {
				return false;
			}

			Entry entry = (Entry) o;

			return atom == entry.atom;
		}

		@Override
		public int hashCode() {
			return atom;
		}

		@Override
		public String toString() {
			return atom + "=" + value.toString() + "(DL" + decisionLevel + ")"
				+ (hasPreviousMBT() ? "MBT(DL" + getMBTDecisionLevel() + ")" : "");
		}
	}
}
