Formulas for which no triggers are generated may use equations from which to derive triggers (addresses issue #3972)

Author: unp1

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ReplacerOfQuanVariablesWithMetavariables.java

@@ -20,8 +20,7 @@
  * <code>allTerm</code> and create constant functions for all existential variables. The variables
  * with new created metavariables or constant functions are store to a map <code>mapQM</code>.
  */
-@Deprecated
-class ReplacerOfQuanVariablesWithMetavariables {
+public class ReplacerOfQuanVariablesWithMetavariables {
 
     private ReplacerOfQuanVariablesWithMetavariables() {}
 

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/EqualityConstraint.java

@@ -38,7 +38,6 @@
  * constraint would not be satisfiable (cycles, unification failed) the Constraint TOP of interface
  * Constraint is returned.
  */
-@Deprecated
 public class EqualityConstraint implements Constraint {
 
     /**

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Metavariable.java

@@ -13,7 +13,6 @@
 import org.key_project.logic.TerminalSyntaxElement;
 import org.key_project.logic.sort.Sort;
 
-@Deprecated
 public final class Metavariable extends JAbstractSortedOperator
         implements Comparable<Metavariable>, TerminalSyntaxElement, Named {
 

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/EqualityTheorySupport.java

@@ -3,12 +3,23 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.strategy.quantifierHeuristics.theory;
 
+
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.Equality;
 import de.uka.ilkd.key.logic.op.Junctor;
+import de.uka.ilkd.key.logic.op.LogicVariable;
+import de.uka.ilkd.key.proof.OpReplacer;
+import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Constraint;
+import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.EqualityConstraint;
+import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable;
 
 import org.key_project.logic.op.Operator;
 import org.key_project.logic.op.QuantifiableVariable;
@@ -103,4 +114,66 @@ public LiteralDecision decideFromAxiom(JTerm literal, JTerm axiom, Services serv
         }
         return LiteralDecision.UNKNOWN;
     }
+
+    @Override
+    public List<JTerm> fallbackTriggers(ClauseTriggers selection, Services services,
+            MetavariableFactory metavariableFactory) {
+        List<JTerm> fallbackTriggers = new ArrayList<>();
+        final ClauseAnalysis clauseInfo = selection.clause();
+
+        final Map<QuantifiableVariable, Metavariable> qv2mv = new LinkedHashMap<>();
+        final Map<Metavariable, QuantifiableVariable> mv2qv = new LinkedHashMap<>();
+        for (QuantifiableVariable var : clauseInfo.clause().freeVars()) {
+            final Metavariable mv = metavariableFactory.fresh(var.sort());
+            qv2mv.put(var, mv);
+            if (clauseInfo.universalVariables().contains(var)) {
+                mv2qv.put(mv, var);
+            }
+        }
+        final OpReplacer qv2mvReplacer =
+            new OpReplacer(qv2mv, services.getTermFactory());
+        final OpReplacer mv2qvReplacer =
+            new OpReplacer(mv2qv, services.getTermFactory());
+        for (JTerm lit : clauseInfo.literals()) {
+            if (lit.op() == Equality.EQUALS) {
+                fallbackTriggers.addAll(
+                    solveEquation(mv2qv.keySet(), qv2mvReplacer, mv2qvReplacer, lit, services));
+            }
+        }
+        return fallbackTriggers;
+    }
+
+    /// solves equation f(u) = f(g(v)) to u = g(MV_V)
+    /// @param mvs set of Metavariables used to replace **universal** bound variables
+    /// @param qv2mv OpReplacer to replace all free variables in lit by their meta variables
+    /// @param mv2qv OpReplacer to restore universal (not existential) bound variables
+    /// @param lit the JTerm representing an uncovered literal
+    /// @param services the Services class provides access to term construction and other services
+    /// @return list of solved equations that describe triggers
+    private List<JTerm> solveEquation(Set<Metavariable> mvs, OpReplacer qv2mv,
+            OpReplacer mv2qv, JTerm lit,
+            Services services) {
+        final TermBuilder tb = services.getTermBuilder();
+        final JTerm litWithMV = qv2mv.replace(lit);
+        final Constraint c =
+            EqualityConstraint.BOTTOM.unify(litWithMV.sub(0), litWithMV.sub(1), services);
+        List<JTerm> solvedEquations = new ArrayList<>();
+        if (c.isSatisfiable()) {
+            for (final Metavariable mv : mvs) {
+                final JTerm solution = c.getInstantiation(mv, services);
+                final Operator instOp = solution.op();
+                if (instOp instanceof LogicVariable ||
+                        instOp instanceof Metavariable) {
+                    // solutions that are a variable
+                    // and contain no function symbol do not
+                    // make useful triggers
+                    continue;
+                }
+                final JTerm solvedEquation = mv2qv.replace(tb.equals(tb.var(mv), solution));
+                solvedEquations.add(solvedEquation);
+                solvedEquations.add(tb.equals(solvedEquation.sub(1), solvedEquation.sub(0)));
+            }
+        }
+        return solvedEquations;
+    }
 }