/**
 * Copyright (c) 2016-2019, the Alpha Team.
 * All rights reserved.
 * <p>
 * Additional changes made by Siemens.
 * <p>
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 * <p>
 * 1) Redistributions of source code must retain the above copyright notice, this
 * list of conditions and the following disclaimer.
 * <p>
 * 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.
 * <p>
 * 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.grounder;

import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.SortedSet;
import java.util.TreeSet;

import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Pair;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import at.ac.tuwien.kr.alpha.api.AnswerSet;
import at.ac.tuwien.kr.alpha.api.config.GrounderHeuristicsConfiguration;
import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.Predicate;
import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
import at.ac.tuwien.kr.alpha.api.programs.literals.Literal;
import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm;
import at.ac.tuwien.kr.alpha.commons.AnswerSets;
import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution;
import at.ac.tuwien.kr.alpha.commons.substitutions.Instance;
import at.ac.tuwien.kr.alpha.commons.util.Util;
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 at.ac.tuwien.kr.alpha.core.common.NoGood;
import at.ac.tuwien.kr.alpha.core.common.NoGoodInterface;
import at.ac.tuwien.kr.alpha.core.grounder.bridges.Bridge;
import at.ac.tuwien.kr.alpha.core.grounder.instantiation.AssignmentStatus;
import at.ac.tuwien.kr.alpha.core.grounder.instantiation.BindingResult;
import at.ac.tuwien.kr.alpha.core.grounder.instantiation.DefaultLazyGroundingInstantiationStrategy;
import at.ac.tuwien.kr.alpha.core.grounder.instantiation.LiteralInstantiationResult;
import at.ac.tuwien.kr.alpha.core.grounder.instantiation.LiteralInstantiator;
import at.ac.tuwien.kr.alpha.core.grounder.structure.AnalyzeUnjustified;
import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram;
import at.ac.tuwien.kr.alpha.core.programs.atoms.ChoiceAtom;
import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom;
import at.ac.tuwien.kr.alpha.core.programs.rules.CompiledRule;

/**
 * A semi-naive grounder.
 *
 * Copyright (c) 2016-2020, the Alpha Team.
 */
