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
Class GCProver

java.lang.Object
  extended byescjava.pa.GCProver
All Implemented Interfaces:
Prover

public class GCProver
extends java.lang.Object
implements Prover


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

bddManager

private mocha.wrappers.jbdd.jbddManager bddManager

loopPredicates

private ExprVec loopPredicates

noisy

private boolean noisy

valid

public mocha.wrappers.jbdd.jbdd valid

validClauses

public java.util.Vector validClauses

allInvalidClauses

private java.util.Vector allInvalidClauses

oldValid

private mocha.wrappers.jbdd.jbdd oldValid

ps

private java.io.PrintStream ps

subst

private VarMap subst

queriesConsidered

int queriesConsidered

queriesTried

int queriesTried

queriesValid

int queriesValid

milliSecsUsed

long milliSecsUsed
Constructor Detail

GCProver

public GCProver(mocha.wrappers.jbdd.jbddManager bddManager,
                ExprVec loopPredicates,
                GuardedCmd g,
                GCProver oldProver)
Method Detail

check

public boolean check(mocha.wrappers.jbdd.jbdd query)
Specified by:
check in interface Prover

quickCheck

public int quickCheck(mocha.wrappers.jbdd.jbdd query)
Specified by:
quickCheck in interface Prover

report

public java.lang.String report()
Specified by:
report in interface Prover

addPerfCounters

public void addPerfCounters(GCProver p)

done

public void done()

printClause

public java.lang.String printClause(mocha.wrappers.jbdd.jbdd b)
Specified by:
printClause in interface Prover

say

private void say(java.lang.String s)

processSimplifyOutput

boolean processSimplifyOutput(java.util.Enumeration results)

concretize

ExprVec concretize(java.util.Vector clauses)

concretize

Expr concretize(mocha.wrappers.jbdd.jbdd b)

size

public int size(mocha.wrappers.jbdd.jbdd b)

size

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

The ESC/Java2 Project Homepage