package aima.core.logic.propositional.inference;

import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

import aima.core.logic.propositional.kb.KnowledgeBase;
import aima.core.logic.propositional.kb.data.Clause;
import aima.core.logic.propositional.parsing.ast.PropositionSymbol;
import aima.core.logic.propositional.transformations.ConvertToConjunctionOfClauses;
import aima.core.logic.propositional.transformations.SymbolCollector;

/**
 * Artificial Intelligence A Modern Approach (3rd Edition): page 258.<br>
 * <br>
 * 
 * <pre>
 * <code>
 * function PL-FC-ENTAILS?(KB, q) returns true or false
 *   inputs: KB, the knowledge base, a set of propositional definite clauses
 *           q, the query, a proposition symbol
 *   count &larr; a table, where count[c] is the number of symbols in c's premise
 *   inferred &larr; a table, where inferred[s] is initially false for all symbols
 *   agenda &larr; a queue of symbols, initially symbols known to be true in KB
 *   
 *   while agenda is not empty do
 *     p &larr; Pop(agenda)
 *     if p = q then return true
 *     if inferred[p] = false then
 *        inferred[p] &larr; true
 *        for each clause c in KB where p is in c.PREMISE do
 *            decrement count[c]
 *            if count[c] = 0 then add c.CONCLUSION to agenda
 *   return false
 * </code>
 * </pre>
 * 
 * Figure 7.15 the forward-chaining algorithm for propositional logic. The
 * <i>agenda</i> keeps track of symbols known to be true but not yet
 * "processed". The <i>count</i> table keeps track of how many premises of each
 * implication are as yet unknown. Whenever a new symbol p from the agenda is
 * processed, the count is reduced by one for each implication in whose premise
 * p appears (easily identified in constant time with appropriate indexing.) If
 * a count reaches zero, all the premises of the implication are known, so its
 * conclusion can be added to the agenda. Finally, we need to keep track of
 * which symbols have been processed; a symbol that is already in the set of
 * inferred symbols need not be added to the agenda again. This avoids redundant
 * work and prevents loops caused by implications such as P &rArr; Q and Q
 * &rArr; P.
 * 
 * @author Ciaran O'Reilly
 * @author Ravi Mohan
 * @author Mike Stampone
 */
public class PLFCEntails {

	/**
	 * PL-FC-ENTAILS?(KB, q)<br>
	 * The forward-chaining algorithm for propositional logic.
	 * 
	 * @param kb
	 *            the knowledge base, a set of propositional definite clauses.
	 * @param q
	 *            q, the query, a proposition symbol
	 * @return true if KB |= q, false otherwise.
	 * @throws IllegalArgumentException
	 *             if KB contains any non-definite clauses.
	 */
	public boolean isEntailed(KnowledgeBase kb, PropositionSymbol q) {
		// count <- a table, where count[c] is the number of symbols in c's
		// premise
		Map<Clause, Integer> count = initializeCount(kb);
		// inferred <- a table, where inferred[s] is initially false for all
		// symbols
		Map<PropositionSymbol, Boolean> inferred = initializeInferred(kb);
		// agenda <- a queue of symbols, initially symbols known to be true in
		// KB
		Queue<PropositionSymbol> agenda = initializeAgenda(count);
		// Note: an index for p to the clauses where p appears in the premise
		Map<PropositionSymbol, Set<Clause>> pToClausesWithPInPremise = initializeIndex(
				count, inferred);

		// while agenda is not empty do
		while (!agenda.isEmpty()) {
			// p <- Pop(agenda)
			PropositionSymbol p = agenda.remove();
			// if p = q then return true
			if (p.equals(q)) {
				return true;
			}
			// if inferred[p] = false then
			if (inferred.get(p).equals(Boolean.FALSE)) {
				// inferred[p] <- true
				inferred.put(p, true);
				// for each clause c in KB where p is in c.PREMISE do
				for (Clause c : pToClausesWithPInPremise.get(p)) {
					// decrement count[c]
					decrement(count, c);
					// if count[c] = 0 then add c.CONCLUSION to agenda
					if (count.get(c) == 0) {
						agenda.add(conclusion(c));
					}
				}
			}
		}

		// return false
		return false;
	}

	//
	// SUPPORTING CODE
	//

	//
	// PROTECTED
	//
	protected Map<Clause, Integer> initializeCount(KnowledgeBase kb) {
		// count <- a table, where count[c] is the number of symbols in c's
		// premise
		Map<Clause, Integer> count = new HashMap<Clause, Integer>();

		Set<Clause> clauses = ConvertToConjunctionOfClauses.apply(
				kb.asSentence()).getClauses();
		for (Clause c : clauses) {
			if (!c.isDefiniteClause()) {
				throw new IllegalArgumentException(
						"Knowledge Base contains non-definite clauses:" + c);
			}
			// Note: # of negative literals is equivalent to the number of
			// symbols in c's premise
			count.put(c, c.getNumberNegativeLiterals());
		}

		return count;
	}

	protected Map<PropositionSymbol, Boolean> initializeInferred(KnowledgeBase kb) {
		// inferred <- a table, where inferred[s] is initially false for all
		// symbols
		Map<PropositionSymbol, Boolean> inferred = new HashMap<PropositionSymbol, Boolean>();
		for (PropositionSymbol p : SymbolCollector.getSymbolsFrom(kb
				.asSentence())) {
			inferred.put(p, false);
		}
		return inferred;
	}

	// Note: at the point of calling this routine, count will contain all the
	// clauses in KB.
	protected Queue<PropositionSymbol> initializeAgenda(Map<Clause, Integer> count) {
		// agenda <- a queue of symbols, initially symbols known to be true in
		// KB
		Queue<PropositionSymbol> agenda = new LinkedList<PropositionSymbol>();
		for (Clause c : count.keySet()) {
			// No premise just a conclusion, then we know its true
			if (c.getNumberNegativeLiterals() == 0) {
				agenda.add(conclusion(c));
			}
		}
		return agenda;
	}

	// Note: at the point of calling this routine, count will contain all the
	// clauses in KB while inferred will contain all the proposition symbols.
	protected Map<PropositionSymbol, Set<Clause>> initializeIndex(
			Map<Clause, Integer> count, Map<PropositionSymbol, Boolean> inferred) {
		Map<PropositionSymbol, Set<Clause>> pToClausesWithPInPremise = new HashMap<PropositionSymbol, Set<Clause>>();
		for (PropositionSymbol p : inferred.keySet()) {
			Set<Clause> clausesWithPInPremise = new HashSet<Clause>();
			for (Clause c : count.keySet()) {
				// Note: The negative symbols comprise the premise
				if (c.getNegativeSymbols().contains(p)) {
					clausesWithPInPremise.add(c);
				}
			}
			pToClausesWithPInPremise.put(p, clausesWithPInPremise);
		}
		return pToClausesWithPInPremise;
	}

	protected void decrement(Map<Clause, Integer> count, Clause c) {
		int currentCount = count.get(c);
		// Note: a definite clause can just be a fact (i.e. 1 positive literal)
		// However, we only decrement those where the symbol is in the premise
		// so we don't need to worry about going < 0.
		count.put(c, currentCount - 1);
	}

	protected PropositionSymbol conclusion(Clause c) {
		// Note: the conclusion is from the single positive
		// literal in the definite clause (which we are
		// restricted to).
		return c.getPositiveSymbols().iterator().next();
	}
}