content: /* 
   * Kodkod -- Copyright (c) 2005-present, 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.ucore;
  
  import java.util.Arrays;
  import java.util.Iterator;
  
  import kodkod.engine.fol2sat.TranslationLog;
  import kodkod.engine.fol2sat.Translator;
  import kodkod.engine.satlab.Clause;
  import kodkod.engine.satlab.ReductionStrategy;
  import kodkod.engine.satlab.ResolutionTrace;
  import kodkod.util.ints.IntBitSet;
  import kodkod.util.ints.IntIterator;
  import kodkod.util.ints.IntSet;
  import kodkod.util.ints.Ints;
  import kodkod.util.ints.SparseSequence;
  import kodkod.util.ints.TreeSequence;
  
  /**
   * Dynamic Recycling Core Extraction is a strategy for generating unsat cores that are minimal at the logic level.  
   * Specifically, let C be a core that is minimal according to this strategy, 
   * and let F(C) be the top-level logic constraints
   * corresponding to C.  Then, this strategy guarantees that there is no clause
   * c in C such that F(C - c) is a strict subset of F(C). Furthermore, it also
   * guarantees that for all f in F(C), F(C) - f is satisfiable.  This is a stronger
   * guarantee than that of {@linkplain HybridStrategy}.  In general, using this strategy
   * is more expensive, timewise, than using {@linkplain HybridStrategy}.
   * 
   * <p>Like Adaptive RCE, DRCE is parameterized with 3 values that control the amount of recycling.  The
   * first is the <tt>noRecycleRatio</tt>, which completely disables recycling if it is greater than
   * the ratio of the size of the core passed to {@linkplain #next(ResolutionTrace)} and the number of axioms in the 
   * trace.  The default value is .03; if the core makes up only 3 percent of the axioms, no recycling 
   * will happen.  The remaining two parameters are the <tt>recycleLimit</tt> and the <tt>hardnessCutOff</tt>.
   * If the hardness of the proof passed to {@linkplain #next(ResolutionTrace)} is greater than <tt>hardnessCutOff</tt>,
   * then the number of relevant axioms, |A_r|, plus the number of recycled resolvents is no greater than 
   * |A_r|*<tt>recycleLimit</tt>.  Otherwise, all valid
   * resolvents are recycled (i.e. added to the relevant axioms).  
   * Proof hardness is the ratio of the trace size to the number of axioms in the trace.
   * Default value for <tt>hardnessCutOff</tt> is 2.0, and  default value for <tt>recycleLimit</tt> is 1.2. 
   * 
   * <p>Unlike ARCE, DRCE uses proof information to determine the order in which the constraints are tested for 
   * membership in a minimal core.  ARCE, RCE, SCE and NCE all use the same (arbitrary but deterministic) ordering.</p>
   * 
   * <p>This implementation of DRCE will work properly only on CNFs generated by the kodkod {@linkplain Translator}. </p>
   * 
   * @specfield noRecycleRatio: double
   * @specfield hardnessCutOff: double
   * @specfield recycleLimit: double
   * @invariant noRecycleRatio in [0..1]
   * @invariant recycleLimit >= 1
   * @invariant hardnessCutOff >= 1
   * @author Emina Torlak
   * @see HybridStrategy
   */
  public final class DynamicRCEStrategy implements ReductionStrategy {
  	private final double noRecycleRatio, recycleLimit, hardnessCutOff;
  	private static final boolean DBG = true;
  	private final SparseSequence<IntSet> hits;
  	/**
  	 * Constructs an ARCE strategy that will use the given translation
  	 * log to relate the cnf clauses back to the logic constraints from 
  	 * which they were generated. 
  	 * @ensures this.hardnessCutOff' = 2 and this.recycleLimit' = 1.2 and this.noRecycleRatio' = .03
  	 */
  	public DynamicRCEStrategy(final TranslationLog log) {
  		this(log, .03, 2.0, 1.2);
  	}
  	
  	/**
  	 * Constructs an ARCE strategy that will use the given translation
  	 * log to relate the cnf clauses back to the logic constraints from 
  	 * which they were generated. 
  	 * @ensures this.hardnessCutOff' = hardnessCutOff and this.recycleLimit' = recycleLimit and 
  	 * this.noRecycleRatio' = noRecycleRatio
  	 */
  	public DynamicRCEStrategy(final TranslationLog log, double noRecycleRatio, double hardnessCutOff, double recycleLimit) {
  		if (noRecycleRatio<0 || noRecycleRatio>1) 
  			throw new IllegalArgumentException("noRecycleRatio must be in [0..1]: " + noRecycleRatio);
  		if (hardnessCutOff < 1)
  			throw new IllegalArgumentException("hardnessCutOff must be >=1: " + hardnessCutOff);
  		if (recycleLimit < 1)
  			throw new IllegalArgumentException("recycleLimit must be >=1: " + recycleLimit);
  		this.noRecycleRatio = noRecycleRatio;
  		this.hardnessCutOff = hardnessCutOff;
  		this.recycleLimit = recycleLimit;
  		this.hits = new TreeSequence<IntSet>();
  		for(IntIterator itr = StrategyUtils.rootVars(log).iterator(); itr.hasNext(); ) { 
  			hits.put(itr.next(), null);
  		}
  	}
  
  	/**
  	 * {@inheritDoc}
  	 * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
  	 */
  	public IntSet next(ResolutionTrace trace) {
  		if (hits.isEmpty()) return Ints.EMPTY_SET; // tried everything
  		final IntSet relevantVars = StrategyUtils.coreTailUnits(trace);
  		
  		final long[] byRelevance = sortByRelevance(trace, relevantVars);
  		if (DBG) printRelevant(byRelevance);
   		for(int i = byRelevance.length-1; i>=0; i--) {
  			final int var = (int)byRelevance[i];
  			if (hits.remove(var)!=null) {
  				// remove maxVar from the set of relevant variables
  				relevantVars.remove(var);
  				if (relevantVars.isEmpty()) break; // there was only one root formula left
  				// get all axioms and resolvents corresponding to the clauses that
  				// form the translations of formulas identified by relevant vars
  				final IntSet relevantClauses = clausesFor(trace, relevantVars); 
  				assert !relevantClauses.isEmpty() && !relevantClauses.contains(trace.size()-1);
  				
  				if (DBG) System.out.println("relevant clauses: " + relevantClauses.size() + ", removed " + var);
  				
  				return relevantClauses;
  			}
  		}
  		
  		hits.clear();		
  		return Ints.EMPTY_SET;
  	}
  	
  	private final void printRelevant(long[] byRelevance) { 
  		System.out.print("\nsorted by relevance: ");
  		for(long r : byRelevance) { 
  			System.out.print((int)(r>>>32) + ":" + (int)r + " ");
  		}
  		System.out.println();
  	}
  	
  	/**
  	 * Returns an array R of longs such that for each i, j in [0..R.length) i < j implies
  	 * that the formula identified by (int)R[i] in this.hits contributes fewer clauses to 
  	 * the core of the given trace than the formula identified by (int)R[j].
  	 * @return an array as described above
  	 */
  	private long[] sortByRelevance(ResolutionTrace trace, IntSet relevantVars) { 
  		hits.indices().retainAll(relevantVars);
  		
  		if (hits.get(hits.indices().min())==null) { // first call, initialize the hits 
  			for(IntIterator varItr = relevantVars.iterator(); varItr.hasNext(); ) { 
  				final int var = varItr.next();
  				final IntSet varReachable = new IntBitSet(var+1);
  				varReachable.add(var);
  				hits.put(var, varReachable);
  			}
  			for(Iterator<Clause> clauseItr = trace.reverseIterator(trace.axioms()); clauseItr.hasNext();) {
  				final Clause clause = clauseItr.next();
  				final int maxVar = clause.maxVariable();
  				for(IntSet reachableVars : hits.values()) {
  					if (reachableVars.contains(maxVar)) {
  						for(IntIterator lits = clause.literals(); lits.hasNext(); ) {
  							reachableVars.add(StrictMath.abs(lits.next()));
  						}
  					} 
  				}
  			}
  		}
  		
  		final long[] counts = new long[hits.size()];
  		
  		for(Iterator<Clause> clauseItr = trace.iterator(trace.core()); clauseItr.hasNext(); ) { 
  			final Clause clause = clauseItr.next();
  			final int maxVar = clause.maxVariable();
  			int i = 0;
  			for(IntSet reachableVars : hits.values()) { 
  				if (reachableVars.contains(maxVar)) { 
  					counts[i]++;
  				}
  				i++;
  			}
  		}
  
  		
  		int  i = 0;	
  		for(IntIterator varItr = hits.indices().iterator(); varItr.hasNext();) { 
  			final int var = varItr.next();
  			counts[i] = (counts[i]<<32) | var;
  			i++;
  		}
  		
  		Arrays.sort(counts);
  	
  		return counts;
  	}
  
  	/**
  	 * Returns the indices of all axioms and resolvents
  	 * in the given trace that form the translations of the formulas
  	 * identified by the given variables.  This method assumes that
  	 * the axioms in the given trace were generated by the Kodkod
  	 * {@linkplain Translator}.
  	 * @return 
  	 * let C = { c: trace.prover.clauses | c.maxVariable() in relevantVars },
  	 *     T = { c1, c2: C | c2.maxVariable() in abs(c1.literals) },
  	 *     A = C.*T | 
  	 *     trace.backwardReachable(A) - trace.backwardReachable(trace.axioms() - A)
  	 */
  	private IntSet clausesFor(ResolutionTrace trace, IntSet relevantVars) { 
  		final double hardness = (double) trace.size() / (double) trace.axioms().size();
  		final double coreRatio = ((double) trace.core().size() / (double) trace.axioms().size());
  		
  		if (DBG) System.out.println("trace size: " + trace.size() + ", axioms: " + trace.axioms().size() + ", core: " + trace.core().size() + ", resolvents: " + trace.resolvents().size());
  		if (DBG) System.out.println("hardness: " + hardness + ", coreRatio: " + coreRatio);
  		
  		final IntSet relevantAxioms = StrategyUtils.clausesFor(trace, relevantVars);
  		if (DBG) System.out.println("relevant axioms:  " + relevantAxioms.size());
  		
  		if (coreRatio < noRecycleRatio) {
  			return relevantAxioms;
  		} else if (hardness < hardnessCutOff) { 
  			return trace.learnable(relevantAxioms);
  		} else {
  			IntSet current = relevantAxioms, last;
  			final int maxRelevant = (int) Math.rint(relevantAxioms.size()*recycleLimit);
  			do {
  				last = current;
  				current = trace.directlyLearnable(current);
  			} while (last.size() < current.size() && current.size() < maxRelevant);
  			
  			if (DBG) System.out.println("last: " + last.size() +", current: " + current.size() + ", maxRelevant: " + maxRelevant);
  			
  			return current.size() < maxRelevant ? current : last;
  		}
  				
  	}
  
  }