|
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.GCProver
Field Summary | |
private java.util.Vector |
allInvalidClauses
|
private mocha.wrappers.jbdd.jbddManager |
bddManager
|
private ExprVec |
loopPredicates
|
(package private) long |
milliSecsUsed
|
private boolean |
noisy
|
private mocha.wrappers.jbdd.jbdd |
oldValid
|
private java.io.PrintStream |
ps
|
(package private) int |
queriesConsidered
|
(package private) int |
queriesTried
|
(package private) int |
queriesValid
|
private VarMap |
subst
|
mocha.wrappers.jbdd.jbdd |
valid
|
java.util.Vector |
validClauses
|
Fields inherited from interface escjava.pa.generic.Prover |
INVALID, UNKNOWN, VALID |
Constructor Summary | |
GCProver(mocha.wrappers.jbdd.jbddManager bddManager,
ExprVec loopPredicates,
GuardedCmd g,
GCProver oldProver)
|
Method Summary | |
void |
addPerfCounters(GCProver p)
|
boolean |
check(mocha.wrappers.jbdd.jbdd query)
|
(package private) Expr |
concretize(mocha.wrappers.jbdd.jbdd b)
|
(package private) ExprVec |
concretize(java.util.Vector clauses)
|
void |
done()
|
java.lang.String |
printClause(mocha.wrappers.jbdd.jbdd b)
|
(package private) boolean |
processSimplifyOutput(java.util.Enumeration results)
|
int |
quickCheck(mocha.wrappers.jbdd.jbdd query)
|
java.lang.String |
report()
|
private void |
say(java.lang.String s)
|
int |
size(mocha.wrappers.jbdd.jbdd b)
|
int |
size(mocha.wrappers.jbdd.jbdd b,
int nbitsFree)
|
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 ExprVec loopPredicates
private boolean noisy
public mocha.wrappers.jbdd.jbdd valid
public java.util.Vector validClauses
private java.util.Vector allInvalidClauses
private mocha.wrappers.jbdd.jbdd oldValid
private java.io.PrintStream ps
private VarMap subst
int queriesConsidered
int queriesTried
int queriesValid
long milliSecsUsed
Constructor Detail |
public GCProver(mocha.wrappers.jbdd.jbddManager bddManager, ExprVec loopPredicates, GuardedCmd g, GCProver oldProver)
Method Detail |
public boolean check(mocha.wrappers.jbdd.jbdd query)
check
in interface Prover
public int quickCheck(mocha.wrappers.jbdd.jbdd query)
quickCheck
in interface Prover
public java.lang.String report()
report
in interface Prover
public void addPerfCounters(GCProver p)
public void done()
public java.lang.String printClause(mocha.wrappers.jbdd.jbdd b)
printClause
in interface Prover
private void say(java.lang.String s)
boolean processSimplifyOutput(java.util.Enumeration results)
ExprVec concretize(java.util.Vector clauses)
Expr concretize(mocha.wrappers.jbdd.jbdd b)
public int size(mocha.wrappers.jbdd.jbdd b)
public int size(mocha.wrappers.jbdd.jbdd b, int nbitsFree)
|
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 |