content: /**
   * Copyright (c) 2020, the Alpha Team.
   * All rights reserved.
   *
   * 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.grounder.instantiation;
  
  import java.util.LinkedHashSet;
  import java.util.Map;
  
  import at.ac.tuwien.kr.alpha.api.Solver;
  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.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.grounder.IndexedInstanceStorage;
  import at.ac.tuwien.kr.alpha.core.grounder.NaiveGrounder;
  import at.ac.tuwien.kr.alpha.core.grounder.WorkingMemory;
  import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth;
  
  /**
   * Implementation of {@link AbstractLiteralInstantiationStrategy} designed for use in {@link NaiveGrounder}.
   * 
   * The instantiation strategy shares a {@link WorkingMemory}, an {@link AtomStore}, an {@link Assignment}, a {@link Map} of atoms that were
   * facts of the currently grounded program, as well as a list of {@link AbstractAtom}s that should be lazily deleted from the working memory,
   * with
   * the grounder.
   * 
   * The working memory and the facts map are maintained by the grounder and are being read by
   * {@link DefaultLazyGroundingInstantiationStrategy} in order to determine {@link AssignmentStatus}es for atoms. The {@link AtomStore} is
   * maintained by {@link DefaultLazyGroundingInstantiationStrategy} in the sense that atoms created from newly encountered ground instances
   * are added by the instantiation strategy. The {@link Assignment} reflects the {@link Solver}s "current view of the world". It is used by
   * {@link DefaultLazyGroundingInstantiationStrategy} to determine {@link AssignmentStatus}es for atoms.
   * 
   * A specialty of this implementation is that - since deletion of obsolete {@link AbstractAtom}s from {@link NaiveGrounder}s
   * {@link WorkingMemory}
   * happens lazily (i.e. at the end of each run of {@link NaiveGrounder#getNoGoods(Assignment)}) - it maintains a set of "stale" atoms that
   * is shared with the grounder. Specifically, whenever {@link DefaultLazyGroundingInstantiationStrategy#getAssignmentStatusForAtom(Atom)}
   * determines that an {@link AbstractAtom} is {@link AssignmentStatus#UNASSIGNED} or {@link AssignmentStatus#FALSE}, that {@link AbstractAtom} is
   * added to
   * the stale atom set, which in turn is processed by the grounder, which then deletes the respective atoms from the working memory.
   * 
   * Copyright (c) 2020, the Alpha Team.
   */
  public class DefaultLazyGroundingInstantiationStrategy extends AbstractLiteralInstantiationStrategy {
  
  	private WorkingMemory workingMemory;
  	private AtomStore atomStore;
  	private Assignment currentAssignment;
  	private LinkedHashSet<Atom> staleWorkingMemoryEntries;
  	private Map<Predicate, LinkedHashSet<Instance>> facts;
  	private boolean accumulatorEnabled;
  
  	public DefaultLazyGroundingInstantiationStrategy(WorkingMemory workingMemory, AtomStore atomStore,
  			Map<Predicate, LinkedHashSet<Instance>> facts, boolean accumulator) {
  		this.workingMemory = workingMemory;
  		this.atomStore = atomStore;
  		this.facts = facts;
  		this.accumulatorEnabled = accumulator;
  	}
  
  	@Override
  	protected Iterable<Instance> computeCandidateInstances(Atom partiallyGroundAtom) {
  		IndexedInstanceStorage instanceStorage = this.workingMemory.get(partiallyGroundAtom, true);
  		return instanceStorage.getInstancesFromPartiallyGroundAtom(partiallyGroundAtom);
  	}
  
  	//@formatter:off
  	/**
  	 * Computes the {@link AssignmentStatus} for a given {@link AbstractAtom} a.
  	 * 
  	 * The atom a is {@link AssignmentStatus#TRUE} iff
  	 * <ul>
  	 * 	<li>The instantiation strategy's <pre>currentAssignment</pre> is null (i.e. the call originated from {@link NaiveGrounder#bootstrap}).</li>
  	 *  <li>a is contained in the working memory and the accumulator flag is enabled.</li>
  	 * 	<li>a is a fact.</li>
  	 *  <li>a is assigned {@link ThriceTruth#TRUE} or {@link ThriceTruth#MBT} in the current assignment by the {@link Solver}.
  	 * </ul>
  	 * 
  	 * An atom is {@link AssignmentStatus#UNASSIGNED} iff it has no {@link ThriceTruth} assigned to it in the current assignment.
  	 * An atom is {@link AssignmentStatus#FALSE} iff it is assigned {@link ThriceTruth#FALSE} in the current assignment by the {@link Solver}.
  	 * 
  	 * Whenever an {@link AbstractAtom} is found to be UNASSIGNED or FALSE,
  	 * that {@link AbstractAtom} is added to the stale atom set for later deletion from working memory by the grounder.
  	 */
  	//@formatter:on
  	@Override
  	protected AssignmentStatus getAssignmentStatusForAtom(Atom atom) {
  		if (this.currentAssignment == null || this.isFact(atom)) {
  			// currentAssignment == null is a legitimate case, grounder may be in bootstrap
  			// and will call bindNextAtom with null assignment in that case.
  			// Assumption: since the atom came from working memory and we must be in
  			// bootstrap here, we can assume for the atom to be true (or atom is a fact
  			// anyway, in which case it's also true).
  			return AssignmentStatus.TRUE;
  		}
  		if (this.accumulatorEnabled) {
  			if (this.workingMemory.get(atom.getPredicate(), true).containsInstance(Instance.fromAtom(atom))) {
  				// Accumulator is enabled. In this case, if the Atom is in the working memory, it is considered true.
  				return AssignmentStatus.TRUE;
  			}
  		}
  
  		// We're neither in bootstrap nor running in accumulator mode, normal workflow starts from here.
  		AssignmentStatus retVal;
  		// First, make sure that the Atom in question exists in the AtomStore.
  		if (atomStore.contains(atom)) {
  			int atomId = this.atomStore.get(atom);
  			this.currentAssignment.growForMaxAtomId();
  			if (currentAssignment.isAssigned(atomId)) {
  				retVal = currentAssignment.getTruth(atomId).toBoolean() ? AssignmentStatus.TRUE : AssignmentStatus.FALSE;
  			} else {
  				retVal = AssignmentStatus.UNASSIGNED;
  			}
  		} else {
  			retVal = AssignmentStatus.UNASSIGNED;
  		}
  		if (retVal == AssignmentStatus.FALSE || retVal == AssignmentStatus.UNASSIGNED) {
  			this.staleWorkingMemoryEntries.add(atom);
  		}
  		return retVal;
  	}
  
  	private boolean isFact(Atom atom) {
  		if (this.facts.get(atom.getPredicate()) == null) {
  			return false;
  		} else {
  			return this.facts.get(atom.getPredicate()).contains(Instance.fromAtom(atom));
  		}
  	}
  
  	@Override
  	protected AssignmentStatus getAssignmentStatusForNegatedGroundLiteral(Literal negatedGroundLiteral) {
  		return AssignmentStatus.TRUE;
  	}
  
  	/**
  	 * Checks whether a given {@link AssignmentStatus} is "acceptable" in the sense
  	 * that an atom with that assignment status represents a valid ground
  	 * substitution for a non-ground atom. This instantiation strategy accepts
  	 * {@link AssignmentStatus#TRUE} and {@link AssignmentStatus#UNASSIGNED}.
  	 */
  	@Override
  	protected boolean assignmentStatusAccepted(AssignmentStatus assignmentStatus) {
  		switch (assignmentStatus) {
  			case TRUE:
  			case UNASSIGNED:
  				return true;
  			case FALSE:
  				return false;
  			default:
  				throw Util.oops("Unsupported AssignmentStatus: " + assignmentStatus);
  		}
  	}
  
  	public void setCurrentAssignment(Assignment currentAssignment) {
  		this.currentAssignment = currentAssignment;
  	}
  
  	public void setStaleWorkingMemoryEntries(LinkedHashSet<Atom> staleWorkingMemoryEntries) {
  		this.staleWorkingMemoryEntries = staleWorkingMemoryEntries;
  	}
  
  }
  