escjava.pa.generic
Class DisjunctionProver

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