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

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

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