/*
 * DlpTransformer.java
 *
 * Copyright (C) 2006 - 2007 Martin Slota
 *
 * This program is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License as published by the Free Software
 * Foundation; either version 2 of the License, or (at your option) any later
 * version.
 *
 * This program is distributed in the hope that it will be useful, but WITHOUT
 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
 * details.
 *
 * You should have received a copy of the GNU General Public License along with
 * this program; if not, write to the Free Software Foundation, Inc., 51
 * Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
 */

/*
 * History:
 * v0.1 (2007-02-10): initial version
 * v0.2 (2007-02-11):
 * - implementation and tests
 * v0.2.1 (2007-02-12):
 * - changes because LogicProgram converted to an interface, implementation is
 *   now in DefaultLogicProgram
 * v0.2.2 (2007-02-14):
 * - transform() returns TransformedDlp instead of LogicProgram
 * v0.2.3 (2007-02-15):
 * - some bugs fixed
 * v0.9.0 (2007-05-06):
 * - public methods documented
 * 
 * TODO docs + refactoring
 */

package lp.trans;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import lp.struct.LpAtom;
import lp.struct.LpConstant;
import lp.struct.LpLiteral;
import lp.struct.LpPredicate;
import lp.struct.LpRule;
import lp.struct.LpTerm;
import lp.struct.util.LpEncoder;
import lp.struct.util.LpBuffer;
import lp.unit.DynamicLogicProgram;
import lp.unit.LogicProgram;
import lp.unit.TransformedDlp;

import static lp.unit.TransDlpRuleType.*;

/**
 * Transforms a dynamic logic program into an equivalent normal logic program.
 *
 * @author Martin Slota
 * @version 0.9.0
 */
public class DlpTransformer {
	private final Map<LpAtom, AtomInfo> atomData;
	private final LpBuffer encoder;
	private int progCount;
	
	/**
	 * Creates a new instance of {@code DlpTransformer}.
	 */
	public DlpTransformer() {
		atomData = new HashMap<LpAtom, AtomInfo>();
		encoder = LpEncoder.getBuffer();
	}
	
	private AtomInfo getData(LpAtom atom) {
		AtomInfo result = atomData.get(atom);
		if (result == null) {
			result = new AtomInfo(atom);
			atomData.put(atom, result);
		}
		return result;
	}
	
	/**
	 * Constructs the transformational equivalent of {@code dlp}.
	 *
	 * @param dlp the dynamic logic program that should be transformed
	 * @return the normal logic program equivalent to {@code dlp}
	 * @throws IllegalArgumentException if {@code dlp.isGround()} returns 
	 * {@code false}
	 */
	public TransformedDlp transform(DynamicLogicProgram dlp) {
		if (!dlp.isGround()) {
			throw new IllegalArgumentException(
					"DlpTransformer only accepts grounded dynamic logic programs!");
		}
		progCount = dlp.size();
		TransformedDlp result = new TransformedDlp();
		for (int i = 0; i < dlp.size(); i++) {
			LogicProgram prog = dlp.get(i);
			int level = i+1;
			for (LpRule r : prog) {
				result.add(makeTransformedRule(r, level), REWRITTEN_RULE);
				LpLiteral head = r.getHead();
				if (head != null) {
					AtomInfo data = getData(head.getAtom());
					data.addOccurence(head.isPositive(), level);
				}
				
				for (LpLiteral l : r.getBody()) {
					if (!l.isPositive()) {
						getData(l.getAtom()).setDefaultNeeded();
					}
				}
			}
		}
		for (int i = 0; i < dlp.size(); i++) {
			LogicProgram prog = dlp.get(i);
			int level = i+1;
			for (LpRule r : prog) {
				LpLiteral head = r.getHead();
				if (head != null) {
					AtomInfo data = getData(head.getAtom());
					int introToLevel = data.getMaxLeqThan(
							!head.isPositive(), level);
					if (introToLevel > -1)
						result.add(makeIntroRejection(r, introToLevel),
								INTRO_REJECTION);
				}
			}
		}
		for (AtomInfo app : atomData.values()) {
			app.addRulesTo(result);
		}
		atomData.clear();
		return result;
	}
	
	private LpRule makeTransformedRule(LpRule origRule, int level) {
		LpLiteral origHead = origRule.getHead();
		LpLiteral head = makeTransformedLiteral(origHead, true);
		Set<LpLiteral> body = new LinkedHashSet<LpLiteral>();
		for (LpLiteral l : origRule.getBody())
			body.add(makeTransformedLiteral(l, true));
		body.add(makeRejectionAtom(origHead, level).getNegativeLiteral());
		return new LpRule(head, body);
	}
	
	private LpRule makeIntroRejection(LpRule origRule, int toLevel) {
		LpLiteral origHead = origRule.getHead();
		LpLiteral head = makeRejectionAtom(
				origHead.getAtom().getLiteral(!origHead.isPositive()),
				toLevel).getPositiveLiteral();
		Set<LpLiteral> body = new LinkedHashSet<LpLiteral>();
		for (LpLiteral l : origRule.getBody())
			body.add(makeTransformedLiteral(l, true));
		return new LpRule(head, body);
	}
	
