/* 
 * Kodkod -- Copyright (c) 2005-2011, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.engine.satlab;

import java.util.Iterator;

import kodkod.util.ints.IntSet;


/**
 * <p>A proof of unsatisfiability generated by a {@linkplain SATProver}.
 * Formally, a resolution trace is a sequence of inferences made by a  
 * prover that ends in a conflict (empty clause).  An element in a resolution
 * trace is called a clause.  There are two kinds of clauses in the trace: 
 * axioms and resolvents.  Axioms are the clauses given to the 
 * prover via the {@linkplain SATSolver#addClause(int[])} method, and resolvents are  
 * the clauses derived by the prover from axioms or previously learned resolvents through 
 * <a href="http://en.wikipedia.org/wiki/Resolution_%28logic%29">resolution</a>.</p>
 * 
 * <p>Clauses in a resolution trace are ordered as follows.  The first |<i>A</i>| elements
 * in the trace correspond to the axioms given to the prover (i.e. prover.clauses).  
 * An axiom <i>a1</i> precedes an axiom <i>a2</i> in the trace if and only if 
 * <i>a1</i> was added to the prover before <i>a2</i>.  (An axiom is "added" to the 
 * prover, and appears in the trace, if and only if the corresponding call to {@linkplain SATSolver#addClause(int[])})
 * returned <tt>true</tt>.)  The remaining elements in the trace
 * are the resolvents.  A resolvent <i>r</i> succeeds all of the resolvents needed for its derivation
 * (i.e. all resolvents reachable from r via the {@linkplain Clause#antecedents()} relation).  
 * The last element in the trace is the conflict resolvent.  The axioms that are reachable from the conflict
 * form the <i>unsatisfiable core</i> of the trace. <p>
 *  
 * @specfield prover: SATProver
 * @specfield elts: Clause[]
 * @specfield conflict: elts[#elts-1]
 * @invariant #elts = #(prover.clauses + prover.resolvents)
 * @invariant elts[[0..#prover.clauses)].literals = prover.clauses
 * @invariant elts[[#prover.clauses..#elts)].literals = prover.resolvents
 * @invariant all i: [0..#prover.clauses) | no elts[i].antecedents 
 * @invariant all i: [#prover.clauses..#elts) | all ante: elts[i].antecedents[int] | elts.ante < i
 * @invariant no conflict.literals
 * 
 * @author Emina Torlak
 */
public interface ResolutionTrace extends Iterable<Clause> {

	/**
	 * Returns the length of this trace.
	 * @return #this.elts
	 */
	public int size();
		
	/**
	 * Returns an iterator over the elements in this trace  in proper sequence.
	 * <p><b>Note:</b>The clause objects returned by the iterator are not 
	 * required to be immutable. In particular, the state of a clause object 
	 * returned by <tt>next()</tt> (as well as the state of any object obtained
	 * through that clause's {@linkplain Clause#antecedents()} method) is guaranteed 
	 * to remain the same only until the subsequent call to the <tt>next()</tt> method 
	 * of the iterator instance.</p>
	 * @return an iterator over the elements in this trace in proper sequence.
	 */
	public abstract Iterator<Clause> iterator();
	
	/**
	 * Returns an iterator over the elements at the given indices in this trace, in proper sequence.
	 * <p><b>Note:</b>The clause objects returned by the iterator are not 
	 * required to be immutable. In particular, the state of a clause object 
	 * returned by <tt>next()</tt> (as well as the state of any object obtained
	 * through that clause's {@linkplain Clause#antecedents()} method) is guaranteed 
	 * to remain the same only until the subsequent call to the <tt>next()</tt> method 
	 * of the iterator instance.</p>
	 * @requires indices.min() >= 0 && indices.max() < this.size()
	 * @return an iterator over the elements at the given indices in this trace, in proper sequence.
	 * @throws IndexOutOfBoundsException  indices.min() < 0 || indices.max() >= this.size()
	 */
	public abstract Iterator<Clause> iterator(IntSet indices);
	
