|
|
TruthTableApp
Proposition.java
import java.util.Random;
/**
* A class that implements many useful methods for working with
* boolean propositions.
* The logical proposition to be operated on is stored as a string.
* For all functions,
* <I>it is assumed that the expression is fully parenthisized</I>.
* The various algorithms assume this input, and assure the property
* if/when they modify the proposition.
* The only characters that should appear are '(', ')', characters,
* and the logical connectivs listed below.
* Since 'T' and 'F' stand for <I>true</I> and <I>false</I>, when they
* appear in the proposition, they will be interpreted as such.
*
* @author Chuck Cusack
* @version 1.0, 06/01
*/
//----------------------------------------------------------------------
public class Proposition extends Connectives{
public static void main(String argv[]) {
}
private BinaryTree theTree;
private String proposition; // The proposition as a String
private String literals; // The list of literals as a string
private boolean[] truthAssignment; // The truth assignment
private int numberLiterals; // The number of literal
//----------------------------------------------------------------------
private void emptyProp() {
theTree=new BinaryTree();
proposition="";
literals="";
truthAssignment=null;
numberLiterals=0;
}
//----------------------------------------------------------------------
private void trueProp() {
theTree=new BinaryTree('T',0);
proposition="T";
literals="";
truthAssignment=null;
numberLiterals=0;
}
//----------------------------------------------------------------------
private void falseProp() {
theTree=new BinaryTree('F',0);
proposition="F";
literals="";
truthAssignment=null;
numberLiterals=0;
}
//----------------------------------------------------------------------
private void singleLiteralProp(char L) {
theTree=new BinaryTree(L,0);
proposition=new String(L+"");
literals=proposition;
truthAssignment=new boolean[1];
truthAssignment[0]=true;
numberLiterals=1;
}
//----------------------------------------------------------------------
public Proposition() { falseProp(); }
public Proposition(String S) {
theTree=new BinaryTree();
setProp(S); }
//----------------------------------------------------------------------
public void setProp(String S) {
proposition=toUnicode(S);
extractLiterals();
theTree.setProposition(S);
}
public String getProp() { return theTree.InOrder(true); }
public String getProp(TreeNode R) {
return theTree.InOrder(R,true); }
public int getNumberLiterals() { return numberLiterals; }
public boolean setTruthAssignment(boolean []TA) {
if(TA.length==truthAssignment.length) {
truthAssignment=TA;
return true;
}
else return false;
}
//----------------------------------------------------------------------
public void updatePropFromTree() { setProp(theTree.InOrder(true)); }
//----------------------------------------------------------------------
public void randomProp(int seed,int terms,int difficulty) {
Random R=new Random(seed);
int minSize=4*(terms+difficulty-1)-3+1;
int maxSize=minSize+3;
StringBuffer leaves=new StringBuffer("ABCDHJKLMNRSWXYZ");
while(leaves.length()>terms) {
int ind=R.nextInt(leaves.length());
leaves.delete(ind,ind+1);
}
int x=difficulty-R.nextInt(Math.min(3,difficulty+1));
leaves.append(leaves);
leaves.append("TF");
int tries=0;
do {
theTree=randomProp(leaves,terms+x,R,difficulty-x);
updatePropFromTree();
tries++;
}
while(numberLiterals!=terms || getProp().length()>maxSize
|| getProp().length()<minSize);
}
public BinaryTree randomProp(StringBuffer leaves,int numTerms,
Random R,int difficulty) {
if(numTerms==0) return null;
char[] symbols={AND,OR,XOR,AND,OR,XOR,OR, CONDITIONAL,BICONDITIONAL,AND};
if(R.nextInt(8)<difficulty) {
return new BinaryTree(new TreeNode(NEGATION,-1),
null,randomProp(leaves,numTerms,R,difficulty).getRoot()
);
}
else if(numTerms==1) {
int choice=R.nextInt(leaves.length());
return new BinaryTree(new TreeNode(leaves.charAt(choice),-1));
}
else {
int choice=R.nextInt(symbols.length);
int left=1+R.nextInt(numTerms-1);
return new BinaryTree(new TreeNode(symbols[choice],-1),
randomProp(leaves,left,R,difficulty),
randomProp(leaves,numTerms-left,R,difficulty)
);
}
}
//----------------------------------------------------------------------
/**
* Go through the string and extract the literals from it.
* It places them in the class variable 'lits'.
* Each literal is included only ONCE, no matter how many times
* it occurs in the proposition.
* The characters 'T' and 'F' are assumed to stand for
* true and false, so are ignored.
*/
private void extractLiterals() {
if(proposition.length()==0) {
literals=null;
numberLiterals=0;
truthAssignment=null;
return ;
}
literals=new String();
for(int i=0;i<proposition.length();i++) {
char t=proposition.charAt(i);
if(Character.isLetter(t)) {
if(literals.indexOf(t)==-1 && t!='T' && t!='F')
literals=literals+t;
}
}
numberLiterals=literals.length();
truthAssignment=new boolean[numberLiterals];
allTrue();
}
//----------------------------------------------------------------------
public boolean[] getTruthAssignment() { return truthAssignment; }
//----------------------------------------------------------------------
public void allTrue() {
for(int i=0;i<numberLiterals;i++) { truthAssignment[i]=true; }
}
public void allFalse() {
for(int i=0;i<numberLiterals;i++) { truthAssignment[i]=false; }
}
//----------------------------------------------------------------------
private void nextTruthAssign() {
int i=numberLiterals-1;
while(i>=0 && truthAssignment[i]==false) {
truthAssignment[i]=true; i--; }
if(i>=0) { truthAssignment[i]=false; }
}
//----------------------------------------------------------------------
public boolean getTruthValue() {
return getTruthValue(theTree.getRoot());
}
//----------------------------------------------------------------------
private boolean getTruthValue(TreeNode r) {
char value=r.getKey();
if(isNEGATION(value)) {
return (!getTruthValue(r.getRight()));
}
else if(isOR(value)) {
return(getTruthValue(r.getLeft()) | getTruthValue(r.getRight()));
}
else if(isAND(value)) {
return(getTruthValue(r.getLeft()) & getTruthValue(r.getRight()));
}
else if(isXOR(value)) {
return(getTruthValue(r.getLeft()) ^ getTruthValue(r.getRight()));
}
else if(isBICONDITIONAL(value)) {
return(getTruthValue(r.getLeft()) == getTruthValue(r.getRight()));
}
else if(isCONDITIONAL(value)) {
return(!(getTruthValue(r.getLeft()) &
(!getTruthValue(r.getRight()))));
}
else if(value=='T') return true;
else if(value=='F') return false;
else { // It had better be a literal...
int ind=literals.indexOf(value);
if(ind!=-1) return truthAssignment[ind];
else return false; // Why not?
}
}
//----------------------------------------------------------------------
public String[] getTruthTableTitle() {
String[] theTable=new String[numberLiterals];
for(int i=0;i<numberLiterals;i++) theTable[i]=literals.substring(i,i+1);
return theTable;
}
//----------------------------------------------------------------------
public boolean [] getAllTruthValues() {
boolean [] tTable=new boolean[(int) Math.pow(2,numberLiterals)];
allTrue();
for(int i=0;i<tTable.length;i++) {
tTable[i]=getTruthValue();
nextTruthAssign();
}
return tTable;
}
//----------------------------------------------------------------------
public Boolean[][] getAllTruthAssignments() {
int rows=(int) Math.pow(2,numberLiterals);
Boolean[][] theTable=new Boolean[rows][numberLiterals];
allTrue();
for(int i=0;i<rows;i++) {
boolean [] ta=getTruthAssignment();
for(int j=0;j<numberLiterals;j++) {
theTable[i][j]=new Boolean(ta[j]);
}
nextTruthAssign();
}
return theTable;
}
//----------------------------------------------------------------------
/**
* Determine whether or not the substring from firstindex to lastindex-1
* is a valid proposition.
*
* @param firstindex the beginning index, inclusive
* @param lastindex the ending index, exclusive
* @param method the equivalence to apply. See below for a list of the
* methods and associated numbers. The function should be called with
* the method name, not its number for clarity.
* @return true if the operation was successful, false otherwise
*
*/
public boolean isSubProp(int firstindex,int lastindex) {
String subprop=theTree.substringTree(firstindex,lastindex).InOrder(true);
return(subprop.equals(proposition.substring(firstindex,lastindex)));
}
//----------------------------------------------------------------------
public static final int DNA=100;
public static final int OK=101;
public static final int INVALID_PROP=102;
public static final int INVALID_EQUIVALENCE=103;
//----------------------------------------------------------------------
/**
* Apply the given equivalence to the substring starting at firstindex
* and ending at lastindex-1.
*
* @param firstindex the beginning index, inclusive
* @param lastindex the ending index, exclusive
* @param method the equivalence to apply. See below for a list of the
* methods and associated numbers. The function should be called with
* the method name, not its number for clarity.
* @return true if the operation was successful, false otherwise
*
*/
public int applyEquivalence(int firstindex, int lastindex, int method) {
return applyEquivalence(firstindex,lastindex,method,"");
}
//----------------------------------------------------------------------
/**
* Apply the given equivalence to the substring starting at firstindex
* and ending at lastindex-1.
*
* @param firstindex the beginning index, inclusive
* @param lastindex the ending index, exclusive
* @param method the equivalence to apply. See below for a list of the
* methods and associated numbers. The function should be called with
* the method name, not its number for clarity.
* @param S A string used in certain identities. For instance the identity
* T => A AND T needs an input string.
* @return true if the operation was successful, false otherwise
*
*/
public int applyEquivalence(int firstindex, int lastindex, int method,
String S) {
int result;
if(!isSubProp(firstindex,lastindex)) {
return INVALID_PROP;
}
TreeNode R=theTree.substringTree(firstindex,lastindex).getRoot();
if(R==null) {
return INVALID_PROP; // This shouldn't happen, but...
}
switch (method) {
case AND_IDENT:
result=applyAndIdent(R);
break;
case AND_IDENT_R:
result=applyAndIdentR(R);
break;
case OR_IDENT:
result=applyOrIdent(R);
break;
case OR_IDENT_R:
result=applyOrIdentR(R);
break;
case OR_DOMIN:
result=applyOrDomin(R);
break;
case OR_DOMIN_R:
result=applyOrDominR(R,S);
break;
case AND_DOMIN:
result=applyAndDomin(R);
break;
case AND_DOMIN_R:
result=applyAndDominR(R,S);
break;
case OR_IDEM:
result=applyOrIdem(R);
break;
case OR_IDEM_R:
result=applyOrIdemR(R);
break;
case AND_IDEM:
result=applyAndIdem(R);
break;
case AND_IDEM_R:
result=applyAndIdemR(R);
break;
case NEG:
result=applyNeg(R);
break;
case NEG_R:
result=applyNegR(R);
break;
case OR_COMMUTE:
result=applyOrCommute(R);
break;
case OR_COMMUTE_R:
result=applyOrCommute(R);
break;
case AND_COMMUTE:
result=applyAndCommute(R);
break;
case AND_COMMUTE_R:
result=applyAndCommute(R);
break;
case OR_ASSOC:
result=applyOrAssoc(R);
break;
case OR_ASSOC_R:
result=applyOrAssocr(R);
break;
case AND_ASSOC:
result=applyAndAssoc(R);
break;
case AND_ASSOC_R:
result=applyAndAssocR(R);
break;
case OR_DIST:
result=applyOrDist(R);
break;
case OR_DIST_R:
result=applyOrDistR(R);
break;
case AND_DIST:
result=applyAndDist(R);
break;
case AND_DIST_R:
result=applyAndDistR(R);
break;
case AND_DEMORGAN:
result=applyAndDemorgan(R);
break;
case AND_DEMORGAN_R:
result=applyAndDemorganR(R);
break;
case OR_DEMORGAN:
result=applyOrDemorgan(R);
break;
case OR_DEMORGAN_R:
result=applyOrDemorganR(R);
break;
case P_OR_NOT_P:
result=applyPOrNotP(R);
break;
case P_OR_NOT_P_R:
result=applyPOrNotPR(R,S);
break;
case P_AND_NOT_P:
result=applyPAndNotP(R);
break;
case P_AND_NOT_P_R:
result=applyPAndNotPR(R,S);
break;
case IMPLICATION:
result=applyImplication(R);
break;
case IMPLICATION_R:
result=applyImplicationR(R);
break;
case NOT_FALSE:
result=applyNotFalse(R);
break;
case NOT_FALSE_R:
result=applyNotFalseR(R);
break;
case NOT_TRUE:
result=applyNotTrue(R);
break;
case NOT_TRUE_R:
result=applyNotTrueR(R);
break;
case CONTRAPOSITIVE:
result=applyContrapositive(R);
break;
case CONTRAPOSITIVE_R:
result=applyContrapositiveR(R);
break;
case IFF:
result=applyIFF(R);
break;
case IFF_R:
result=applyIFFR(R);
break;
case XOR_DEF:
result=applyXORDEF(R);
break;
case XOR_DEF_R:
result=applyXORDEFR(R);
break;
default:
result=INVALID_EQUIVALENCE;
}
if(result==OK) {
updatePropFromTree();
}
return result;
}
//----------------------------------------------------------------------
/**
* The Logical Equivalences. Each function has an associated constant.
* The ones ending in "R" are the identities in the reverse order.
*/
private int applyAndIdent(TreeNode R) {
if(isAND(R.getKey())) {
if(getProp(R.getLeft()).equals("T") ) {
R.removeLeft();
theTree.spliceOut(R);
return OK;
}
else if(getProp(R.getRight()).equals("T") ) {
R.removeRight();
theTree.spliceOut(R);
return OK;
}
else
return DNA;
}
return DNA;
}
//----------------------------------------------------------------------
private int applyAndIdentR(TreeNode R) {
TreeNode newAnd=new TreeNode(AND);
theTree.spliceInLeft(R,newAnd);
newAnd.setRight(new TreeNode('T',-1));
return OK;
}
//----------------------------------------------------------------------
private int applyOrIdent(TreeNode R) {
if(isOR(R.getKey())) {
if(getProp(R.getLeft()).equals("F") ) {
R.removeLeft();
theTree.spliceOut(R);
return OK;
}
else if(getProp(R.getRight()).equals("F") ) {
R.removeRight();
theTree.spliceOut(R);
return OK;
}
else return DNA;
}
return DNA;
}
//----------------------------------------------------------------------
private int applyOrIdentR(TreeNode R) {
TreeNode newOr=new TreeNode(OR);
theTree.spliceInLeft(R,newOr);
newOr.setRight(new TreeNode('F',-1));
return OK;
}
//----------------------------------------------------------------------
private int applyOrDomin(TreeNode R) {
if(isOR(R.getKey()) && (getProp(R.getLeft()).equals("T") ||
getProp(R.getRight()).equals("T") ) ) {
theTree.replaceSubtree(R,new TreeNode('T',-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrDominR(TreeNode R,String S) {
if(getProp(R).equals("T")) {
TreeNode A=new TreeNode(OR,-1);
theTree.spliceInRight(R,A);
BinaryTree T=new BinaryTree(S,BinaryTree.LOGIC_PROP);
A.setLeft(T.getRoot());
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndDomin(TreeNode R) {
if(isAND(R.getKey()) && (getProp(R.getLeft()).equals("F") ||
getProp(R.getRight()).equals("F") ) )
{
theTree.replaceSubtree(R,new TreeNode('F',-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndDominR(TreeNode R,String S) {
if(getProp(R).equals("F")) {
TreeNode A=new TreeNode(AND,-1);
theTree.spliceInRight(R,A);
BinaryTree T=new BinaryTree(S,BinaryTree.LOGIC_PROP);
A.setLeft(T.getRoot());
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrIdem(TreeNode R) {
if(isOR(R.getKey()) && getProp(R.getLeft()).equals(getProp(R.getRight()))) {
R.removeLeft();
theTree.spliceOut(R);
return OK;
}
else
return DNA;
}
//----------------------------------------------------------------------
private int applyOrIdemR(TreeNode R) {
TreeNode A=new TreeNode(OR,-1);
theTree.spliceInLeft(R,A);
A.setRight(R); // I am cheating here by making the subtree R BOTH children
return OK;
}
//----------------------------------------------------------------------
private int applyAndIdem(TreeNode R) {
if(isAND(R.getKey()) && getProp(R.getLeft()).equals(getProp(R.getRight()))) {
R.removeLeft();
theTree.spliceOut(R);
return OK;
}
else
return DNA;
}
//----------------------------------------------------------------------
private int applyAndIdemR(TreeNode R) {
TreeNode A=new TreeNode(AND,-1);
theTree.spliceInLeft(R,A);
A.setRight(R); // I am cheating here by making the subtree R BOTH children
return OK;
}
//----------------------------------------------------------------------
private int applyNeg(TreeNode R) {
TreeNode RR=R.getRight();
if (isNEGATION(R.getKey()) && RR!=null && isNEGATION(RR.getKey()) ) {
theTree.spliceOut(R);
theTree.spliceOut(RR);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyNegR(TreeNode R) {
TreeNode N1=new TreeNode(NEGATION,-1);
TreeNode N2=new TreeNode(NEGATION,-1);
theTree.spliceInRight(R,N1);
theTree.spliceInRight(N1,N2);
return OK;
}
//----------------------------------------------------------------------
private int applyOrCommute(TreeNode R) {
if(isOR(R.getKey())) {
TreeNode T=R.getLeft();
R.setLeft(R.getRight());
R.setRight(T);
return OK;
}
else return DNA;
}
private int applyAndCommute(TreeNode R) {
if(isAND(R.getKey())) {
R.swapChildren();
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrAssoc(TreeNode R) {
if(isOR(R.getKey()) && isOR(R.getLeft().getKey())) {
theTree.rightRotate(R);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrAssocr(TreeNode R) {
if(isOR(R.getKey()) && isOR(R.getRight().getKey())) {
theTree.leftRotate(R);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndAssoc(TreeNode R) {
if(isAND(R.getKey()) && isAND(R.getLeft().getKey())) {
theTree.rightRotate(R);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndAssocR(TreeNode R) {
if(isAND(R.getKey()) && isAND(R.getRight().getKey())) {
theTree.leftRotate(R);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrDist(TreeNode R) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if(isOR(R.getKey()) && isAND(RR.getKey())) {
theTree.leftRotate(R);
TreeNode A=new TreeNode(OR,-1);
theTree.spliceInRight(RR.getRight(),A);
A.setLeft(RL);
return OK;
}
else if(isOR(R.getKey()) && isAND(RL.getKey())) {
theTree.rightRotate(R);
TreeNode A=new TreeNode(OR,-1);
theTree.spliceInLeft(RL.getLeft(),A);
A.setRight(RR);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrDistR(TreeNode R) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if(isAND(R.getKey()) && isOR(RR.getKey()) && isOR(RL.getKey())) {
if(RR.getLeft()==null || RR.getRight()==null ||
RL.getLeft()==null || RL.getRight()==null )
return DNA;
if(RL.getLeft().getKey()==RR.getLeft().getKey()) {
RR.removeLeft();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else if(RL.getLeft().getKey()==RR.getRight().getKey()) {
RR.removeRight();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else if(RL.getRight().getKey()==RR.getLeft().getKey()) {
applyOrCommute(RL);
RR.removeLeft();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else if(RL.getRight().getKey()==RR.getRight().getKey()) {
applyOrCommute(RL);
RR.removeRight();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else return DNA;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndDist(TreeNode R) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if(isAND(R.getKey()) && isOR(RR.getKey())) {
theTree.leftRotate(R);
TreeNode A=new TreeNode(AND,-1);
theTree.spliceInRight(RR.getRight(),A);
A.setLeft(RL);
return OK;
}
else if(isAND(R.getKey()) && isOR(RL.getKey())) {
theTree.rightRotate(R);
TreeNode A=new TreeNode(AND,-1);
theTree.spliceInLeft(RL.getLeft(),A);
A.setRight(RR);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndDistR(TreeNode R) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if(isOR(R.getKey()) && isAND(RR.getKey()) && isAND(RL.getKey())) {
if(RR.getLeft()==null || RR.getRight()==null ||
RL.getLeft()==null || RL.getRight()==null )
return DNA;
if(RL.getLeft().getKey()==RR.getLeft().getKey()) {
RR.removeLeft();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else if(RL.getLeft().getKey()==RR.getRight().getKey()) {
RR.removeRight();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else if(RL.getRight().getKey()==RR.getLeft().getKey()) {
applyAndCommute(RL);
RR.removeLeft();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else if(RL.getRight().getKey()==RR.getRight().getKey()) {
applyAndCommute(RL);
RR.removeRight();
theTree.spliceOut(RR);
theTree.rightRotate(R);
return OK;
}
else return DNA;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndDemorgan(TreeNode R) {
TreeNode RR=R.getRight();
if(isNEGATION(R.getKey()) && isAND(RR.getKey())) {
theTree.spliceOut(R);
RR.setKey(OR);
theTree.spliceInRight(RR.getLeft(),new TreeNode(NEGATION,-1));
theTree.spliceInRight(RR.getRight(),new TreeNode(NEGATION,-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyAndDemorganR(TreeNode R) {
if(isOR(R.getKey()) && isNEGATION(R.getLeft().getKey())
&& isNEGATION(R.getRight().getKey()) ) {
theTree.spliceOut(R.getRight());
theTree.spliceOut(R.getLeft());
R.setKey(AND);
theTree.spliceInRight(R,new TreeNode(NEGATION,-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrDemorgan(TreeNode R) {
TreeNode RR=R.getRight();
if(isNEGATION(R.getKey()) && isOR(RR.getKey())) {
theTree.spliceOut(R);
RR.setKey(AND);
theTree.spliceInRight(RR.getLeft(),new TreeNode(NEGATION,-1));
theTree.spliceInRight(RR.getRight(),new TreeNode(NEGATION,-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyOrDemorganR(TreeNode R) {
if(isAND(R.getKey()) && isNEGATION(R.getLeft().getKey())
&& isNEGATION(R.getRight().getKey()) ) {
theTree.spliceOut(R.getRight());
theTree.spliceOut(R.getLeft());
R.setKey(OR);
theTree.spliceInRight(R,new TreeNode(NEGATION,-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyPOrNotP(TreeNode R) {
if(isOR(R.getKey())) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if((isNEGATION(RR.getKey()) &&
getProp(RR.getRight()).equals(getProp(RL))) ||
(isNEGATION(RL.getKey()) &&
getProp(RL.getRight()).equals(getProp(RR)))) {
theTree.replaceSubtree(R,new TreeNode('T',-1));
return OK;
}
}
return DNA;
}
//----------------------------------------------------------------------
private int applyPOrNotPR(TreeNode R,String S) {
if(getProp(R).equals("T")) {
BinaryTree A=new BinaryTree(S,BinaryTree.LOGIC_PROP);
TreeNode ORNode=new TreeNode(OR,-1);
theTree.replaceSubtree(R,ORNode);
ORNode.setLeft(A.getRoot());
ORNode.setRight(new TreeNode(NEGATION,-1));
ORNode.getRight().setRight(A.getRoot()); // Cheating again by using the
// subtree twice--it gets fixed...
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyPAndNotP(TreeNode R) {
if(isAND(R.getKey())) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if( (isNEGATION(RR.getKey()) &&
getProp(RR.getRight()).equals(getProp(RL))) ||
(isNEGATION(RL.getKey()) &&
getProp(RL.getRight()).equals(getProp(RR))) ) {
theTree.replaceSubtree(R,new TreeNode('F',-1));
return OK;
}
}
return DNA;
}
//----------------------------------------------------------------------
private int applyPAndNotPR(TreeNode R,String S) {
if(getProp(R).equals("F")) {
BinaryTree A=new BinaryTree(S,BinaryTree.LOGIC_PROP);
TreeNode ANDNode=new TreeNode(AND,-1);
theTree.replaceSubtree(R,ANDNode);
ANDNode.setLeft(A.getRoot());
ANDNode.setRight(new TreeNode(NEGATION,-1));
ANDNode.getRight().setRight(A.getRoot()); // Cheating again by using the
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyImplication(TreeNode R) {
if(isCONDITIONAL(R.getKey())) {
R.setKey(OR);
theTree.spliceInRight(R.getLeft(),new TreeNode(NEGATION,-1));
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyImplicationR(TreeNode R) {
if(isOR(R.getKey()) && R.getLeft()!=null &&
isNEGATION(R.getLeft().getKey())) {
R.setKey(CONDITIONAL);
theTree.spliceOut(R.getLeft());
return OK;
}
else if(isOR(R.getKey()) && R.getRight()!=null &&
isNEGATION(R.getRight().getKey())) {
R.swapChildren();
R.setKey(CONDITIONAL);
theTree.spliceOut(R.getLeft());
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyContrapositive(TreeNode R) {
if(isCONDITIONAL(R.getKey())) {
R.swapChildren();
theTree.spliceInRight(R.getLeft(),new TreeNode(NEGATION));
theTree.spliceInRight(R.getRight(),new TreeNode(NEGATION));
return OK;
}
else return DNA;
}
private int applyContrapositiveR(TreeNode R) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if(isCONDITIONAL(R.getKey()) && isNEGATION(RR.getKey())
&& isNEGATION(RL.getKey())) {
theTree.spliceOut(RR);
theTree.spliceOut(RL);
R.swapChildren();
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyNotFalse(TreeNode R) {
if(isNEGATION(R.getKey()) && R.getRight().getKey()=='F') {
R.setKey('T');
R.removeRight();
return OK;
}
else return DNA;
}
private int applyNotFalseR(TreeNode R) {
if(R.getKey()=='T') {
R.setKey(NEGATION);
R.setRight('F');
return OK;
}
else return DNA;
}
private int applyNotTrue(TreeNode R) {
if(isNEGATION(R.getKey()) && R.getRight().getKey()=='T') {
R.setKey('F');
R.removeRight();
return OK;
}
else return DNA;
}
private int applyNotTrueR(TreeNode R) {
if(R.getKey()=='F') {
R.setKey(NEGATION);
R.setRight('T');
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyIFF(TreeNode R) {
if(isBICONDITIONAL(R.getKey())) {
TreeNode RL=R.getLeft();
TreeNode RR=R.getRight();
R.setKey(AND);
R.setLeft(new TreeNode(CONDITIONAL,RL,RR));
R.setRight(new TreeNode(CONDITIONAL,RR,RL));
return OK;
}
else return DNA;
}
private int applyIFFR(TreeNode R) {
TreeNode RR=R.getRight();
TreeNode RL=R.getLeft();
if(isAND(R.getKey()) &&
isCONDITIONAL(RR.getKey()) &&
isCONDITIONAL(RL.getKey()) &&
getProp(RL.getLeft()).equals(getProp(RR.getRight())) &&
getProp(RL.getRight()).equals(getProp(RR.getLeft())) ) {
R.removeRight();
theTree.spliceOut(R);
RL.setKey(BICONDITIONAL);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
private int applyXORDEF(TreeNode R) {
if(isXOR(R.getKey())) {
TreeNode RL=R.getLeft();
TreeNode RR=R.getRight();
TreeNode np=new TreeNode(NEGATION,null,RL);
TreeNode nq=new TreeNode(NEGATION,null,RR);
R.setKey(OR);
R.setLeft(new TreeNode(AND,RL,nq));
R.setRight(new TreeNode(AND,np,RR));
return OK;
}
else return DNA;
}
private int applyXORDEFR(TreeNode R) {
TreeNode RL=R.getLeft();
TreeNode RLL=RL.getLeft();
TreeNode RLR=RL.getRight();
TreeNode RR=R.getRight();
TreeNode RRR=RR.getRight();
TreeNode RRL=RR.getLeft();
if(isOR(R.getKey()) &&
isAND(RR.getKey()) &&
isAND(RL.getKey()) &&
isNEGATION(RLR.getKey()) &&
isNEGATION(RRL.getKey()) &&
getProp(RLR.getRight()).equals(getProp(RRR)) &&
getProp(RRL.getRight()).equals(getProp(RLL))
) {
R.setKey(XOR);
R.setLeft(RLL);
R.setRight(RRR);
return OK;
}
else return DNA;
}
//----------------------------------------------------------------------
public static final int NOT_FALSE= 0; // (!F) => T
public static final int NOT_FALSE_R= 1; // T => (!F)
public static final int NOT_TRUE= 2; // (!T) => F
public static final int NOT_TRUE_R= 3; // F => (!T)
public static final int AND_IDENT= 4; // p&T => p
// T&p => p
public static final int AND_IDENT_R= 5; // p => p&T
public static final int OR_IDENT= 6; // p|F => p
public static final int OR_IDENT_R= 7; // p => p|F
public static final int OR_DOMIN= 8; // p|T => T
public static final int OR_DOMIN_R= 9; // T => p|T
public static final int AND_DOMIN=10; // p&F => F
// F&P => F
public static final int AND_DOMIN_R=11; // F => p&F
public static final int OR_IDEM=12; // p|p => p
public static final int OR_IDEM_R=13; // p => p|p
public static final int AND_IDEM=14; // p&p => p
public static final int AND_IDEM_R=15; // p => p&p
public static final int NEG=16; // !(!p) => p
public static final int NEG_R=17; // p => !(!p)
public static final int OR_COMMUTE=18; // p|q => q|p
public static final int OR_COMMUTE_R=19; // p|q => q|p
public static final int AND_COMMUTE=20; // p&q => q&p
public static final int AND_COMMUTE_R=21; // p&q => q&p
public static final int OR_ASSOC=22; // (p|q)|r => p|(q|r)
public static final int OR_ASSOC_R=23; // p|(q|r) => (p|q)|r
public static final int AND_ASSOC=24; // (p&q)&r => p&(q&r)
public static final int AND_ASSOC_R=25; // p&(q&r) => (p&q)&r
public static final int OR_DIST=26; // p|(q&r) => (p|q)&(p|r)
public static final int OR_DIST_R=27; // (p|q)&(p|r) => p|(q&r)
// (p|q)&(r|p) => p|(q&r)
// (q|p)&(p|r) => p|(q&r)
// (q|p)&(r|p) => p|(q&r)
public static final int AND_DIST=28; // p&(q|r) => (p&q)|(p&r)
public static final int AND_DIST_R=29; // (p&q)|(p&r) => p&(q|r)
// (p&q)|(r&p) => p&(q|r)
// (q&p)|(p&r) => p&(q|r)
// (q&p)|(r&p) => p&(q|r)
public static final int AND_DEMORGAN=30; // !(p&q) => (!p)|(!q)
public static final int AND_DEMORGAN_R=31; // (!p)|(!q) => !(p&q)
public static final int OR_DEMORGAN=32; // !(p|q) => (!p)&(!q)
public static final int OR_DEMORGAN_R=33; // (!p)&(!q) => !(p|q)
public static final int P_OR_NOT_P=34; // p|!p => T
// !p|p => T
public static final int P_OR_NOT_P_R=35; // T => p|!p
public static final int P_AND_NOT_P=36; // p&!p => F
// !p&p => F
public static final int P_AND_NOT_P_R=37; // F => p&!p
public static final int IMPLICATION=38; // p->q => !p|q
public static final int IMPLICATION_R=39; // !p|q => p->q
public static final int CONTRAPOSITIVE=40; // (p->q) => (!q)->(!p)
public static final int CONTRAPOSITIVE_R=41; // ((!p)->(!q)) => (q->p)
public static final int IFF=42; // (p<->q) <=> (p->q)&(q->p)
public static final int IFF_R=43; // (p->q)&(q->p) <=> (p<->q)
public static final int XOR_DEF=44; // (p^q) <=> (!p&q)|(p&!q)
public static final int XOR_DEF_R=45; // (p&!q)|(!p&q) <=> (p^q)
//----------------------------------------------------------------------
public static final String []EquivList={
"("+NEGATION+"F) <=> T",
"("+NEGATION+"T) <=> F",
"(P"+AND+"T) <=> P",
"(P"+OR+"F) <=> P",
"(P"+OR+"T) <=> T",
"(P"+AND+"F) <=> F",
"(P"+OR+"P) <=> P",
"(P"+AND+"P) <=> P",
"("+NEGATION+"("+NEGATION+"P)) <=> P",
"(P"+OR+"Q) <=> (Q"+OR+"P)",
"(P"+AND+"Q) <=> (Q"+AND+"P)",
"((P"+OR+"Q)"+OR+"R) <=> (P"+OR+"(Q"+OR+"R))",
"((P"+AND+"Q)"+AND+"R) <=> (P"+AND+"(Q"+AND+"R))",
"(P"+OR+"(Q"+AND+"R)) <=> ((P"+OR+"Q)"+AND+"(P"+OR+"R))",
"(P"+AND+"(Q"+OR+"R)) <=> ((P"+AND+"Q)"+OR+"(P"+AND+"R))",
"("+NEGATION+"(P"+AND+"Q)) <=> (("+NEGATION+"P)"+OR+"("+NEGATION+"Q))",
"("+NEGATION+"(P"+OR+"Q)) <=> (("+NEGATION+"P)"+AND+"("+NEGATION+"Q))",
"(P"+OR+"("+NEGATION+"P)) <=> T",
"(P"+AND+"("+NEGATION+"P)) <=> F",
"(P"+CONDITIONAL+"Q) <=> (("+NEGATION+"P)"+OR+"Q)",
"(P"+CONDITIONAL+"Q) <=> (("+NEGATION+"Q)"+CONDITIONAL+"("+NEGATION
+"P))",
"(P"+BICONDITIONAL+"Q) <=> ((P"+CONDITIONAL+"Q)"+AND+"(Q"+CONDITIONAL
+"P))",
"(P"+XOR+"Q) <=> ((P"+AND+"("+NEGATION+"Q))"+OR
+"(("+NEGATION+"P)"+AND+"Q))"
};
public static final String []EquivList2={
"("+NEGATION+"F) => T",
"T => ("+NEGATION+"F)",
"("+NEGATION+"T) => F",
"F => ("+NEGATION+"T)",
"(P"+AND+"T) => P",
"P => (P"+AND+"T)",
"(P"+OR+"F) => P",
"P => (P"+OR+"F)",
"(P"+OR+"T) => T",
"T => (P"+OR+"T)",
"(P"+AND+"F) => F",
"F => (P"+AND+"F)",
"(P"+OR+"P) => P",
"P => (P"+OR+"P)",
"(P"+AND+"P) => P",
"P => (P"+AND+"P)",
"("+NEGATION+"("+NEGATION+"P)) => P",
"P => ("+NEGATION+"("+NEGATION+"P))",
"(P"+OR+"Q) => (Q"+OR+"P)",
"(Q"+OR+"P) => (P"+OR+"Q)",
"(P"+AND+"Q) => (Q"+AND+"P)",
"(Q"+AND+"P) => (P"+AND+"Q)",
"((P"+OR+"Q)"+OR+"R) => (P"+OR+"(Q"+OR+"R))",
"(P"+OR+"(Q"+OR+"R)) => ((P"+OR+"Q)"+OR+"R)",
"((P"+AND+"Q)"+AND+"R) => (P"+AND+"(Q"+AND+"R))",
"(P"+AND+"(Q"+AND+"R)) => ((P"+AND+"Q)"+AND+"R)",
"(P"+OR+"(Q"+AND+"R))=> "+
"((P"+OR+"Q)"+AND+"(P"+OR+"R))",
"((P"+OR+"Q)"+AND+"(P"+OR+"R)) => "+
"(P"+OR+"(Q"+AND+"R))",
"(P"+AND+"(Q"+OR+"R)) => "+
"((P"+AND+"Q)"+OR+"(P"+AND+"R))",
"((P"+AND+"Q)"+OR+"(P"+AND+"R)) => "+
"(P"+AND+"(Q"+OR+"R))",
"("+NEGATION+"(P"+AND+"Q)) => (("+
NEGATION+"P)"+OR+"("+NEGATION+"Q))",
"(("+NEGATION+"P)"+OR+"("+NEGATION+"Q))"+
" => ("+NEGATION+"(P"+AND+"Q))",
"("+NEGATION+"(P"+OR+"Q)) => (("+
NEGATION+"P)"+AND+"("+NEGATION+"Q))",
"(("+NEGATION+"P)"+AND+"("+NEGATION+"Q))"+
" => ("+NEGATION+"(P"+OR+"Q))",
"(P"+OR+"("+NEGATION+"P)) => T",
"T => (P"+OR+"("+NEGATION+"P))",
"(P"+AND+"("+NEGATION+"P)) => F",
"F => (P"+AND+"("+NEGATION+"P))",
"(P"+CONDITIONAL+"Q) => (("+NEGATION+"P)"+OR+"Q)",
"(("+NEGATION+"P)"+OR+"Q) => (P"+CONDITIONAL+"Q)",
"(P"+CONDITIONAL+"Q) => (("+NEGATION+"Q)"+CONDITIONAL+"("+NEGATION
+"P))",
"(("+NEGATION+"Q)"+CONDITIONAL+"("+NEGATION
+"P)) => (P"+CONDITIONAL+"Q)",
"(P"+BICONDITIONAL+"Q) => (P"+CONDITIONAL+"Q)"
+AND+"(Q"+CONDITIONAL+"P))",
"(P"+CONDITIONAL+"Q)"+AND+"(Q"+CONDITIONAL
+"P)) => (P"+BICONDITIONAL+"Q)",
"(P"+XOR+"Q) => ((P"+AND+"("+NEGATION+"Q))"
+OR+"(("+NEGATION+"P)"+AND+"Q))",
"((P"+AND+"("+NEGATION+"Q))"+OR+"(("+NEGATION+"P)"+AND
+"Q)) => (P"+XOR+"Q)"
};
public static final String[] EquivNames={
"definition of T/F",
"definition of T/F",
"AND identity",
"OR identity",
"OR domination law",
"AND domination law",
"OR idempotent law",
"AND idempotent law",
"double NEGATION law",
"OR commutative law",
"AND commutative law",
"OR associative law",
"AND associative law",
"OR distributive law",
"AND distributive law",
"DeMorgan's law with AND",
"DeMorgan's law with OR",
"OR complement law",
"AND complement law",
"conditional law",
"contrapositive",
"definition of biconditional",
"definition of XOR"
};
//----------------------------------------------------------------------
}
|