diff --git a/nars_core_java/nars/inference/CompositionalRules.java b/nars_core_java/nars/inference/CompositionalRules.java
index 6574b4bd60e3dd2782e10f2751c026c494057d45..c91de3ed0401d054a40a0680f510e7f7f328851a 100644
--- a/nars_core_java/nars/inference/CompositionalRules.java
+++ b/nars_core_java/nars/inference/CompositionalRules.java
@@ -426,6 +426,9 @@ public final class CompositionalRules {
substitute.put(commonTerm2, new Variable("$varInd2"));
}
content = Implication.make(premise1, oldCompound, memory);
+ if (content == null) {
+ return;
+ }
content.applySubstitute(substitute);
if (premise1.equals(taskSentence.getContent())) {
truth = TruthFunctions.induction(belief.getTruth(), taskSentence.getTruth());
diff --git a/nars_core_java/nars/inference/LocalRules.java b/nars_core_java/nars/inference/LocalRules.java
index 374ae1c9847e7274aec6b429f2b5e4f23940be18..f53e1aacdd44b26bdbe5ded68887ec9d6993a84d 100644
--- a/nars_core_java/nars/inference/LocalRules.java
+++ b/nars_core_java/nars/inference/LocalRules.java
@@ -110,8 +110,8 @@ public class LocalRules {
Variable.unify(Symbols.VAR_INDEPENDENT, content, problem.cloneContent());
belief = (Sentence) belief.clone();
belief.setContent(content);
- Stamp st = new Stamp(memory.currentBelief.getStamp(), memory.getTime());
- st.addToChain(memory.currentBelief.getContent());
+ Stamp st = new Stamp(belief.getStamp(), memory.getTime());
+ st.addToChain(belief.getContent());
belief.setStamp(st);
}
task.setBestSolution(belief);
diff --git a/nars_core_java/nars/language/CompoundTerm.java b/nars_core_java/nars/language/CompoundTerm.java
index 3cf6a55fbb609dbdca947bfba4a3c20df189c4dc..46ff0af416cdd9fa0b08bb052e263c51b650e3dc 100644
--- a/nars_core_java/nars/language/CompoundTerm.java
+++ b/nars_core_java/nars/language/CompoundTerm.java
@@ -645,8 +645,11 @@ public abstract class CompoundTerm extends Term {
Term t1, t2;
for (int i = 0; i < size(); i++) {
t1 = componentAt(i);
- t2 = subs.get(t1);
- if (t2 != null) {
+ if (subs.containsKey(t1)) {
+ t2 = subs.get(t1);
+ while (subs.containsKey(t2)) {
+ t2 = subs.get(t2);
+ }
components.set(i, (Term) t2.clone());
} else if (t1 instanceof CompoundTerm) {
((CompoundTerm) t1).applySubstitute(subs);
diff --git a/nars_core_java/nars/language/Variable.java b/nars_core_java/nars/language/Variable.java
index b8284f7d3727380d4427415818f27275279563b8..d5effb52ca08b140dd8600b9d0143abecce48407 100644
--- a/nars_core_java/nars/language/Variable.java
+++ b/nars_core_java/nars/language/Variable.java
@@ -149,13 +149,15 @@ public class Variable extends Term {
HashMap<Term, Term> map2 = new HashMap<>();
boolean hasSubs = findSubstitute(type, t1, t2, map1, map2); // find substitution
if (hasSubs) {
- renameVar(map1, compound1, "-1");
- renameVar(map2, compound2, "-2");
+// renameVar(map1, compound1, "-1");
+// renameVar(map2, compound2, "-2");
if (!map1.isEmpty()) {
((CompoundTerm) compound1).applySubstitute(map1);
+ ((CompoundTerm) compound1).renameVariables();
}
if (!map2.isEmpty()) {
((CompoundTerm) compound2).applySubstitute(map2);
+ ((CompoundTerm) compound2).renameVariables();
}
}
return hasSubs;
@@ -175,52 +177,46 @@ public class Variable extends Term {
private static boolean findSubstitute(char type, Term term1, Term term2,
HashMap<Term, Term> map1, HashMap<Term, Term> map2) {
Term t;
- if (term1 instanceof Variable) {
+ if ((term1 instanceof Variable) && (((Variable) term1).getType() == type)) {
Variable var1 = (Variable) term1;
t = map1.get(var1);
if (t != null) { // already mapped
return findSubstitute(type, t, term2, map1, map2);
} else { // not mapped yet
- if (var1.getType() == type) {
- if ((term2 instanceof Variable) && (((Variable) term2).getType() == type)) {
- Variable var = new Variable(var1.getName() + term2.getName());
- map1.put(var1, var); // unify
- map2.put(term2, var); // unify
- } else {
- map1.put(var1, term2); // elimination
+ if ((term2 instanceof Variable) && (((Variable) term2).getType() == type)) {
+ Variable CommonVar = makeCommonVariable(term1, term2);
+ map1.put(var1, CommonVar); // unify
+ map2.put(term2, CommonVar); // unify
+ } else {
+ map1.put(var1, term2); // elimination
+ if (isCommonVariable(var1)) {
+ map2.put(var1, term2);
}
- } else { // different type
-// map1.put(var1, new Variable(var1.getName() + "-1")); // rename
- return false;
}
return true;
}
- }
- if (term2 instanceof Variable) {
+ } else if ((term2 instanceof Variable) && (((Variable) term2).getType() == type)) {
Variable var2 = (Variable) term2;
t = map2.get(var2);
if (t != null) { // already mapped
return findSubstitute(type, term1, t, map1, map2);
} else { // not mapped yet
- if (var2.getType() == type) {
- map2.put(var2, term1); // elimination
- } else {
-// map2.put(var2, new Variable(var2.getName() + "-2")); // rename
- return false;
+ map2.put(var2, term1); // elimination
+ if (isCommonVariable(var2)) {
+ map1.put(var2, term1);
}
return true;
}
- }
- if ((term1 instanceof CompoundTerm) && term1.getClass().equals(term2.getClass())) {
+ } else if ((term1 instanceof CompoundTerm) && term1.getClass().equals(term2.getClass())) {
CompoundTerm cTerm1 = (CompoundTerm) term1;
CompoundTerm cTerm2 = (CompoundTerm) term2;
if (cTerm1.size() != (cTerm2).size()) {
return false;
}
- if ((cTerm1 instanceof ImageExt) && (((ImageExt)cTerm1).getRelationIndex() != ((ImageExt)cTerm2).getRelationIndex())) {
+ if ((cTerm1 instanceof ImageExt) && (((ImageExt) cTerm1).getRelationIndex() != ((ImageExt) cTerm2).getRelationIndex())) {
return false;
}
- if ((cTerm1 instanceof ImageInt) && (((ImageInt)cTerm1).getRelationIndex() != ((ImageInt)cTerm2).getRelationIndex())) {
+ if ((cTerm1 instanceof ImageInt) && (((ImageInt) cTerm1).getRelationIndex() != ((ImageInt) cTerm2).getRelationIndex())) {
return false;
}
for (int i = 0; i < cTerm1.size(); i++) { // assuming matching order, to be refined in the future
@@ -236,6 +232,15 @@ public class Variable extends Term {
return term1.equals(term2); // for atomic constant terms
}
+ private static Variable makeCommonVariable(Term v1, Term v2) {
+ return new Variable(v1.getName() + v2.getName() + '$');
+ }
+
+ private static boolean isCommonVariable(Variable v) {
+ String s = v.getName();
+ return s.charAt(s.length() - 1) == '$';
+ }
+
/**
* Check if two terms can be unified
*
@@ -250,23 +255,24 @@ public class Variable extends Term {
/**
* Rename the variables to prepare for unification of two terms
+ *
* @param map The substitution so far
- * @param term The term to be processed
- * @param suffix The suffix that distinguish the variables in one premise from those from the other
+ * @param term The term to be processed
+ * @param suffix The suffix that distinguish the variables in one premise
+ * from those from the other
*/
- private static void renameVar(HashMap<Term, Term> map, Term term, String suffix) {
- if (term instanceof Variable) {
- Term t = map.get(term);
- if (t == null) { // new mapped yet
- map.put(term, new Variable(term.getName() + suffix)); // rename
- }
- } else if (term instanceof CompoundTerm) {
- for (Term t : ((CompoundTerm) term).components) { // assuming matching order, to be refined in the future
- renameVar(map, t, suffix);
- }
- }
- }
-
+// private static void renameVar(HashMap<Term, Term> map, Term term, String suffix) {
+// if (term instanceof Variable) {
+// Term t = map.get(term);
+// if (t == null) { // new mapped yet
+// map.put(term, new Variable(term.getName() + suffix)); // rename
+// }
+// } else if (term instanceof CompoundTerm) {
+// for (Term t : ((CompoundTerm) term).components) { // assuming matching order, to be refined in the future
+// renameVar(map, t, suffix);
+// }
+// }
+// }
/**
* variable terms are listed first alphabetically
*