Examples of kodkod.util.ints.IntSet

kodkod.util.ints.IntSet
An ordered set of integers. @specfield ints: set int @author Emina Torlak

   * @return indices of all clauses in the given trace that are 
   * reachable from the conflict clause through the resolvents in
   * trace[roots..trace.length-1]
   */
  private static IntSet reachable(int[][] trace, int roots) { 
    final IntSet reachable = new IntBitSet(trace.length);
    reachable.add(trace.length-1);
    for(int i = trace.length-1; i >= roots; i--) {
      if (reachable.contains(i)) {
        int[] resolvent = trace[i];
        for(int j = 0; j < resolvent.length; j++) {
          reachable.add(resolvent[j]);
        }
      }
    }
    return reachable;
  }

View Full Code Here

   * reachable between 0, inclusive, and axioms, exclusive.
   * @return a set that contains the elements from the given
   * reachable between 0, inclusive, and axioms, exclusive.
   */
  private static IntSet core(IntSet reachable, int axioms) { 
    final IntSet core = new IntBitSet(axioms);
    for(IntIterator itr = reachable.iterator(0, axioms-1); itr.hasNext(); ) {
      core.add(itr.next());
    }
    return Ints.unmodifiableIntSet(core);
  }

View Full Code Here

   * @see kodkod.engine.satlab.ResolutionTrace#implicants(kodkod.util.ints.IntSet)
   */
  public IntSet reachable(IntSet indices) {
    if (indices.isEmpty()) return Ints.EMPTY_SET;
    else if (valid(indices)) {
      final IntSet ret = new IntBitSet(trace.length);
      ret.addAll(indices);
      for(int i = indices.max(); i >= axioms; i--) {
        if (ret.contains(i)) {
          int[] resolvent = trace[i];
          if (resolved(i)) { 
            for(int j = 1, antes = resolvent[0]; j <= antes; j++) {
              ret.add(resolvent[j]);
            }
          } else {
            for(int j = 0; j < resolvent.length; j++) {
              ret.add(resolvent[j]);
            }
          }
        }
      }
      return ret;

View Full Code Here

   * @see kodkod.engine.satlab.ResolutionTrace#backwardReachable(kodkod.util.ints.IntSet)
   */
  public IntSet backwardReachable(IntSet indices) {
    if (indices.isEmpty()) return Ints.EMPTY_SET;
    else if (valid(indices)) {
      final IntSet ret = new IntBitSet(trace.length);
      ret.addAll(indices);
      for(int i = axioms, length = trace.length; i < length; i++) {
        int[] resolvent = trace[i];
        if (resolved(i)) { 
          for(int j = 1, antes = resolvent[0]; j <= antes; j++) {
            if (ret.contains(resolvent[j])) {
              ret.add(i);
              break;
            }
          }
        } else {
          for(int j = 0; j < resolvent.length; j++) {
            if (ret.contains(resolvent[j])) {
              ret.add(i);
              break;
            }
          }
        }
      }

View Full Code Here

   * @see kodkod.engine.satlab.ResolutionTrace#learnable(kodkod.util.ints.IntSet)
   */
  public IntSet learnable(IntSet indices) {
    if (indices.isEmpty()) return Ints.EMPTY_SET;
    else if (valid(indices)) {
      final IntSet ret = new IntBitSet(trace.length);
      ret.addAll(indices);
      TOP: for(int i = axioms, length = trace.length; i < length; i++) {
        int[] resolvent = trace[i];
        if (resolved(i)) { 
          for(int j = 1, antes = resolvent[0]; j <= antes; j++) {
            if (!ret.contains(resolvent[j])) {
              continue TOP;
            }
          }
        } else {
          for(int j = 0; j < resolvent.length; j++) {
            if (!ret.contains(resolvent[j])) {
              continue TOP;
            }
          }
        }
        ret.add(i);
      }
      return ret;
    }
    else throw new IndexOutOfBoundsException("invalid indices: " + indices);
  }

View Full Code Here

   * @see kodkod.engine.satlab.ResolutionTrace#directlyLearnable(kodkod.util.ints.IntSet)
   */
  public IntSet directlyLearnable(IntSet indices) { 
    if (indices.isEmpty()) return Ints.EMPTY_SET;
    else if (valid(indices)) {
      final IntSet ret = new IntBitSet(trace.length);
      ret.addAll(indices);
      TOP: for(int i = axioms, length = trace.length; i < length; i++) {
        int[] resolvent = trace[i];
        if (resolved(i)) { 
          for(int j = 1, antes = resolvent[0]; j <= antes; j++) {
            if (!indices.contains(resolvent[j])) {
              continue TOP;
            }
          }
        } else {
          for(int j = 0; j < resolvent.length; j++) {
            if (!indices.contains(resolvent[j])) {
              continue TOP;
            }
          }
        }
        ret.add(i);
      }
      return ret;
    }
    
    else throw new IndexOutOfBoundsException("invalid indices: " + indices);

View Full Code Here

   * the representatives of sets from this.symmetries contained in the upper bound of r.
   */
  private List<RelationParts> relParts() {
    final List<RelationParts> relParts = new ArrayList<RelationParts>(bounds.relations().size());
    for(Relation r: bounds.relations()) {    
      IntSet upper = bounds.upperBound(r).indexView();
      if (upper.size()==bounds.lowerBound(r).size()) continue; // skip constant relation
      IntSet reps = Ints.bestSet(usize);
      for(IntIterator tuples = upper.iterator(); tuples.hasNext(); ) {
        for(int tIndex = tuples.next(), i = r.arity(); i > 0; i--, tIndex /= usize) {
          for(IntSet symm : symmetries) {
            if (symm.contains(tIndex%usize)) {
              reps.add(symm.min());
              break;
            }
          }
        }
      }

View Full Code Here

   */
  private final Formula breakAcyclic(RelationPredicate.Acyclic acyclic, boolean aggressive) {
    final IntSet[] colParts = symmetricColumnPartitions(acyclic.relation());
    if (colParts!=null) {
      final Relation relation = acyclic.relation();
      final IntSet upper = bounds.upperBound(relation).indexView();
      final IntSet reduced = Ints.bestSet(usize*usize);
      for(IntIterator tuples = upper.iterator(); tuples.hasNext(); ) {
        int tuple = tuples.next();
        int mirror = (tuple / usize) + (tuple % usize)*usize;
        if (tuple != mirror) {
          if (!upper.contains(mirror)) return null;
          if (!reduced.contains(mirror))
            reduced.add(tuple);  
        }
      }
      
      // remove the partition from the set of symmetric partitions
      removePartition(colParts[0].min());

View Full Code Here

   * 
   * @see #breakMatrixSymmetries(Map,boolean)
   */
  private final Formula breakTotalOrder(RelationPredicate.TotalOrdering total, boolean aggressive) {
    final Relation first = total.first(), last = total.last(), ordered = total.ordered(), relation = total.relation();
    final IntSet domain = bounds.upperBound(ordered).indexView();    
  
    if (symmetricColumnPartitions(ordered)!=null && 
      bounds.upperBound(first).indexView().contains(domain.min()) && 
      bounds.upperBound(last).indexView().contains(domain.max())) {
      
      // construct the natural ordering that corresponds to the ordering of the atoms in the universe
      final IntSet ordering = Ints.bestSet(usize*usize);
      int prev = domain.min();
      for(IntIterator atoms = domain.iterator(prev+1, usize); atoms.hasNext(); ) {
        int next = atoms.next();
        ordering.add(prev*usize + next);
        prev = next;
      }
      
      if (ordering.containsAll(bounds.lowerBound(relation).indexView()) &&
        bounds.upperBound(relation).indexView().containsAll(ordering)) {
        
        // remove the ordered partition from the set of symmetric partitions
        removePartition(domain.min());

View Full Code Here

   *         {colParts: [0..r.arity)->IntSet | 
   *          all i: [0..r.arity()) | colParts[i] = bounds.upperBound[r].project(i).indexView() },
   *         null
   */
  private final IntSet[] symmetricColumnPartitions(Relation r) {
    final IntSet upper = bounds.upperBound(r).indexView();
    if (upper.isEmpty()) return null;
    
    final IntSet[] colParts = new IntSet[r.arity()];
    for(int i = r.arity()-1, min = upper.min(); i >= 0; i--, min /= usize) {
      for(IntSet part : symmetries) {
        if (part.contains(min%usize)) {
          colParts[i] = part; 
          break;
        }
      }
      if (colParts[i]==null) 
        return null;
    }
    for(IntIterator tuples = upper.iterator(); tuples.hasNext(); ) {
      for(int i = r.arity()-1, tuple = tuples.next(); i >= 0; i--, tuple /= usize) {
        if (!colParts[i].contains(tuple%usize))
          return null;
      }    
    }

View Full Code Here

0 1 2 3 4 5

TOP

Related Classes of kodkod.util.ints.IntSet

kodkod.engine.fol2sat.FOL2BoolTranslator

kodkod.engine.fol2sat.LeafInterpreter

kodkod.engine.fol2sat.SymmetryBreaker

kodkod.engine.fol2sat.SymmetryDetector

kodkod.engine.fol2sat.Translation

kodkod.engine.ResolutionBasedProof

kodkod.engine.satlab.ArrayTrace

kodkod.engine.satlab.LazyTrace

kodkod.engine.satlab.MiniSatProver

kodkod.engine.Solver

All source code are property of their respective owners. Java is a trademark of Sun Microsystems, Inc and owned by ORACLE Inc. Contact coftware#gmail.com.