public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGrounder {
	private static final Logger LOGGER = LoggerFactory.getLogger(NaiveGrounder.class);

	private final WorkingMemory workingMemory = new WorkingMemory();
	private final AtomStore atomStore;
	private final NogoodRegistry registry = new NogoodRegistry();
	final NoGoodGenerator noGoodGenerator;
	private final ChoiceRecorder choiceRecorder;
	private final CompiledProgram program;
	private final AnalyzeUnjustified analyzeUnjustified;

	private final Map<Predicate, LinkedHashSet<Instance>> factsFromProgram;
	private final Map<IndexedInstanceStorage, ArrayList<FirstBindingAtom>> rulesUsingPredicateWorkingMemory = new HashMap<>();
	private final Map<Integer, CompiledRule> knownNonGroundRules;

	private ArrayList<CompiledRule> fixedRules = new ArrayList<>();
	private LinkedHashSet<Atom> removeAfterObtainingNewNoGoods = new LinkedHashSet<>();
	private final boolean debugInternalChecks;

	private final GrounderHeuristicsConfiguration heuristicsConfiguration;

	// Handles instantiation of literals, i.e. supplies ground substitutions for literals of non-ground rules
	// according to the rules set by the LiteralInstantiationStrategy used by this grounder.
	private final LiteralInstantiator ruleInstantiator;
	private final DefaultLazyGroundingInstantiationStrategy instantiationStrategy;

	public NaiveGrounder(CompiledProgram program, AtomStore atomStore, boolean debugInternalChecks, Bridge... bridges) {
		this(program, atomStore, new GrounderHeuristicsConfiguration(), debugInternalChecks, bridges);
	}

	private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks,
			Bridge... bridges) {
		this(program, atomStore, p -> true, heuristicsConfiguration, debugInternalChecks, bridges);
	}

	NaiveGrounder(CompiledProgram program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter,
			GrounderHeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks, Bridge... bridges) {
		super(filter, bridges);
		this.atomStore = atomStore;
		this.heuristicsConfiguration = heuristicsConfiguration;
		LOGGER.debug("Grounder configuration: {}", heuristicsConfiguration);

		this.program = program;

		this.factsFromProgram = program.getFactsByPredicate();
		this.knownNonGroundRules = program.getRulesById();

		this.analyzeUnjustified = new AnalyzeUnjustified(this.program, this.atomStore, this.factsFromProgram);

		this.initializeFactsAndRules();

		final Set<CompiledRule> uniqueGroundRulePerGroundHead = getRulesWithUniqueHead();
		choiceRecorder = new ChoiceRecorder(atomStore);
		noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, this.program, uniqueGroundRulePerGroundHead);

		this.debugInternalChecks = debugInternalChecks;

		// Initialize RuleInstantiator and instantiation strategy. Note that the instantiation strategy also
		// needs the current assignment, which is set with every call of getGroundInstantiations.
		this.instantiationStrategy = new DefaultLazyGroundingInstantiationStrategy(this.workingMemory, this.atomStore, this.factsFromProgram,
				this.heuristicsConfiguration.isAccumulatorEnabled());
		this.instantiationStrategy.setStaleWorkingMemoryEntries(this.removeAfterObtainingNewNoGoods);
		this.ruleInstantiator = new LiteralInstantiator(this.instantiationStrategy);
	}

	private void initializeFactsAndRules() {
		// Initialize all facts.
		for (Atom fact : program.getFacts()) {
			final Predicate predicate = fact.getPredicate();

			// Record predicate
			workingMemory.initialize(predicate);
		}

		// Register internal atoms.
		workingMemory.initialize(RuleAtom.PREDICATE);
		workingMemory.initialize(ChoiceAtom.OFF);
		workingMemory.initialize(ChoiceAtom.ON);

		// Initialize rules and constraints in working memory.
		for (CompiledRule nonGroundRule : program.getRulesById().values()) {
			// Create working memories for all predicates occurring in the rule.
			for (Predicate predicate : nonGroundRule.getOccurringPredicates()) {
				// FIXME: this also contains interval/builtin predicates that are not needed.
				workingMemory.initialize(predicate);
			}

			// If the rule has fixed ground instantiations, it is not registered but grounded once like facts.
			if (nonGroundRule.getGroundingInfo().hasFixedInstantiation()) {
				fixedRules.add(nonGroundRule);
				continue;
			}

			// Register each starting literal at the corresponding working memory.
			for (Literal literal : nonGroundRule.getGroundingInfo().getStartingLiterals()) {
				registerLiteralAtWorkingMemory(literal, nonGroundRule);
			}
		}
	}

	private Set<CompiledRule> getRulesWithUniqueHead() {
		// FIXME: below optimisation (adding support nogoods if there is only one rule instantiation per unique atom over the interpretation) could
		// be done as a transformation (adding a non-ground constraint corresponding to the nogood that is generated by the grounder).
		// Record all unique rule heads.
		final Set<CompiledRule> uniqueGroundRulePerGroundHead = new HashSet<>();

		for (Map.Entry<Predicate, LinkedHashSet<CompiledRule>> headDefiningRules : program.getPredicateDefiningRules().entrySet()) {
			if (headDefiningRules.getValue().size() != 1) {
				continue;
			}

			CompiledRule nonGroundRule = headDefiningRules.getValue().iterator().next();
			// Check that all variables of the body also occur in the head (otherwise grounding is not unique).
			Atom headAtom = nonGroundRule.getHeadAtom();

			// Rule is not guaranteed unique if there are facts for it.
			HashSet<Instance> potentialFacts = factsFromProgram.get(headAtom.getPredicate());
			if (potentialFacts != null && !potentialFacts.isEmpty()) {
				continue;
			}

			// Collect head and body variables.
			HashSet<VariableTerm> occurringVariablesHead = new HashSet<>(headAtom.toLiteral().getBindingVariables());
			HashSet<VariableTerm> occurringVariablesBody = new HashSet<>();
			for (Literal lit : nonGroundRule.getPositiveBody()) {
				occurringVariablesBody.addAll(lit.getBindingVariables());
			}
			occurringVariablesBody.removeAll(occurringVariablesHead);

			// Check if ever body variables occurs in the head.
			if (occurringVariablesBody.isEmpty()) {
				uniqueGroundRulePerGroundHead.add(nonGroundRule);
			}
		}
		return uniqueGroundRulePerGroundHead;
	}

	/**
	 * Registers a starting literal of a NonGroundRule at its corresponding working memory.
	 * 
	 * @param nonGroundRule the rule in which the literal occurs.
	 */
	private void registerLiteralAtWorkingMemory(Literal literal, CompiledRule nonGroundRule) {
		if (literal.isNegated()) {
			throw new RuntimeException("Literal to register is negated. Should not happen.");
		}
		IndexedInstanceStorage workingMemory = this.workingMemory.get(literal.getPredicate(), true);
		rulesUsingPredicateWorkingMemory.putIfAbsent(workingMemory, new ArrayList<>());
		rulesUsingPredicateWorkingMemory.get(workingMemory).add(new FirstBindingAtom(nonGroundRule, literal));
	}

	@Override
	public AnswerSet assignmentToAnswerSet(Iterable<Integer> trueAtoms) {
		Map<Predicate, SortedSet<Atom>> predicateInstances = new LinkedHashMap<>();
		SortedSet<Predicate> knownPredicates = new TreeSet<>();

		// Iterate over all true atomIds, computeNextAnswerSet instances from atomStore and add them if not filtered.
		for (int trueAtom : trueAtoms) {
			final Atom atom = atomStore.get(trueAtom);
			Predicate predicate = atom.getPredicate();

			// Skip atoms over internal predicates.
			if (predicate.isInternal()) {
				continue;
			}

			// Skip filtered predicates.
			if (!filter.test(predicate)) {
				continue;
			}

			knownPredicates.add(predicate);
			predicateInstances.putIfAbsent(predicate, new TreeSet<>());
			Set<Atom> instances = predicateInstances.get(predicate);
			instances.add(atom);
		}

		// Add true atoms from facts.
		for (Map.Entry<Predicate, LinkedHashSet<Instance>> facts : factsFromProgram.entrySet()) {
			Predicate factPredicate = facts.getKey();
			// Skip atoms over internal predicates.
			if (factPredicate.isInternal()) {
				continue;
			}
			// Skip filtered predicates.
			if (!filter.test(factPredicate)) {
				continue;
			}
			// Skip predicates without any instances.
			if (facts.getValue().isEmpty()) {
				continue;
			}
			knownPredicates.add(factPredicate);
			predicateInstances.putIfAbsent(factPredicate, new TreeSet<>());
			for (Instance factInstance : facts.getValue()) {
				SortedSet<Atom> instances = predicateInstances.get(factPredicate);
				instances.add(Atoms.newBasicAtom(factPredicate, factInstance.terms));
			}
		}

		if (knownPredicates.isEmpty()) {
			return AnswerSets.EMPTY_SET;
		}

		return AnswerSets.newAnswerSet(knownPredicates, predicateInstances);
	}

	/**
	 * Prepares facts of the input program for joining and derives all NoGoods representing ground rules. May only be called once.
	 * 
	 * @return
	 */
	protected HashMap<Integer, NoGood> bootstrap() {
		final HashMap<Integer, NoGood> groundNogoods = new LinkedHashMap<>();

		for (Predicate predicate : factsFromProgram.keySet()) {
			// Instead of generating NoGoods, add instance to working memories directly.
			workingMemory.addInstances(predicate, true, factsFromProgram.get(predicate));
		}

		for (CompiledRule nonGroundRule : fixedRules) {
			// Generate NoGoods for all rules that have a fixed grounding.
			RuleGroundingOrder groundingOrder = nonGroundRule.getGroundingInfo().getFixedGroundingOrder();
			BindingResult bindingResult = getGroundInstantiations(nonGroundRule, groundingOrder, new BasicSubstitution(), null);
			groundAndRegister(nonGroundRule, bindingResult.getGeneratedSubstitutions(), groundNogoods);
		}

		fixedRules = null;

		return groundNogoods;
	}

	@Override
	public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
		// In first call, prepare facts and ground rules.
		final Map<Integer, NoGood> newNoGoods = fixedRules != null ? bootstrap() : new LinkedHashMap<>();

		// Compute new ground rule (evaluate joins with newly changed atoms)
		for (IndexedInstanceStorage modifiedWorkingMemory : workingMemory.modified()) {
			// Skip predicates solely used in the solver which do not occur in rules.
			Predicate workingMemoryPredicate = modifiedWorkingMemory.getPredicate();
			if (workingMemoryPredicate.isSolverInternal()) {
				continue;
			}

			// Iterate over all rules whose body contains the interpretation corresponding to the current workingMemory.
			final ArrayList<FirstBindingAtom> firstBindingAtoms = rulesUsingPredicateWorkingMemory.get(modifiedWorkingMemory);

			// Skip working memories that are not used by any rule.
			if (firstBindingAtoms == null) {
				continue;
			}

			for (FirstBindingAtom firstBindingAtom : firstBindingAtoms) {
				// Use the recently added instances from the modified working memory to construct an initial substitution
				CompiledRule nonGroundRule = firstBindingAtom.rule;

				// Generate substitutions from each recent instance.
				for (Instance instance : modifiedWorkingMemory.getRecentlyAddedInstances()) {
					// Check instance if it matches with the atom.

					final Substitution unifier = BasicSubstitution.specializeSubstitution(firstBindingAtom.startingLiteral, instance,
							BasicSubstitution.EMPTY_SUBSTITUTION);

					if (unifier == null) {
						continue;
					}

					final BindingResult bindingResult = getGroundInstantiations(
							nonGroundRule,
							nonGroundRule.getGroundingInfo().orderStartingFrom(firstBindingAtom.startingLiteral),
							unifier,
							currentAssignment);

					groundAndRegister(nonGroundRule, bindingResult.getGeneratedSubstitutions(), newNoGoods);
				}
			}

			// Mark instances added by updateAssignment as done
			modifiedWorkingMemory.markRecentlyAddedInstancesDone();
		}

		workingMemory.reset();
		for (Atom removeAtom : removeAfterObtainingNewNoGoods) {
			final IndexedInstanceStorage storage = workingMemory.get(removeAtom, true);
			Instance instance = new Instance(removeAtom.getTerms());
			if (storage.containsInstance(instance)) {
				// permissive grounder heuristics may attempt to remove instances that are not yet in the working memory
				storage.removeInstance(instance);
			}
		}

		// Re-Initialize the stale working memory entries set and pass to instantiation strategy.
		removeAfterObtainingNewNoGoods = new LinkedHashSet<>();
		instantiationStrategy.setStaleWorkingMemoryEntries(removeAfterObtainingNewNoGoods);
		if (LOGGER.isDebugEnabled()) {
			LOGGER.debug("Grounded NoGoods are:");
			for (Map.Entry<Integer, NoGood> noGoodEntry : newNoGoods.entrySet()) {
				LOGGER.debug("{} == {}", noGoodEntry.getValue(), atomStore.noGoodToString(noGoodEntry.getValue()));
			}
			LOGGER.debug("{}", choiceRecorder);
		}

		if (debugInternalChecks) {
			checkTypesOfNoGoods(newNoGoods.values());
		}

		return newNoGoods;
	}

	/**
	 * Grounds the given {@code nonGroundRule} by applying the given {@code substitutions} and registers the nogoods generated during that
	 * process.
	 *
	 * @param nonGroundRule the rule to be grounded.
	 * @param substitutions the substitutions to be applied.
	 * @param newNoGoods    a set of nogoods to which newly generated nogoods will be added.
	 */
	private void groundAndRegister(final CompiledRule nonGroundRule, final List<Substitution> substitutions, final Map<Integer, NoGood> newNoGoods) {
		for (Substitution substitution : substitutions) {
			List<NoGood> generatedNoGoods = noGoodGenerator.generateNoGoodsFromGroundSubstitution(nonGroundRule, substitution);
			registry.register(generatedNoGoods, newNoGoods);
		}
	}

	@Override
	public int register(NoGood noGood) {
		return registry.register(noGood);
	}

	// Ideally, this method should be private. It's only visible because NaiveGrounderTest needs to access it.
	BindingResult getGroundInstantiations(CompiledRule rule, RuleGroundingOrder groundingOrder, Substitution partialSubstitution,
			Assignment currentAssignment) {
		int tolerance = heuristicsConfiguration.getTolerance(rule.isConstraint());
		if (tolerance < 0) {
			tolerance = Integer.MAX_VALUE;
		}

		// Update instantiationStrategy with current assignment.
		// Note: Actually the assignment could be an instance variable of the grounder (shared with solver),
		// but this would have a larger impact on grounder/solver communication design as a whole.
		instantiationStrategy.setCurrentAssignment(currentAssignment);
		BindingResult bindingResult = bindNextAtomInRule(groundingOrder, 0, tolerance, tolerance, partialSubstitution);
		if (LOGGER.isDebugEnabled()) {
			for (int i = 0; i < bindingResult.size(); i++) {
				Integer numberOfUnassignedPositiveBodyAtoms = bindingResult.getNumbersOfUnassignedPositiveBodyAtoms().get(i);
				if (numberOfUnassignedPositiveBodyAtoms > 0) {
					LOGGER.debug("Grounded rule in which {} positive atoms are still unassigned: {} (substitution: {})", numberOfUnassignedPositiveBodyAtoms,
							rule, bindingResult.getGeneratedSubstitutions().get(i));
				}
			}
		}
		return bindingResult;
	}

	/**
	 * Helper method used by {@link NaiveGrounder#bindNextAtomInRule(RuleGroundingOrderImpl, int, int, int, BasicSubstitution)}.
	 *
	 * Takes an <code>ImmutablePair</code> of a {@link BasicSubstitution} and an accompanying {@link AssignmentStatus} and calls
	 * <code>bindNextAtomInRule</code> for the next literal in the grounding order.
	 * If the assignment status for the last bound literal was {@link AssignmentStatus#UNASSIGNED}, the <code>remainingTolerance</code>
	 * parameter is decreased by 1. If the remaining tolerance drops below zero, this method returns an empty {@link BindingResult}.
	 *
	 * @param groundingOrder
	 * @param orderPosition
	 * @param originalTolerance
	 * @param remainingTolerance
	 * @param lastLiteralBindingResult
	 * @return the result of calling bindNextAtomInRule on the next literal in the grounding order, or an empty binding result if remaining
	 *         tolerance is less than zero.
	 */
	private BindingResult continueBinding(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance,
			ImmutablePair<Substitution, AssignmentStatus> lastLiteralBindingResult) {
		Substitution substitution = lastLiteralBindingResult.left;
		AssignmentStatus lastBoundLiteralAssignmentStatus = lastLiteralBindingResult.right;
		switch (lastBoundLiteralAssignmentStatus) {
			case TRUE:
				return advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, substitution);
			case UNASSIGNED:
				// The last literal bound to obtain the current substitution has not been assigned a truth value by the solver yet.
				// If we still have enough tolerance, we can continue grounding nevertheless.
				int toleranceForNextRun = remainingTolerance - 1;
				if (toleranceForNextRun >= 0) {
					return advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, toleranceForNextRun, substitution);
				} else {
					return BindingResult.empty();
				}
			case FALSE:
				throw Util.oops("Got an assignmentStatus FALSE for literal " + groundingOrder.getLiteralAtOrderPosition(orderPosition) + " and substitution "
						+ substitution + " - should not happen!");
			default:
				throw Util.oops("Got unsupported assignmentStatus " + lastBoundLiteralAssignmentStatus);
		}
	}

	private BindingResult advanceAndBindNextAtomInRule(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance,
			Substitution partialSubstitution) {
		groundingOrder.considerUntilCurrentEnd();
		return bindNextAtomInRule(groundingOrder, orderPosition + 1, originalTolerance, remainingTolerance, partialSubstitution);
	}

	private BindingResult pushBackAndBindNextAtomInRule(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance,
			Substitution partialSubstitution) {
		RuleGroundingOrder modifiedGroundingOrder = groundingOrder.pushBack(orderPosition);
		if (modifiedGroundingOrder == null) {
			return BindingResult.empty();
		}
		return bindNextAtomInRule(modifiedGroundingOrder, orderPosition + 1, originalTolerance, remainingTolerance, partialSubstitution);
	}

	//@formatter:off
	/**
	 * Computes ground substitutions for a literal based on a {@link RuleGroundingOrderImpl} and a {@link BasicSubstitution}.
	 *
	 * Computes ground substitutions for the literal at position <code>orderPosition</code> of <code>groundingOrder</code>
	 * Actual substitutions are computed by this grounder's {@link LiteralInstantiator}. 
	 *
	 * @param groundingOrder a {@link RuleGroundingOrderImpl} representing the body literals of a rule in the 
	 * 						 sequence in which the should be bound during grounding.
	 * @param orderPosition the current position within <code>groundingOrder</code>, indicates which literal should be bound
	 * @param originalTolerance the original tolerance of the used grounding heuristic
	 * @param remainingTolerance the remaining tolerance, determining if binding continues in the presence of substitutions based on unassigned atoms
	 * @param partialSubstitution a substitution
	 * @return a {@link BindingResult} representing applicable ground substitutions for all literals after orderPosition in groundingOrder
	 */
	//@formatter:on
	private BindingResult bindNextAtomInRule(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance,
			Substitution partialSubstitution) {
		Literal currentLiteral = groundingOrder.getLiteralAtOrderPosition(orderPosition);
		if (currentLiteral == null) {
			LOGGER.trace("No more literals found in grounding order, therefore stopping binding!");
			return BindingResult.singleton(partialSubstitution, originalTolerance - remainingTolerance);
		}
		LOGGER.trace("Binding current literal {} with remaining tolerance {} and partial substitution {}.", currentLiteral,
				remainingTolerance, partialSubstitution);
		LiteralInstantiationResult instantiationResult = ruleInstantiator.instantiateLiteral(currentLiteral, partialSubstitution);
		switch (instantiationResult.getType()) {
			case CONTINUE:
				/*
				 * Recursively call bindNextAtomInRule for each generated substitution
				 * and the next literal in the grounding order (i.e. advance), thereby reducing remaining
				 * tolerance by 1 iff a substitution uses an unassigned ground atom.
				 * If remainingTolerance falls below zero, an empty {@link BindingResult} is returned.
				 */
				List<ImmutablePair<Substitution, AssignmentStatus>> substitutionInfos = instantiationResult.getSubstitutions();
				LOGGER.trace("Literal instantiator yielded {} substitutions for literal {}.", substitutionInfos.size(), currentLiteral);
				BindingResult retVal = new BindingResult();
				for (ImmutablePair<Substitution, AssignmentStatus> substitutionInfo : substitutionInfos) {
					retVal.add(this.continueBinding(groundingOrder, orderPosition, originalTolerance, remainingTolerance,
							substitutionInfo));
				}
				return retVal;
			case PUSH_BACK:
				/*
				 * Delegate to pushBackAndBindNextAtomInRule(RuleGroundingOrder, int, int, int, Substitution, Assignment).
				 * Pushes the current literal to the end of the grounding order and calls bindNextAtomInRule with the modified grounding oder.
				 */
				LOGGER.trace("Pushing back literal {} in grounding order.", currentLiteral);
				return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution);
			case MAYBE_PUSH_BACK:
				/*
				 * Indicates that the rule instantiator could not find any substitutions for the current literal. If a permissive grounder heuristic is in
				 * use, push the current literal to the end of the grounding order and proceed with the next one, otherwise return an empty BindingResult.
				 */
				if (originalTolerance > 0) {
					LOGGER.trace(
							"No substitutions yielded by literal instantiator for literal {}, but using permissive heuristic, therefore pushing the literal back.",
							currentLiteral);
					// This occurs when the grounder heuristic in use is a "permissive" one,
					// i.e. it is deemed acceptable to have ground rules where a number of body atoms are not yet assigned a truth value by the solver.
					return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution);
				} else {
					LOGGER.trace("No substitutions found for literal {}", currentLiteral);
					return BindingResult.empty();
				}
			case STOP_BINDING:
				LOGGER.trace("No substitutions found for literal {}", currentLiteral);
				return BindingResult.empty();
			default:
				throw Util.oops("Unhandled literal instantiation result type: " + instantiationResult.getType());
		}
	}

	@Override
	public Pair<Map<Integer, Integer>, Map<Integer, Integer>> getChoiceAtoms() {
		return choiceRecorder.getAndResetChoices();
	}

	@Override
	public Map<Integer, Set<Integer>> getHeadsToBodies() {
		return choiceRecorder.getAndResetHeadsToBodies();
	}

	@Override
	public void updateAssignment(IntIterator it) {
		while (it.hasNext()) {
			workingMemory.addInstance(atomStore.get(it.next()), true);
		}
	}

	@Override
	public void forgetAssignment(int[] atomIds) {
		throw new UnsupportedOperationException("Forgetting assignments is not implemented");
	}

	@Override
	public CompiledRule getNonGroundRule(Integer ruleId) {
		return knownNonGroundRules.get(ruleId);
	}

	@Override
	public boolean isFact(Atom atom) {
		LinkedHashSet<Instance> instances = factsFromProgram.get(atom.getPredicate());
		if (instances == null) {
			return false;
		}
		return instances.contains(new Instance(atom.getTerms()));
	}

	@Override
	public Set<Literal> justifyAtom(int atomToJustify, Assignment currentAssignment) {
		Set<Literal> literals = analyzeUnjustified.analyze(atomToJustify, currentAssignment);
		// Remove facts from justification before handing it over to the solver.
		for (Iterator<Literal> iterator = literals.iterator(); iterator.hasNext();) {
			Literal literal = iterator.next();
			if (literal.isNegated()) {
				continue;
			}
			LinkedHashSet<Instance> factsOverPredicate = factsFromProgram.get(literal.getPredicate());
			if (factsOverPredicate != null && factsOverPredicate.contains(new Instance(literal.getAtom().getTerms()))) {
				iterator.remove();
			}
		}
		return literals;
	}

	/**
	 * Checks that every nogood not marked as {@link NoGoodInterface.Type#INTERNAL} contains only
	 * atoms which are not {@link PredicateImpl#isSolverInternal()} (except {@link RuleAtom}s, which are allowed).
	 *
	 * @param newNoGoods
	 */
	private void checkTypesOfNoGoods(Collection<NoGood> newNoGoods) {
		for (NoGood noGood : newNoGoods) {
			if (noGood.getType() != NoGoodInterface.Type.INTERNAL) {
				for (int literal : noGood) {
					Atom atom = atomStore.get(atomOf(literal));
					if (atom.getPredicate().isSolverInternal() && !(atom instanceof RuleAtom)) {
						throw oops("NoGood containing atom of internal predicate " + atom + " is " + noGood.getType() + " instead of INTERNAL");
					}
				}
			}
		}
	}

	private static class FirstBindingAtom {
		final CompiledRule rule;
		final Literal startingLiteral;

		FirstBindingAtom(CompiledRule rule, Literal startingLiteral) {
			this.rule = rule;
			this.startingLiteral = startingLiteral;
		}
	}

}
