- minor performance tweaks to OTTER Like theorem prover (delaying factoring and ordering of lightest clauses).

Author: ctjoreilly

src/aima/logic/fol/inference/FOLOTTERLikeTheoremProver.java

@@ -253,21 +253,21 @@ private Set<Clause> infer(Clause clause, Set<Clause> usable) {
 		// Remember to resolve with self
 		Set<Clause> resolvents = clause.binaryResolvents(clause);
 		for (Clause rc : resolvents) {
-			resultingClauses.addAll(rc.getFactors());
+			resultingClauses.add(rc);
 		}
 
 		// * resolve clause with each member of usable
 		for (Clause c : usable) {
 			resolvents = clause.binaryResolvents(c);
 			for (Clause rc : resolvents) {
-				resultingClauses.addAll(rc.getFactors());
+				resultingClauses.add(rc);
 			}
 
 			// if using paramodulation to handle equality
 			if (isUseParamodulation()) {
 				Set<Clause> paras = paramodulation.apply(clause, c, true);
 				for (Clause p : paras) {
-					resultingClauses.addAll(p.getFactors());
+					resultingClauses.add(p);
 				}
 			}
 		}
@@ -304,8 +304,12 @@ private void process(OTTERAnswerHandler ansHandler, Set<Clause> clauses,
 				// LightestClauseHeuristic to loop continuously
 				// on the same pair of objects.
 				if (!sos.contains(clause) && !usable.contains(clause)) {
-					sos.add(clause);
-					getLightestClauseHeuristic().addedClauseToSOS(clause);
+					for (Clause ac : clause.getFactors()) {
+						if (!sos.contains(ac) && !usable.contains(ac)) {
+							sos.add(ac);
+							getLightestClauseHeuristic().addedClauseToSOS(ac);
+						}
+					}
 				}
 
 				// * if clause has one literal then look for unit refutation

src/aima/logic/fol/inference/otter/defaultimpl/DefaultLightestClauseHeuristic.java

@@ -5,6 +5,8 @@
 import java.util.Comparator;
 import java.util.List;
 import java.util.Set;
+import java.util.SortedSet;
+import java.util.TreeSet;
 
 import aima.logic.fol.inference.otter.LightestClauseHeuristic;
 import aima.logic.fol.kb.data.Clause;
@@ -15,8 +17,8 @@
  */
 public class DefaultLightestClauseHeuristic implements LightestClauseHeuristic {
 
-	private List<Clause> sos = new ArrayList<Clause>();
-	private LightestClauseSorter lightestClauseSorter = new LightestClauseSorter();
+	private LightestClauseSorter c = new LightestClauseSorter();
+	private SortedSet<Clause> sos = new TreeSet<Clause>(c);
 
 	public DefaultLightestClauseHeuristic() {
 
@@ -28,7 +30,7 @@ public Clause getLightestClause() {
 		Clause lightest = null;
 
 		if (sos.size() > 0) {
-			lightest = sos.get(0);
+			lightest = sos.first();
 		}
 
 		return lightest;
@@ -37,12 +39,10 @@ public Clause getLightestClause() {
 	public void initialSOS(Set<Clause> clauses) {
 		sos.clear();
 		sos.addAll(clauses);
-		Collections.sort(sos, lightestClauseSorter);
 	}
 
 	public void addedClauseToSOS(Clause clause) {
 		sos.add(clause);
-		Collections.sort(sos, lightestClauseSorter);
 	}
 
 	public void removedClauseFromSOS(Clause clause) {
@@ -55,8 +55,18 @@ public void removedClauseFromSOS(Clause clause) {
 
 class LightestClauseSorter implements Comparator<Clause> {
 	public int compare(Clause c1, Clause c2) {
+		if (c1 == c2) {
+			return 0;
+		}
 		int c1Val = c1.getNumberLiterals();
 		int c2Val = c2.getNumberLiterals();
-		return (c1Val < c2Val ? -1 : (c1Val == c2Val ? 0 : 1));
+		return (c1Val < c2Val ? -1 : (c1Val == c2Val ? (compareEqualityIdentities(c1, c2)) : 1));
 	}
-}
+	
+	private int compareEqualityIdentities(Clause c1, Clause c2) {
+		int c1Len = c1.getEqualityIdentity().length();
+		int c2Len = c2.getEqualityIdentity().length();
+		
+		return (c1Len < c2Len ? -1 : (c1Len == c2Len ? c1.getEqualityIdentity().compareTo(c2.getEqualityIdentity()): 1));
+	}
+}

src/aima/logic/fol/kb/data/Clause.java

@@ -348,6 +348,10 @@ public boolean equals(Object othObj) {
 
 		return equalityIdentity.equals(othClause.equalityIdentity);
 	}
+	
+	public String getEqualityIdentity() {
+		return equalityIdentity;
+	}
 
 	//
 	// PRIVATE METHODS