Repaired a bug in the ChainingProcessor

app/src/main/java/charlie/terms/Binder.java

@@ -167,4 +167,9 @@ public boolean equals(Replaceable other) {
   public boolean equals(Variable other) {
     return other == this;
   }
+
+  /** Returns a hashcode that (uniquely) identifies this Binder */
+  public int hashCode() {
+    return 3 * _index + 1;
+  }
 }

app/src/main/java/charlie/terms/HigherMetaVar.java

@@ -99,6 +99,11 @@ public boolean equals(Replaceable other) {
     return other == this;
   }
 
+  /** Returns a hashcode that (uniquely) identifies this meta-variable */
+  public int hashCode() {
+    return 3 * _index + 2;
+  }
+
   public String toString() {
     return _name;
   }

app/src/main/java/charlie/terms/Var.java

@@ -172,4 +172,9 @@ public int compareTo(Replaceable other) {
     if (_index > other.queryIndex()) return 1;
     return queryType().toString().compareTo(other.queryType().toString());
   }
+
+  /** Returns a hashcode that (uniquely) identifies this Var */
+  public int hashCode() {
+    return 3 * _index;
+  }
 }

app/src/main/java/cora/Parameters.java

@@ -70,6 +70,7 @@ private TreeSet<String> disableableTechniques() {
     addTechnique(set, cora.termination.dependency_pairs.processors.graph.GraphProcessor.queryDisabledCode());
     addTechnique(set, cora.termination.dependency_pairs.processors.IntegerMappingProcessor.queryDisabledCode());
     addTechnique(set, cora.termination.dependency_pairs.processors.graph.ReachabilityProcessor.queryDisabledCode());
+    addTechnique(set, cora.termination.dependency_pairs.processors.ChainingProcessor.queryDisabledCode());
     addTechnique(set, cora.termination.dependency_pairs.processors.SplittingProcessor.queryDisabledCode());
     addTechnique(set, cora.termination.dependency_pairs.processors.SubtermProcessor.queryDisabledCode());
     addTechnique(set, cora.termination.dependency_pairs.processors.TheoryArgumentsProcessor.queryDisabledCode());

app/src/main/java/cora/termination/dependency_pairs/DP.java

@@ -15,20 +15,14 @@
 
 package cora.termination.dependency_pairs;
 
-import charlie.terms.Substitution;
-import charlie.terms.Term;
-import charlie.terms.TermFactory;
-import charlie.terms.TheoryFactory;
-import charlie.terms.Variable;
-import charlie.util.Renamer;
+import charlie.terms.*;
 
 import java.util.ArrayList;
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
 
 /**
- * Docu-guess (Carsten):
  * Dependency Pair for Logically Constrained Simply-typed Term Rewrite Systems
  * (LCSTRSs) as introduced in:
  *<p>
@@ -76,82 +70,69 @@ public DP(Term lhs, Term rhs, Term constraint) {
     this(lhs, rhs, constraint, constraint.vars().toSet());
   }
 
-  /**
-   * Creates a new DP of the form s ⇒ t | true {}, to be used for unconstrained rewriting.
-   */
+  /** Creates a new DP of the form s ⇒ t | true {}, to be used for unconstrained rewriting. */
   public DP(Term lhs, Term rhs) {
     this(lhs, rhs, TheoryFactory.createValue(true), Set.of());
   }
 
   /**
-   *
-   * @return a set of all variables occurring in this DP; may be modified
+   * @return a modifiable set of all variables occurring in this DP
    */
-  public Set<Variable> getAllVariables() {
-    Set<Variable> result = new LinkedHashSet<>();
-    for (Variable x : this.lhs.vars()) {
-      result.add(x);
-    }
-    for (Variable x : this.rhs.vars()) {
-      result.add(x);
-    }
-    for (Variable x : this.constraint.vars()) {
-      result.add(x);
-    }
-    result.addAll(this.lvars);
+  public LinkedHashSet<Variable> getAllVariables() {
+    LinkedHashSet<Variable> result = new LinkedHashSet<>();
+    for (Variable x : this.lhs.vars()) result.add(x);
+    for (Variable x : this.rhs.vars()) result.add(x);
+    for (Variable x : this.constraint.vars()) result.add(x);
     return result;
   }
 
   /**
-   *
-   * @param forbiddenVarNames variable names that must not occur in the result;
-   *                          will not be modified by this method
-   * @return a DP that is structurally equivalent to the present one
-   *  but does not use any of the names in forbiddenVarNames for its
-   *  variables
-   * @throws NullPointerException if forbiddenVarNames is null
+   * @return a DP that is structurally equivalent to the present one but uses fresh variables
    */
-  public DP getRenamed(Set<String> forbiddenVarNames) {
-    Renamer renamer = new Renamer();
-    renamer.addForbiddenNames(forbiddenVarNames);
+  public DP getRenamed() {
     Substitution subst = TermFactory.createEmptySubstitution();
     for (Variable x : getAllVariables()) {
-      extendSubstitution(subst, x, renamer);
+      subst.extend(x, TermFactory.createVar(x.queryName(), x.queryType()));
     }
     Term newLhs = this.lhs.substitute(subst);
     Term newRhs = this.rhs.substitute(subst);
     Term newConstraint = this.constraint.substitute(subst);
     Set<Variable> newTheoryVars = new LinkedHashSet<>();
     for (Variable x : this.lvars) {
-      newTheoryVars.add(subst.get(x).queryVariable());
+      Term y = subst.get(x);
+      if (y != null) newTheoryVars.add(y.queryVariable());
     }
     return new DP(newLhs, newRhs, newConstraint, newTheoryVars);
   }
 
-  private static void extendSubstitution(Substitution subst, Variable x, Renamer r) {
-    if (subst.get(x) == null) {
-      String newName = r.assignOrGetNewName(x.queryName());
-      subst.extend(x, TermFactory.createVar(newName, x.queryType()));
-    }
-  }
-
+  /**
+   * Default toString() functionality; deliberately ugly because printing to the user should always
+   * be done through an output module.
+   */
   @Override
   public String toString() {
+    return toString(new Renaming(Set.of()));
+  }
+
+  /** Better toString() functionality for a given Renaming */
+  public String toString(Renaming renaming) {
     StringBuilder builder = new StringBuilder();
-    builder.append(lhs.toString());
+    TermPrinter printer = new TermPrinter(Set.of());
+    printer.print(lhs, renaming, builder);
     builder.append(" => ");
-    builder.append(rhs.toString());
+    printer.print(rhs, renaming, builder);
     builder.append(" | ");
-    builder.append(constraint.toString());
+    printer.print(constraint, renaming, builder);
     builder.append(" {");
     boolean first = true;
     for (Variable x : lvars) {
       if (constraint.vars().contains(x)) continue;
       if (first) { first = false; builder.append(" "); }
       else builder.append(", ");
-      builder.append(x.toString());
+      printer.print(x, renaming, builder);
     }
     builder.append(" }");
     return builder.toString();
   }
 }
+

app/src/main/java/cora/termination/dependency_pairs/DPProofObject.java

@@ -314,16 +314,12 @@ private void describeUnknownDPP(OutputModule module, Problem problem, HashMap<Pr
   }
 
   /**
-   * This function handles the printing of a DP, by translating it into a Pair that the OutputModule
-   * knows how to print (but with good use of variables, and cleverly printing only those
-   * constraints and variables that we have to).
+   * This function handles the printing of a DP with a previously-fixed renaming for all its
+   * components, by translating it into a single Pair that the OutputModule knows how to print.
    */
-  private Pair<String,Object[]> makeDPObject(DP dp, OutputModule module) {
-    Renaming naming =
-      module.queryTermPrinter().generateUniqueNaming(dp.lhs(), dp.rhs(), dp.constraint());
-
+  private Pair<String,Object[]> makeDPObject(DP dp, Renaming naming) {
     StringBuilder ret = new StringBuilder("%a %{thickArrow} %a");
-    ArrayList<Object> args = new ArrayList<Object>();
+    ArrayList<Object> args = new ArrayList<Object>(4);
     args.add(new Pair<Term,Renaming>(dp.lhs(), naming));
     args.add(new Pair<Term,Renaming>(dp.rhs(), naming));
 
@@ -353,11 +349,27 @@ private Pair<String,Object[]> makeDPObject(DP dp, OutputModule module) {
     return new Pair<String,Object[]>(ret.toString(), args.toArray());
   }
 
+  /**
+   * This function handles the printing of a DP, by translating it into a Pair that the OutputModule
+   * knows how to print (but with good use of variables, and cleverly printing only those
+   * constraints and variables that we have to).
+   */
+  private Pair<String,Object[]> makeDPObject(DP dp, OutputModule module) {
+    Renaming naming =
+      module.queryTermPrinter().generateUniqueNaming(dp.lhs(), dp.rhs(), dp.constraint());
+    return makeDPObject(dp, naming);
+  }
+
   /** We use this adapted OutputModule for printing, so we can naturally handle dependency pairs. */
   private class OutputModuleWithDependencyPairs extends OutputModuleAdapter {
     public OutputModuleWithDependencyPairs(OutputModule m) { super(m); }
     protected Object alterObject(Object ob) {
       if (ob instanceof DP dp) return makeDPObject(dp, _module);
+      if (ob instanceof Pair p) {
+        if (p.fst() instanceof DP dp && p.snd() instanceof Renaming r) {
+          return makeDPObject(dp, r);
+        }
+      }
       return null;
     }
   }