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)