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.generic
Class DisjunctionProver

java.lang.Object
  extended byescjava.pa.generic.DisjunctionProver

public class DisjunctionProver
extends java.lang.Object


Field Summary
private  mocha.wrappers.jbdd.jbddManager bddManager
           
private  java.util.ArrayList invalid
           
static int INVALID
           
private  Prover prover
           
static int UNKNOWN
           
private  java.util.ArrayList valid
           
static int VALID
           
 
Constructor Summary
DisjunctionProver(Prover prover, mocha.wrappers.jbdd.jbddManager bddManager)
           
 
Method Summary
 boolean check(Disjunction d)
           
(package private)  mocha.wrappers.jbdd.jbdd disjToBdd(Disjunction d)
           
 boolean implies(Disjunction d1, Disjunction d2)
           
 java.lang.String printClause(Disjunction d)
           
 int quickCheck(Disjunction d)
           
 java.lang.String report()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

VALID

public static final int VALID
See Also:
Constant Field Values

INVALID

public static final int INVALID
See Also:
Constant Field Values

UNKNOWN

public static final int UNKNOWN
See Also:
Constant Field Values

valid

private java.util.ArrayList valid

invalid

private java.util.ArrayList invalid

prover

private Prover prover

bddManager

private mocha.wrappers.jbdd.jbddManager bddManager
Constructor Detail

DisjunctionProver

public DisjunctionProver(Prover prover,
                         mocha.wrappers.jbdd.jbddManager bddManager)
Method Detail

quickCheck

public int quickCheck(Disjunction d)

check

public boolean check(Disjunction d)

printClause

public java.lang.String printClause(Disjunction d)

report

public java.lang.String report()

implies

public boolean implies(Disjunction d1,
                       Disjunction d2)

disjToBdd

mocha.wrappers.jbdd.jbdd disjToBdd(Disjunction d)

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