package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <a href="mailto:mandarax@jbdietrich.com">Jens Dietrich</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library 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
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
import org.mandarax.kernel.LoopCheckingAlgorithm;
import org.mandarax.util.logging.LogCategories;

/**
 * Simple implementation of a loop checking algorithm that can be customized
 * by setting some parameters. Suitable if one can estimate the recurrence patterns
 * causing an infinite loop. (number of recurrences indicating that we are in a loop, max
 * number of recuring patterns).
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.3
 */
public class DefaultLoopCheckingAlgorithm
		implements LoopCheckingAlgorithm, LogCategories {

	// number of proof steps without checks
	private int numberOfStepsWithoutCheck = 10;

	// we check for sequences of clauses that are repeated. this is the max length of such patterns checked
	private int maxPatternLength = 5;

	// the min number of recurrences of a pattern needed to regard this sequence as an infinite loop 
	private int minRecurrenceNumber = 5;

	/**
	 * Constructor.
	 */
	public DefaultLoopCheckingAlgorithm() {
		super ();
	}
	
	/**
	 * Constructor.
	 * @param par1 we check for sequences of clauses that are repeated. this is the max length of such patterns checked
	 * @param par2 the min number of recurrences of a pattern needed to regard this sequence as an infinite loop
	 * @param par3 number of proof steps without checks
	 */
	public DefaultLoopCheckingAlgorithm(int par1, int par2, int par3) {
		super ();
		maxPatternLength          = par1;
		minRecurrenceNumber       = par2;
		numberOfStepsWithoutCheck = par3;
	}
	/**
	 * Check the sequences.
	 * @return boolean
	 * @param startSeq1 start index of the first sequence
	 * @param startSeq2 start index of the second sequence
	 * @param length the length of the sequences
	 * @param list the list
	 * @param index the number of the comparsion
	 */
	private boolean check(int startSeq1, int startSeq2, int length,
						  java.util.List list, int index) {
		if(index == 0) {
			return true;
		}

		boolean result = compareSequences (startSeq1, startSeq2, length,
										   list);

		if(result && (startSeq1 >= length)) {
			return check (startSeq1 - length, startSeq2 - length, length,
						  list, index - 1);
		} else {
			return false;
		}
	}
	/**
	 * Compare two sequences of elements in a list.
	 * @return boolean if the sequences are equal
	 * @param startSeq1 the start index of the first index
	 * @param startSeq2 the start index of the second sequence
	 * @param length the length of the sequences
	 * @param list the list of objects
	 */
	private boolean compareSequences(int startSeq1, int startSeq2,
									 int length, java.util.List list) {
		for(int i = 0; i < length; i++) {
			if(list.get (startSeq1 + i) != list.get (startSeq2 + i)) {
				return false;
			}
		}

		return true;
	}
	/**
	 * Insert the method's description here.
	 * Creation date: (2/14/2001 8:36:28 AM)
	 * @return boolean
	 * @param startSeq1 int
	 * @param startSeq2 int
	 * @param length int
	 * @param list java.util.List
	 * @param comp int
	 */
	private boolean compareSequences(int startSeq1, int startSeq2,
									 int length, java.util.List list,
									 int comp) {
		return false;
	}
	/**
	 * Get the max pattern length.
	 * @return a value
	 */
	public int getMaxPatternLength() {
		return maxPatternLength;
	}
	/**
	 * Get the min recurrence number.
	 * @return a value
	 */
	public int getMinRecurrenceNumber() {
		return minRecurrenceNumber;
	}
	/**
	 * Get the number of steps without checks.
	 * @return a value
	 */
	public int getNumberOfStepsWithoutCheck() {
		return numberOfStepsWithoutCheck;
	}
	/**
	 * Indicates whether the list of applied clauses represents an infinite loop.
	 * No loop checking means return false.
	 * @return false
	 * @param appliedClauses a list
	 */
	public boolean isInfiniteLoop(java.util.List appliedClauses) {
		int s = appliedClauses.size ();

		if((s == 0) || (s % numberOfStepsWithoutCheck > 0)) {
			return false;
		}

		boolean logOn = LOG_IE_LOOPCHECK.isDebugEnabled ();

		// start check
		for(int i = 1; i < maxPatternLength + 1; i++) {
			if(i * minRecurrenceNumber > s) {
				if(logOn) {
					LOG_IE_LOOPCHECK.debug ("No loop detected in :"
											+ appliedClauses);
				}

				return false;
			}

			if(check (s - (2 * i), s - i, i, appliedClauses,
					  minRecurrenceNumber)) {
				if(logOn) {
					LOG_IE_LOOPCHECK.debug ("Loop detected in :"
											+ appliedClauses);
					LOG_IE_LOOPCHECK.debug (
						"The length of the recuring pattern is: " + i);
					LOG_IE_LOOPCHECK.debug ("The pattern recures "
											+ minRecurrenceNumber + " times");
				}

				return true;
			}
		}

		if(logOn) {
			LOG_IE_LOOPCHECK.debug ("No loop detected in :" + appliedClauses);
		}

		return false;
	}
	/**
	 * Set the max pattern length.
	 * @param value the new value
	 */
	public void setMaxPatternLength(int value) {
		maxPatternLength = value;
	}
	/**
	 * Set the min recurrence number.
	 * @param value the new value
	 */
	public void setMinRecurrenceNumber(int value) {
		minRecurrenceNumber = value;
	}
	/**
	 * Set the number of steps without checks.
	 * @param value the new value
	 */
	public void setNumberOfStepsWithoutChecks(int value) {
		numberOfStepsWithoutCheck = value;
	}
}