	private LpLiteral makeTransformedLiteral(LpLiteral origLit, boolean positive) {
		if (origLit == null)
			return null;
		
		LpPredicate origPred = origLit.getPredicate();
		StringBuilder predName = new StringBuilder();
		predName.append(origLit.isPositive() ? "" : "_N");
		predName.append(origLit.getPredicate().getName());
		LpPredicate pred = LpPredicate.getInstance(predName.toString(),
				origPred.getArity());
		
		return LpAtom.getInstance(pred, origLit.getArguments()).getLiteral(positive);
	}
	
	private LpAtom makeRejectionAtom(LpLiteral lit, int level) {
		LpConstant litConst = LpConstant.getInstance(encoder.asString(lit));
		
		LpPredicate rejPred = LpPredicate.getInstance("_rej", 2);
		List<LpTerm> args = new ArrayList<LpTerm>(2);
		args.add(LpConstant.getInstance(Integer.toString(level)));
		args.add(litConst);
		
		return LpAtom.getInstance(rejPred, args);
	}
	
	/**
	 * A container for metadata about an atom's appearance in the input program.
	 * First it needs to be filled with information by calling the methods
	 * {@link #addOccurence(boolean, int)}. Based on this data, it can formulate
	 * all default assumptions, propagation rejections and completeness
	 * constraints for the given atom.
	 *
	 * @author Martin Slota
	 * @version 0.2
	 * @see DlpTransformer
	 */
	private class AtomInfo {
		private final LpAtom forAtom;
		
		
		private boolean defaultNeeded;
		
		private final IntArrayWrapper posOccurences;
		
		private final IntArrayWrapper negOccurences;
		
		public AtomInfo(LpAtom forAtom) {
			this.forAtom = forAtom;
			defaultNeeded = false;
			posOccurences = new IntArrayWrapper(progCount);
			negOccurences = new IntArrayWrapper(progCount);
		}
		
		public void setDefaultNeeded() {
			defaultNeeded = true;
		}
		
		public int getMaxLeqThan(boolean positive, int level) {
			if (positive) {
				return posOccurences.getMaxLeqThan(level);
			} else {
				int result = negOccurences.getMaxLeqThan(level);
				if (result == -1 && defaultNeeded)
					result = 0;
				return result;
			}
		}
		
		public void addOccurence(boolean positive, int level) {
			if (positive) {
				posOccurences.add(level);
			} else {
				negOccurences.add(level);
			}
		}
		
		public void addRulesTo(TransformedDlp prog) {
			boolean makeConstraint = false;
			for (int level = 1; level <= progCount; level++) {
				if (posOccurences.contains(level) &&
						negOccurences.contains(level))
					makeConstraint = true;
			}
			
			boolean makeDefault = defaultNeeded || makeConstraint;
			
			if (makeDefault)
				prog.add(makeDefault(), DEFAULT_RULE);
			
			if (makeConstraint)
				prog.add(makeConstraint(), CONSTRAINT);
			
			
			int maxNeg = negOccurences.getMax();
			if (!posOccurences.isEmpty()) {
				int toLevel = posOccurences.get(0);
				int fromLevel;
				int i = 1;
				while (i < posOccurences.length()) {
					fromLevel = posOccurences.get(i);
					if (fromLevel <= maxNeg) {
						prog.add(
								makePropagationRejection(true, fromLevel, toLevel),
								PROPAGATION_REJECTION);
						toLevel = fromLevel;
						i++;
					} else {
						break;
					}
				}
			}
			
			int maxPos = posOccurences.getMax();
			if (!negOccurences.isEmpty()) {
				int i, toLevel, fromLevel;
				if (makeDefault) {
					toLevel = 0;
					i = 0;
				} else {
					toLevel = negOccurences.get(0);
					i = 1;
				}
				while (i < negOccurences.length()) {
					fromLevel = negOccurences.get(i);
					if (fromLevel <= maxPos) {
						prog.add(
								makePropagationRejection(false, fromLevel, toLevel),
								PROPAGATION_REJECTION);
						toLevel = fromLevel;
						i++;
					} else {
						break;
					}
				}
			}
		}
		
		private LpRule makePropagationRejection(boolean positive, int fromLevel, int toLevel) {
			LpLiteral origHead = forAtom.getLiteral(positive);
			LpLiteral head = makeRejectionAtom(origHead, toLevel).getPositiveLiteral();
			Set<LpLiteral> body = Collections.singleton(
					makeRejectionAtom(origHead, fromLevel).getPositiveLiteral());
			return new LpRule(head, body);
		}
		
		private LpRule makeDefault() {
			LpLiteral origLit = forAtom.getNegativeLiteral();
			LpLiteral head = makeTransformedLiteral(origLit, true);
			Set<LpLiteral> body = Collections.singleton(
					makeRejectionAtom(origLit, 0).getNegativeLiteral());
			return new LpRule(head, body);
		}
		
		private LpRule makeConstraint() {
			Set<LpLiteral> body = new LinkedHashSet<LpLiteral>(2);
			body.add(makeTransformedLiteral(forAtom.getPositiveLiteral(), false));
			body.add(makeTransformedLiteral(forAtom.getNegativeLiteral(), false));
			return new LpRule(null, body);
		}
	}
}