	/**
	 * Returns an iterator over the elements at the given indices in this trace, in the 
	 * reverse order of indices.
	 * <p><b>Note:</b>The clause objects returned by the iterator are not 
	 * required to be immutable. In particular, the state of a clause object 
	 * returned by <tt>next()</tt> (as well as the state of any object obtained
	 * through that clause's {@linkplain Clause#antecedents()} method) is guaranteed 
	 * to remain the same only until the subsequent call to the <tt>next()</tt> method 
	 * of the iterator instance.</p>
	 * @requires indices.min() >= 0 && indices.max() < this.size()
	 * @return an iterator over the elements at the given indices in this trace, in the 
	 * reverse order of indices.
	 * @throws IndexOutOfBoundsException  indices.min() < 0 || indices.max() >= this.size()
	 */
	public abstract Iterator<Clause> reverseIterator(IntSet indices);
	
	/**
	 * Returns the indices of the axioms that form the unsatisfiable core of this trace.
	 * @return { i: int | no this.elts[i].antecedents and this.elts[i] in this.conflict.^antecedents }
	 */
	public abstract IntSet core();
		
	/**
	 * Returns the indices of the axioms in this trace.
	 * @return { i: int | this.elts[i] in this.prover.clauses }
	 */
	public abstract IntSet axioms(); 
	
	/**
	 * Returns the indices of the resolvents in this trace.
	 * @return { i: int | this.elts[i] in this.prover.resolvents }
	 */
	public abstract IntSet resolvents();
	
	/**
	 * Returns  the indices of all clauses reachable from the clauses at the given indices 
	 * by following the antecedent relation zero or more times.
	 * @requires indices.min() >= 0 && indices.max() < this.size()
	 * @return { i: int | this.elts[i] in this.elts[indices].*antecedents }
	 * @throws IllegalArgumentException  indices.min() < 0 || indices.max() >= this.size()
	 */
	public abstract IntSet reachable(IntSet indices);
	
	/**
	 * Returns the indices of all clauses reachable from the clauses at the given indices 
	 * by following the transpose of the antecedent relation zero or more times.
	 * @requires indices.min() >= 0 && indices.max() < this.size()
	 * @return { i: int | this.elts[i] in this.elts[indices].*~antecedents }
	 * @throws IllegalArgumentException  indices.min() < 0 || indices.max() >= this.size()
	 */
	public abstract IntSet backwardReachable(IntSet indices);
	
	/**
	 * Returns the indices of all clauses in this trace that can be learned solely from the
	 * clauses with the given indices.
	 * @requires indices.min() >= 0 && indices.max() < this.size()
	 * @return { i: int | this.elts[i].*antecedents = this.elts[indices].*antecedents + this.elts[i].*antecedents & this.elts[indices].*~antecedents }
	 * @throws IllegalArgumentException  indices.min() < 0 || indices.max() >= this.size()
	 */
	public abstract IntSet learnable(IntSet indices);
	
	/**
	 * Returns the indices of all clauses in this trace that can be learned solely and directly from the
	 * clauses with the given indices.
	 * @requires indices.min() >= 0 && indices.max() < this.size()
	 * @return { i: int | this.elts[i].antecedents in this.elts[indices] }
	 * @throws IllegalArgumentException  indices.min() < 0 || indices.max() >= this.size()
	 */
	public abstract IntSet directlyLearnable(IntSet indices);
	
	
	/**
	 * Returns the clause at the given index.  Note that this method is not required 
	 * to always return the same Clause object; it is only required to return Clause
	 * objects that are equal according to their <tt>equals</tt> methods.  The Clause
	 * objects returned by this method are guaranteed to be immutable.
	 * @requires 0 <= index < this.size()
	 * @return this.elts[index]
	 * @throws IndexOutOfBoundsException  0 < index || index >= this.size()
	 */
	public abstract Clause get(int index);
	
}
