Restructured the way reduction pairs work

app/src/main/java/charlie/smt/Junction.java

@@ -33,7 +33,7 @@ abstract sealed class Junction extends Constraint permits Conjunction, Disjuncti
 
   Junction(List<Constraint> args) {
     _children = new ArrayList<Constraint>();
-    for (int i = 0; i < args.size(); i++) addChild(args.get(i));
+    for (Constraint c : args) addChild(c);
   }
 
   private void addChild(Constraint child) {

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

@@ -73,7 +73,7 @@ private TreeSet<String> disableableTechniques() {
     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());
-    addTechnique(set, cora.termination.reduction_pairs.Horpo.queryDisabledCode());
+    addTechnique(set, cora.termination.reduction_pairs.horpo.Horpo.queryDisabledCode());
     return set;
   }
 

app/src/main/java/cora/termination/TerminationHandler.java

@@ -25,7 +25,7 @@
 import cora.io.ProofObject;
 import cora.config.Settings;
 import cora.termination.transformation.CallByValueModifier;
-import cora.termination.reduction_pairs.Horpo;
+//import cora.termination.reduction_pairs.Horpo;
 import cora.termination.dependency_pairs.DPFramework;
 import cora.termination.dependency_pairs.FullDPFramework;
 
@@ -38,9 +38,12 @@ public static ProofObject proveTermination(TRS trs) {
     DPFramework framework = chooseFramework(trs, true);
     ProofObject po = framework.checkApplicable();
     if (po.queryAnswer() != ProofObject.Answer.YES) {
+      /*
       ProofObject ret = Horpo.proveTermination(trs);
       if (ret.queryAnswer() == ProofObject.Answer.YES) return wrap(ret, trs, "termination");
       else return wrap(po, ret, trs, "termination");
+      */
+      return wrap(po, trs, "termination");
 
     }
     return wrap(framework.run(), trs, "termination");

app/src/main/java/cora/termination/reduction_pairs/ArgumentFilter.java

@@ -0,0 +1,84 @@
+/**************************************************************************************************
+ Copyright 2024 Cynthia Kop
+
+ Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
+ in compliance with the License.
+ You may obtain a copy of the License at
+
+     http://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software distributed under the
+ License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ express or implied.
+ See the License for the specific language governing permissions and limitations under the License.
+ *************************************************************************************************/
+
+package cora.termination.reduction_pairs;
+
+import charlie.util.Pair;
+import charlie.terms.FunctionSymbol;
+import charlie.smt.BVar;
+import charlie.smt.SmtProblem;
+import charlie.smt.Valuation;
+
+import java.util.ArrayList;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import java.util.function.BiFunction;
+
+/**
+ * An instance of the Monotonicity class that represents an argument filtering: a function that
+ * regards a specific set of arguments, as described by an SMT problem.
+ */
+public class ArgumentFilter implements Monotonicity {
+  private SmtProblem _problem;
+  private TreeMap<FunctionSymbol,TreeMap<Integer,BVar>> _variables;
+
+  /**
+   * Creates an argument filtering that will use the given SMT problem to create its "regards"
+   * variables.  The problem will be stored in the ArgumentFiltering.
+   */
+  public ArgumentFilter(SmtProblem problem) {
+    _problem = problem;
+    _variables = new TreeMap<FunctionSymbol,TreeMap<Integer,BVar>>();
+  }
+
+  /** @return false */
+  public boolean stronglyMonotonic() {
+    return false;
+  }
+
+  /** This always returns the same BVar, which has been forced to evaluate to true. */
+  public BVar regards(FunctionSymbol f, int index) {
+    if (!_variables.containsKey(f)) _variables.put(f, new TreeMap<Integer,BVar>());
+    TreeMap<Integer,BVar> fmap = _variables.get(f);
+    if (fmap.containsKey(index)) return fmap.get(index);
+    BVar newvar = _problem.createBooleanVariable("regards{" + f.queryName() + "," + index + "}");
+    fmap.put(index, newvar);
+    return newvar;
+  }
+
+  /**
+   * For the given valuation, returns a non-smt-dependent function to evaluate which arguments were
+   * regarded.  Note that this will only include function symbols and arguments that we have
+   * actually been asked about.
+   */
+  public BiFunction<FunctionSymbol,Integer,Boolean> getRegardedArguments(Valuation valuation) {
+    TreeMap<FunctionSymbol,TreeSet<Integer>> ret = new TreeMap<FunctionSymbol,TreeSet<Integer>>();
+    for (FunctionSymbol f : _variables.keySet()) {
+      TreeMap<Integer,BVar> map = _variables.get(f);
+      TreeSet<Integer> tmp = null;
+      for (Integer i : map.keySet()) {
+        BVar x = map.get(i);
+        if (!valuation.queryAssignment(x)) continue;
+        if (tmp == null) {
+          tmp = new TreeSet<Integer>();
+          ret.put(f, tmp);
+        }
+        tmp.add(i);
+      }
+    }
+    return (f, i) -> ret.containsKey(f) && ret.get(f).contains(i);
+  }
+}
+