- fixed subtle defect in Model Elimination inference algorithm.

ctjoreilly · ctjoreilly · commit 8b8eb41f2c51 · 2009-03-21T03:06:48.000Z
- cleaned up some unnecessary API calls that were impacting performance.
diff --git a/src/aima/logic/fol/StandardizeApart.java b/src/aima/logic/fol/StandardizeApart.java
@@ -88,7 +88,7 @@ public Clause standardizeApart(Clause clause,
 				literals.add(substVisitor.subst(renameSubstitution, l));
 			}
 			Clause renamed = new Clause(literals);
-			renamed.setProofStep(new ProofStepRenaming(renamed.toString(),
+			renamed.setProofStep(new ProofStepRenaming(renamed,
 					clause.getProofStep()));
 			return renamed;
 		}
@@ -125,7 +125,7 @@ public Chain standardizeApart(Chain chain,
 
 			Chain renamed = new Chain(lits);
 
-			renamed.setProofStep(new ProofStepRenaming(renamed.toString(),
+			renamed.setProofStep(new ProofStepRenaming(renamed,
 					chain.getProofStep()));
 
 			return renamed;
diff --git a/src/aima/logic/fol/SubstVisitor.java b/src/aima/logic/fol/SubstVisitor.java
@@ -39,15 +39,15 @@ public SubstVisitor() {
 	 * 
 	 */
 	public Sentence subst(Map<Variable, Term> theta, Sentence aSentence) {
-		return (Sentence) ((Sentence) aSentence.accept(this, theta)).copy();
+		return (Sentence) aSentence.accept(this, theta);
 	}
 	
 	public Term subst(Map<Variable, Term> theta, Term aTerm) {
-		return (Term) ((Term) aTerm.accept(this, theta)).copy();
+		return (Term) aTerm.accept(this, theta);
 	}
 	
 	public Function subst(Map<Variable, Term> theta, Function aFunction) {
-		return (Function) ((Function) aFunction.accept(this, theta)).copy();
+		return (Function) aFunction.accept(this, theta);
 	}
 	
 	public Literal subst(Map<Variable, Term> theta, Literal aLiteral) {
@@ -63,7 +63,7 @@ public Object visitVariable(Variable variable, Object arg) {
 		if (substitution.containsKey(variable)) {
 			return substitution.get(variable).copy();
 		}
-		return variable;
+		return variable.copy();
 	}
 
 	@SuppressWarnings("unchecked")
@@ -83,12 +83,12 @@ public Object visitQuantifiedSentence(QuantifiedSentence sentence,
 				if (st instanceof Variable) {
 					// Only if it is a variable to I replace it, otherwise
 					// I drop it.
-					variables.add((Variable) st);
+					variables.add((Variable) st.copy());
 				}
 			} else {
 				// No substitution for the quantified variable, so
 				// keep it.
-				variables.add(v);
+				variables.add(v.copy());
 			}
 		}
 
diff --git a/src/aima/logic/fol/inference/FOLModelElimination.java b/src/aima/logic/fol/inference/FOLModelElimination.java
@@ -178,7 +178,7 @@ private void recursiveDLS(int maxDepth,
 				int noNextFarParents = indexedFarParents
 						.getNumberFarParents(nextNearParent);
 				// Add to indexed far parents
-				indexedFarParents.addToIndex(nextNearParent);
+				nextNearParent = indexedFarParents.addToIndex(nextNearParent);
 				
 				// Check the next level
 				recursiveDLS(maxDepth, currentDepth + 1, nextNearParent,
@@ -279,7 +279,7 @@ public AnswerHandler(FOLKnowledgeBase kb, Sentence aQuery,
 			}
 			
 			for (Chain s : sos) {
-				s.setProofStep(new ProofStepGoal(s.toString()));
+				s.setProofStep(new ProofStepGoal(s));
 			}
 		}
 		
@@ -521,7 +521,8 @@ public Chain attemptReduction(Chain nearParent,
 		return nnpc;
 	}
 	
-	public void addToIndex(Chain c) {
+	public Chain addToIndex(Chain c) {
+		Chain added = null;
 		Literal head = c.getHead();
 		if (null != head) {
 			Map<String, List<Chain>> toAddTo = null;
@@ -538,8 +539,10 @@ public void addToIndex(Chain c) {
 				toAddTo.put(key, farParents);
 			}
 			// Ensure is standardized apart when added.
-			farParents.add(standardizeApart.standardizeApart(c, _saIndexical));
+			added = standardizeApart.standardizeApart(c, _saIndexical);
+			farParents.add(added);
 		}
+		return added;
 	}
 	
 	public String toString() {
diff --git a/src/aima/logic/fol/inference/FOLOTTERLikeTheoremProver.java b/src/aima/logic/fol/inference/FOLOTTERLikeTheoremProver.java
@@ -189,7 +189,7 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
 					notAlpha, answerLiteral.getAtomicSentence());
 			for (Clause c : KB.convertToClauses(notAlphaWithAnswer)) {
 				c = KB.standardizeApart(c);
-				c.setProofStep(new ProofStepGoal(c.toString()));
+				c.setProofStep(new ProofStepGoal(c));
 				c.setStandardizedApartCheckNotRequired();
 				sos.addAll(c.getFactors());
 			}
@@ -198,7 +198,7 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
 		} else {
 			for (Clause c : KB.convertToClauses(notAlpha)) {
 				c = KB.standardizeApart(c);
-				c.setProofStep(new ProofStepGoal(c.toString()));
+				c.setProofStep(new ProofStepGoal(c));
 				c.setStandardizedApartCheckNotRequired();
 				sos.addAll(c.getFactors());
 			}
diff --git a/src/aima/logic/fol/inference/FOLTFMResolution.java b/src/aima/logic/fol/inference/FOLTFMResolution.java
@@ -97,7 +97,7 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
 					notAlpha, answerLiteral.getAtomicSentence());
 			for (Clause c : KB.convertToClauses(notAlphaWithAnswer)) {
 				c = KB.standardizeApart(c);
-				c.setProofStep(new ProofStepGoal(c.toString()));
+				c.setProofStep(new ProofStepGoal(c));
 				c.setStandardizedApartCheckNotRequired();
 				clauses.addAll(c.getFactors());
 			}
@@ -106,7 +106,7 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
 		} else {
 			for (Clause c : KB.convertToClauses(notAlpha)) {
 				c = KB.standardizeApart(c);
-				c.setProofStep(new ProofStepGoal(c.toString()));
+				c.setProofStep(new ProofStepGoal(c));
 				c.setStandardizedApartCheckNotRequired();
 				clauses.addAll(c.getFactors());
 			}
diff --git a/src/aima/logic/fol/inference/proof/ProofStepClauseClausifySentence.java b/src/aima/logic/fol/inference/proof/ProofStepClauseClausifySentence.java
@@ -18,7 +18,7 @@ public class ProofStepClauseClausifySentence extends AbstractProofStep {
 	public ProofStepClauseClausifySentence(Clause clausified,
 			Sentence origSentence) {
 		this.clausified = clausified;
-		this.predecessors.add(new ProofStepPremise(origSentence.toString()));
+		this.predecessors.add(new ProofStepPremise(origSentence));
 	}
 
 	//
diff --git a/src/aima/logic/fol/inference/proof/ProofStepGoal.java b/src/aima/logic/fol/inference/proof/ProofStepGoal.java
@@ -12,9 +12,9 @@ public class ProofStepGoal extends AbstractProofStep {
 	//
 	private static final List<ProofStep> _noPredecessors = new ArrayList<ProofStep>();
 	//
-	private String proof = "";
+	private Object proof = "";
 
-	public ProofStepGoal(String proof) {
+	public ProofStepGoal(Object proof) {
 		this.proof = proof;
 	}
 
diff --git a/src/aima/logic/fol/inference/proof/ProofStepPremise.java b/src/aima/logic/fol/inference/proof/ProofStepPremise.java
@@ -12,9 +12,9 @@ public class ProofStepPremise extends AbstractProofStep {
 	//
 	private static final List<ProofStep> _noPredecessors = new ArrayList<ProofStep>();
 	//
-	private String proof = "";
+	private Object proof = "";
 
-	public ProofStepPremise(String proof) {
+	public ProofStepPremise(Object proof) {
 		this.proof = proof;
 	}
 
diff --git a/src/aima/logic/fol/inference/proof/ProofStepRenaming.java b/src/aima/logic/fol/inference/proof/ProofStepRenaming.java
@@ -10,9 +10,9 @@
  */
 public class ProofStepRenaming extends AbstractProofStep {
 	private List<ProofStep> predecessors = new ArrayList<ProofStep>();	
-	private String proof = "";
+	private Object proof = "";
 
-	public ProofStepRenaming(String proof, ProofStep predecessor) {
+	public ProofStepRenaming(Object proof, ProofStep predecessor) {
 		this.proof = proof;
 		this.predecessors.add(predecessor);
 	}
diff --git a/src/aima/logic/fol/kb/data/Chain.java b/src/aima/logic/fol/kb/data/Chain.java
@@ -41,7 +41,7 @@ public Chain(Set<Literal> literals) {
 	public ProofStep getProofStep() {
 		if (null == proofStep) {
 			// Assume was a premise
-			proofStep = new ProofStepPremise(this.toString());
+			proofStep = new ProofStepPremise(this);
 		}
 		return proofStep;
 	}
diff --git a/src/aima/logic/fol/kb/data/Clause.java b/src/aima/logic/fol/kb/data/Clause.java
@@ -95,7 +95,7 @@ public Clause(List<Literal> lits1, List<Literal> lits2) {
 	public ProofStep getProofStep() {
 		if (null == proofStep) {
 			// Assume was a premise
-			proofStep = new ProofStepPremise(this.toString());
+			proofStep = new ProofStepPremise(this);
 		}
 		return proofStep;
 	}
diff --git a/src/aima/logic/fol/parsing/AbstractFOLVisitor.java b/src/aima/logic/fol/parsing/AbstractFOLVisitor.java
@@ -28,7 +28,7 @@ protected Sentence recreate(Object ast) {
 	}
 
 	public Object visitVariable(Variable variable, Object arg) {
-		return variable;
+		return variable.copy();
 	}
 
 	public Object visitQuantifiedSentence(QuantifiedSentence sentence,

Original file line number	Diff line number	Diff line change
`@@ -88,7 +88,7 @@ public Clause standardizeApart(Clause clause,`
`88`	`88`	`literals.add(substVisitor.subst(renameSubstitution, l));`
`89`	`89`	`}`
`90`	`90`	`Clause renamed = new Clause(literals);`
`91`		`- renamed.setProofStep(new ProofStepRenaming(renamed.toString(),`
	`91`	`+ renamed.setProofStep(new ProofStepRenaming(renamed,`
`92`	`92`	`clause.getProofStep()));`
`93`	`93`	`return renamed;`
`94`	`94`	`}`
`@@ -125,7 +125,7 @@ public Chain standardizeApart(Chain chain,`
`125`	`125`
`126`	`126`	`Chain renamed = new Chain(lits);`
`127`	`127`
`128`		`- renamed.setProofStep(new ProofStepRenaming(renamed.toString(),`
	`128`	`+ renamed.setProofStep(new ProofStepRenaming(renamed,`
`129`	`129`	`chain.getProofStep()));`
`130`	`130`
`131`	`131`	`return renamed;`
Original file line number	Diff line number	Diff line change
`@@ -39,15 +39,15 @@ public SubstVisitor() {`
`39`	`39`	`*`
`40`	`40`	`*/`
`41`	`41`	`public Sentence subst(Map<Variable, Term> theta, Sentence aSentence) {`
`42`		`- return (Sentence) ((Sentence) aSentence.accept(this, theta)).copy();`
	`42`	`+ return (Sentence) aSentence.accept(this, theta);`
`43`	`43`	`}`
`44`	`44`
`45`	`45`	`public Term subst(Map<Variable, Term> theta, Term aTerm) {`
`46`		`- return (Term) ((Term) aTerm.accept(this, theta)).copy();`
	`46`	`+ return (Term) aTerm.accept(this, theta);`
`47`	`47`	`}`
`48`	`48`
`49`	`49`	`public Function subst(Map<Variable, Term> theta, Function aFunction) {`
`50`		`- return (Function) ((Function) aFunction.accept(this, theta)).copy();`
	`50`	`+ return (Function) aFunction.accept(this, theta);`
`51`	`51`	`}`
`52`	`52`
`53`	`53`	`public Literal subst(Map<Variable, Term> theta, Literal aLiteral) {`
`@@ -63,7 +63,7 @@ public Object visitVariable(Variable variable, Object arg) {`
`63`	`63`	`if (substitution.containsKey(variable)) {`
`64`	`64`	`return substitution.get(variable).copy();`
`65`	`65`	`}`
`66`		`- return variable;`
	`66`	`+ return variable.copy();`
`67`	`67`	`}`
`68`	`68`
`69`	`69`	`@SuppressWarnings("unchecked")`
`@@ -83,12 +83,12 @@ public Object visitQuantifiedSentence(QuantifiedSentence sentence,`
`83`	`83`	`if (st instanceof Variable) {`
`84`	`84`	`// Only if it is a variable to I replace it, otherwise`
`85`	`85`	`// I drop it.`
`86`		`- variables.add((Variable) st);`
	`86`	`+ variables.add((Variable) st.copy());`
`87`	`87`	`}`
`88`	`88`	`} else {`
`89`	`89`	`// No substitution for the quantified variable, so`
`90`	`90`	`// keep it.`
`91`		`- variables.add(v);`
	`91`	`+ variables.add(v.copy());`
`92`	`92`	`}`
`93`	`93`	`}`
`94`	`94`
Original file line number	Diff line number	Diff line change
`@@ -178,7 +178,7 @@ private void recursiveDLS(int maxDepth,`
`178`	`178`	`int noNextFarParents = indexedFarParents`
`179`	`179`	`.getNumberFarParents(nextNearParent);`
`180`	`180`	`// Add to indexed far parents`
`181`		`- indexedFarParents.addToIndex(nextNearParent);`
	`181`	`+ nextNearParent = indexedFarParents.addToIndex(nextNearParent);`
`182`	`182`
`183`	`183`	`// Check the next level`
`184`	`184`	`recursiveDLS(maxDepth, currentDepth + 1, nextNearParent,`
`@@ -279,7 +279,7 @@ public AnswerHandler(FOLKnowledgeBase kb, Sentence aQuery,`
`279`	`279`	`}`
`280`	`280`
`281`	`281`	`for (Chain s : sos) {`
`282`		`- s.setProofStep(new ProofStepGoal(s.toString()));`
	`282`	`+ s.setProofStep(new ProofStepGoal(s));`
`283`	`283`	`}`
`284`	`284`	`}`
`285`	`285`
`@@ -521,7 +521,8 @@ public Chain attemptReduction(Chain nearParent,`
`521`	`521`	`return nnpc;`
`522`	`522`	`}`
`523`	`523`
`524`		`- public void addToIndex(Chain c) {`
	`524`	`+ public Chain addToIndex(Chain c) {`
	`525`	`+ Chain added = null;`
`525`	`526`	`Literal head = c.getHead();`
`526`	`527`	`if (null != head) {`
`527`	`528`	`Map<String, List<Chain>> toAddTo = null;`
`@@ -538,8 +539,10 @@ public void addToIndex(Chain c) {`
`538`	`539`	`toAddTo.put(key, farParents);`
`539`	`540`	`}`
`540`	`541`	`// Ensure is standardized apart when added.`
`541`		`- farParents.add(standardizeApart.standardizeApart(c, _saIndexical));`
	`542`	`+ added = standardizeApart.standardizeApart(c, _saIndexical);`
	`543`	`+ farParents.add(added);`
`542`	`544`	`}`
	`545`	`+ return added;`
`543`	`546`	`}`
`544`	`547`
`545`	`548`	`public String toString() {`
Original file line number	Diff line number	Diff line change
`@@ -18,7 +18,7 @@ public class ProofStepClauseClausifySentence extends AbstractProofStep {`
`18`	`18`	`public ProofStepClauseClausifySentence(Clause clausified,`
`19`	`19`	`Sentence origSentence) {`
`20`	`20`	`this.clausified = clausified;`
`21`		`- this.predecessors.add(new ProofStepPremise(origSentence.toString()));`
	`21`	`+ this.predecessors.add(new ProofStepPremise(origSentence));`
`22`	`22`	`}`
`23`	`23`
`24`	`24`	`//`
Original file line number	Diff line number	Diff line change
`@@ -41,7 +41,7 @@ public Chain(Set<Literal> literals) {`
`41`	`41`	`public ProofStep getProofStep() {`
`42`	`42`	`if (null == proofStep) {`
`43`	`43`	`// Assume was a premise`
`44`		`- proofStep = new ProofStepPremise(this.toString());`
	`44`	`+ proofStep = new ProofStepPremise(this);`
`45`	`45`	`}`
`46`	`46`	`return proofStep;`
`47`	`47`	`}`