Howdy, Stranger!

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

Categories

Welcome to the new platform of Programmer's Heaven! We apologize for the inconvenience caused, if you visited us from a broken link of the previous version. The main reason to move to a new platform is to provide more effective and collaborative experience to you all. Please feel free to experience the new platform and use its exciting features. Contact us for any issue that you need to get clarified. We are more than happy to help you.

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.