need help on java coding - Programmers Heaven

Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Categories

need help on java coding

rduderdude Posts: 2Member
[link=http://www.hlt.utdallas.edu/~vince/cs4365/assignments/hw4/hw4.pdf]Program Details[/link][code]import java.util.Vector;
import java.util.Collections;
import java.util.Iterator;
import java.util.StringTokenizer;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;

// each literal is a string containing atoms or negation of atoms
// for example "p" or "~q".
// Literals are case sensitive. i.e., q and Q are different
class Literal
{
private String atom = "";
public Literal()
{

}
public Literal(String s)
{
atom = s;
}

public void set(String s)
{
atom = s;
}
public String get()
{
return atom;
}
public Literal getNot() // get the NOT of the literal
{
String s = "";
if(atom.charAt(0) == '~') // then this is a negative literal
{
s = s + atom.substring(1); // make it positive
}
else // this is a positive literal
{
s = "~" + atom; // make it negataive
}
return new Literal(s);
}

public boolean equals(Object o)
{
return atom.equals(((Literal)o).get());
}
}

class Clause implements Comparable
{
/* literals are stored as Vector of Literal objects
A zero sized vector means the clause to be False
*/
private Vector literals = new Vector();
private int parent[] = {-1,-1}; // parent clauses (from which this has been resolved)
private int index = -1; // original index of this clause in the sequence

// Constructors
public Clause()
{

}

public Clause(Vector l)
{
literals = l;
}

// Initialization
public void init()
{
literals = new Vector();
parent[0] = parent[1] = -1;
index = -1;
}

// set and get methods
public void setLiterals(Vector l)
{
literals = l;
}

public Vector getLiterals()
{
return literals;
}

// adds one or more disjunction
public void addLiterals(Literal l)
{
literals.add(l);
}

public void setParents(int p1, int p2)
{
parent[0] = p1;
parent[1] = p2;
}
public int[] getParents()
{
return parent;
}

public void setIndex(int i)
{
index = i;
}
public int getIndex()
{
return index;
}

public Clause isResolvable(Clause c) // is c resolvable with this
{
/*** TO BE IMPLEMENTED ***/
/* for each literal in Clause c, find whether a negative exists in "this.literals"
* if found then
* resolve two clauses using resolution rule
* return resolved clause
* if not found then
* return null;
*/
} // end public Clause isResolvable(Clause c)

public Clause resolve(Clause c) // resolve c with this
{
return isResolvable(c);
}
public boolean equals(Object o)
{
Vector v1 = ((Clause)o).getLiterals();
Vector v2 = this.literals;
int i;
// Check whether all of v1 is in v2
for(i = 0; i < v1.size() ; i ++)
{
if(!v2.contains(v1.get(i)))
return false;
}
// Check whether all of v2 is in v1
for(i = 0; i < v2.size() ; i ++)
{
if(!v1.contains(v2.get(i)))
return false;
}
return true;
}
public int compareTo(Object o)
{
return this.index - ((Clause)o).getIndex();
}
public String toString()
{
String s = "";
if(literals.size() > 0)
{
for(int i = 0; i < literals.size(); i ++)
{
s += ((Literal)literals.get(i)).get() + " ";
}
}
else
{
s = "False";
}
return s;
}

}
public class TheoremProver {

private Vector clauses = new Vector();
private Vector finalClauses = new Vector();
int lastIndex = 0;
/** Creates a new instance of TheoremProver */
public TheoremProver() {
}
// read initial clauses from file
public void readClauses(String fname)
{
try{
BufferedReader in = new BufferedReader(new FileReader(fname));
String line = "";
Vector literals = new Vector();
boolean toAdd = true;
int index = 0;

// read lines from the file
while((line = in.readLine()) != null)
{
//tokenize the literals in each line and add to literal
index ++; // new clause

StringTokenizer st = new StringTokenizer(line," ");
literals = new Vector();
toAdd = true;
while(st.hasMoreTokens())
{
String s = st.nextToken(); // next literal to be inserted
if(s.equalsIgnoreCase("TRUE")) // then a true clause, ommit the whole clause
{
toAdd = false;
break;
}
else if (s.equalsIgnoreCase("FALSE")) // then ommit this literal (makes no sense adding)
{
}
else literals.add(new Literal(s));
}
// now create a new clause
if(toAdd) // then add this clause
{
Clause cl = new Clause(literals);
cl.setIndex(index-1);
// add to the list of the current clauses
clauses.add(cl);
System.out.println(cl.toString());
}
}
}
catch (IOException e) {
System.out.println(e.getMessage());
}
}

// apply resolution
public boolean resolve()
{
/*** TO BE IMPLEMENTED ***/
/* for each clause c1, find another clause c2 that may be resolved with c1
* let r be the resolved clause
* set parents of r to be c1 and c2
* add r to the clause list if it is not already there
* if r == 'FALSE' then return true
* return false (no 'FALSE' clause found)
*/
}//public void resolve()


// write resolved clauses to file
public void writeClauses(boolean success, String outFile)
{

try{
BufferedWriter out = new BufferedWriter(new FileWriter(outFile));
if(success == false)
{
out.write("Theorem could not be proved");
}
else
{
int i,j;
// Add only the relevant clauses to the final clause

finalClauses = new Vector();
Vector v = new Vector();
v.add(clauses.get(clauses.size()-1)); //Add the False Clause
//Apply BFS to get all related clauses
while(!v.isEmpty())
{
Clause c = (Clause)v.remove(0);
if(!finalClauses.contains(c))
{
finalClauses.add(c);
System.out.println("index: " + c.getIndex() + ", parents: " + c.getParents()[0] + "," + c.getParents()[1]);
System.out.println("Clause size: " + clauses.size());
if(c.getParents()[0] != -1)
{
v.add(clauses.get(c.getParents()[0]));
v.add(clauses.get(c.getParents()[1]));
}
}
}

System.out.println("FinalClauses size: " + finalClauses.size());
Collections.sort(finalClauses);
for(i = 0; i < finalClauses.size(); i ++)
{
Clause cl = (Clause)finalClauses.get(i);
System.out.println(cl.toString());

out.write((cl.getIndex() + 1)+". ");
out.write(cl.toString()+" ");
if(cl.getParents()[0] != -1) // then has parents
{
out.write("{" + (cl.getParents()[0] + 1) + "," + (cl.getParents()[1] + 1) + "}
");
}
else
{
out.write("{}
");
}
}//for(i = 0; i < finalClauses.length; i ++)
out.write("size of final clause set: " + lastIndex + "
");
}//else
out.close();
}//try
catch(IOException e)
{
System.out.println(e.getMessage());
}
}



public static void main(String[] args) {

if(args.length != 2)
{
System.out.println("Total args = " + args.length);
System.out.println("Usage: ");
return;
}
else
{
TheoremProver tp = new TheoremProver();
tp.readClauses(args[0]);
boolean success = tp.resolve();
tp.writeClauses(success, args[1]);
System.out.println("Run complete..Please see output");
}
}
}

[/code]
need help in implementing the methods isResolvable() and resolve()
any hint would be great

Comments

Sign In or Register to comment.