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

escjava.pa.generic
Class EnumNFindK

java.lang.Object
  extended byescjava.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)

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

The ESC/Java2 Project Homepage