|
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 |
java.lang.Objectescjava.pa.generic.EnumNFindK
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 |
private mocha.wrappers.jbdd.jbddManager bddManager
private int k
private mocha.wrappers.jbdd.jbdd R
private java.util.Vector clauses
private java.util.Vector disj
private boolean noisy
private static boolean invLeqK
private final long seed
private java.util.Random random
Constructor Detail |
public EnumNFindK(mocha.wrappers.jbdd.jbddManager bddManager, int k)
Method Detail |
public mocha.wrappers.jbdd.jbdd get()
get
in interface Abstractor
public java.util.Vector getClauses()
getClauses
in interface Abstractor
private void add(Disjunction d, DisjunctionProver disjProver)
public boolean union(Prover prover)
union
in interface Abstractor
private void findMinDisjValid(Disjunction d, DisjunctionProver disjProver, long dropWhich)
private boolean extendToMaxDisjUnknown(Disjunction nd, int i, DisjunctionProver disjProver)
private void say(java.lang.String s)
private int size(Disjunction d)
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 |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |