Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.pa.generic
Class EnumNFindK

    java.lang.Object
      escjava.pa.generic.EnumNFindK

All Implemented Interfaces:
  Abstractor

public class EnumNFindK
extends java.lang.Object
implements Abstractor

Field Summary
`private mocha.wrappers.jbdd.jbddManager` | `bddManager`
`private java.util.Vector` | `clauses`
`private java.util.Vector` | `disj`
`private static boolean` | `invLeqK`
`private int` | `k`
`private boolean` | `noisy`
`private mocha.wrappers.jbdd.jbdd` | `R`
`private java.util.Random` | `random`
`private long` | `seed`

Constructor Summary
`EnumNFindK(mocha.wrappers.jbdd.jbddManager bddManager, int k)`

Method Summary
`private void` | `add(Disjunction d, DisjunctionProver disjProver)`
`private boolean` | `extendToMaxDisjUnknown(Disjunction nd, int i, DisjunctionProver disjProver)`
`private void` | `findMinDisjValid(Disjunction d, DisjunctionProver disjProver, long dropWhich)`
`mocha.wrappers.jbdd.jbdd` | `get()`
`java.util.Vector` | `getClauses()`
`(package private) mocha.wrappers.jbdd.jbdd` | `longsToBdd(long stars, long bits)`
`private void` | `say(java.lang.String s)`
`private int` | `size(Disjunction d)`
`boolean` | `union(Prover prover)`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### bddManager

    private mocha.wrappers.jbdd.jbddManager bddManager

### k

    private int k

### R

    private mocha.wrappers.jbdd.jbdd R

### clauses

    private java.util.Vector clauses

### disj

    private java.util.Vector disj

### noisy

    private boolean noisy

### invLeqK

    private static boolean invLeqK

### seed

    private final long seed

See Also:
  Constant Field Values

### random

    private java.util.Random random

Constructor Detail

### EnumNFindK

    public EnumNFindK(mocha.wrappers.jbdd.jbddManager bddManager,
                      int k)

Method Detail

### get

    public mocha.wrappers.jbdd.jbdd get()

  Specified by:
    `get` in interface `Abstractor`

### getClauses

    public java.util.Vector getClauses()

  Specified by:
    `getClauses` in interface `Abstractor`

### add

    private void add(Disjunction d,
                     DisjunctionProver disjProver)

### union

    public boolean union(Prover prover)

  Specified by:
    `union` in interface `Abstractor`

### findMinDisjValid

    private void findMinDisjValid(Disjunction d,
                                  DisjunctionProver disjProver,
                                  long dropWhich)

### extendToMaxDisjUnknown

    private boolean extendToMaxDisjUnknown(Disjunction nd,
                                           int i,
                                           DisjunctionProver disjProver)

### say

    private void say(java.lang.String s)

### size

    private int size(Disjunction d)

### longsToBdd

    mocha.wrappers.jbdd.jbdd longsToBdd(long stars,
                                        long bits)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage