Improve the SMT translation by translating axiom taclets (mostly for invariants)

key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java

@@ -12,6 +12,7 @@
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
+import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.taclettranslation.TacletFormula;
 import de.uka.ilkd.key.taclettranslation.assumptions.DefaultTacletSetTranslation;
@@ -176,10 +177,10 @@ public TacletSetTranslation getTacletSetTranslation() {
     }
 
     @Override
-    public final StringBuilder translateProblem(Sequent sequent, Services services,
+    public final StringBuilder translateProblem(Goal goal, Services services,
             SMTSettings settings) throws IllegalFormulaException {
         smtSettings = settings;
-        Term problem = sequentToTerm(sequent, services);
+        Term problem = sequentToTerm(goal.sequent(), services);
         StringBuilder hb = translateTerm(problem, new ArrayList<>(), services);
 
         // add one variable for each sort

key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.rule.PosTacletApp;
 import de.uka.ilkd.key.rule.TacletApp;
 import de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth;
+import de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
@@ -176,9 +177,13 @@ static Integer[] parseZ3Format(String lastLine) {
         lastLine = lastLine.substring(1, lastLine.length() - 1);
 
         String[] labels = lastLine.trim().split(" +");
-        Integer[] numbers = new Integer[labels.length];
+        // some labels (for non-sequent formulas) are not for the unsat core -> filter them
+        String[] filtered = Arrays.stream(labels)
+                .filter(s -> s.startsWith(ModularSMTLib2Translator.UNSAT_CORE_PREFIX))
+                .toArray(String[]::new);
+        Integer[] numbers = new Integer[filtered.length];
         for (int i = 0; i < numbers.length; i++) {
-            numbers[i] = Integer.parseInt(labels[i].substring(2));
+            numbers[i] = Integer.parseInt(filtered[i].substring(2));
         }
         return numbers;
     }
@@ -201,6 +206,7 @@ static Integer[] parseCVC5Format(String[] lines) {
             if (lines[i].equals("(")) {
                 Integer[] numbers = new Integer[lines.length - 2 - i];
                 for (int j = i + 1; j < lines.length - 1; j++) {
+                    // TODO: substring here is dangerous, should check for UNSAT_CORE_PREFIX ...
                     numbers[j - i - 1] = Integer.parseInt(lines[j].substring(2));
                 }
                 return numbers;

key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java

@@ -11,10 +11,10 @@
 import de.uka.ilkd.key.java.declaration.ClassDeclaration;
 import de.uka.ilkd.key.java.declaration.InterfaceDeclaration;
 import de.uka.ilkd.key.ldt.JavaDLTheory;
-import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
+import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.smt.hierarchy.SortNode;
 import de.uka.ilkd.key.smt.hierarchy.TypeHierarchy;
 import de.uka.ilkd.key.smt.lang.*;
@@ -428,11 +428,11 @@ private void initSMTSorts() {
     }
 
     @Override
-    public StringBuffer translateProblem(Sequent sequent, Services services, SMTSettings settings)
+    public StringBuffer translateProblem(Goal goal, Services services, SMTSettings settings)
             throws IllegalFormulaException {
         this.settings = settings;
         this.services = services;
-        Term problem = sequentToTerm(sequent, services);
+        Term problem = sequentToTerm(goal.sequent(), services);
         SMTFile file = translateProblem(problem);
         String s = file.toString();
         return new StringBuffer(s);

key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java

@@ -332,15 +332,16 @@ private String[] translateToCommand(Sequent sequent) throws IllegalFormulaExcept
 
             SMTObjTranslator objTrans =
                 new SMTObjTranslator(smtSettings, services, typeOfClassUnderTest);
-            problemString = objTrans.translateProblem(sequent, services, smtSettings).toString();
+            problemString =
+                objTrans.translateProblem(problem.getGoal(), services, smtSettings).toString();
             ModelExtractor transQuery = objTrans.getQuery();
             getSocket().setQuery(transQuery);
             tacletTranslation = null;
 
         } else {
             SMTTranslator trans = getType().createTranslator();
             problemString =
-                indent(trans.translateProblem(sequent, services, smtSettings).toString());
+                indent(trans.translateProblem(problem.getGoal(), services, smtSettings).toString());
             if (trans instanceof AbstractSMTTranslator) {
                 // Since taclet translation in the old form is no longer used,
                 // this will likely disappear.

key.core/src/main/java/de/uka/ilkd/key/smt/SMTTranslator.java

@@ -4,7 +4,7 @@
 package de.uka.ilkd.key.smt;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.proof.Goal;
 
 
 /**
@@ -17,12 +17,12 @@ public interface SMTTranslator {
      * Translates a problem into the given syntax. The only difference to
      * <code>translate(Term t, Services services)</code> is that assumptions will be added.
      *
-     * @param sequent the sequent to be translated.
+     * @param goal the sequent to be translated.
      * @param services
      * @return a representation of the term in the given syntax.
      * @throws IllegalFormulaException
      */
-    CharSequence translateProblem(Sequent sequent, Services services, SMTSettings settings)
+    CharSequence translateProblem(Goal goal, Services services, SMTSettings settings)
             throws IllegalFormulaException;
 
 }

key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java

@@ -10,13 +10,18 @@
 import java.util.Arrays;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.NoPosTacletApp;
+import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.smt.SMTSettings;
+import de.uka.ilkd.key.smt.SMTTranslationException;
 import de.uka.ilkd.key.smt.SMTTranslator;
 import de.uka.ilkd.key.smt.newsmt2.SExpr.Type;
 
@@ -40,6 +45,19 @@ public class ModularSMTLib2Translator implements SMTTranslator {
      */
     private static final Logger LOGGER = LoggerFactory.getLogger(ModularSMTLib2Translator.class);
 
+    // TODO: check this list ... Represents axioms?
+    private static final String[] AXIOM_TACLET_PREFIXES = {
+        "Class_invariant_axiom_for",
+        "Static_class_invariant_axiom_for",
+        "Definition_axiom_for_",
+        "Free_class_invariant_axiom_for_",
+        "Free_static_class_invariant_axiom_for_",
+        "Partial_inv_axiom_for_JML_class_invariant_",
+            // "Query_axiom_for_" // Do we need those (not translatable at the moment (SkolemSV))?
+    };
+
+    public static final String UNSAT_CORE_PREFIX = "L_";
+
     /**
      * Handler option. If provided, the translator will label translations of sequent formulas such
      * that {@link de.uka.ilkd.key.smt.SMTFocusResults} can interpret the unsat core.
@@ -108,16 +126,15 @@ public ModularSMTLib2Translator() {
     }
 
     @Override
-    public CharSequence translateProblem(Sequent sequent, Services services, SMTSettings settings) {
-
+    public CharSequence translateProblem(Goal goal, Services services, SMTSettings settings) {
         MasterHandler master;
         try {
             master = new MasterHandler(services, settings, handlerNames, handlerOptions);
         } catch (IOException ex) {
             throw new RuntimeException(ex);
         }
 
-        List<Term> sequentAsserts = getTermsFromSequent(sequent, services);
+        List<Term> sequentAsserts = getTermsFromSequent(goal.sequent(), services);
         List<SExpr> sequentSMTAsserts = makeSMTAsserts(master, sequentAsserts);
 
         StringBuilder sb = new StringBuilder();
@@ -126,6 +143,11 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett
         sb.append(preamble);
         sb.append(System.lineSeparator());
 
+        // add axioms for invariants, static invariants, represents axioms, ...
+        for (String prefix : AXIOM_TACLET_PREFIXES) {
+            addAxioms(prefix, goal, services, master);
+        }
+
         sb.append("; --- Declarations\n");
         extractSortDeclarations(services, master);
         for (Writable decl : master.getDeclarations()) {
@@ -144,7 +166,7 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett
         int i = 1;
         for (SExpr ass : sequentSMTAsserts) {
             if (getUnsatCore) {
-                String label = "L_" + i;
+                String label = UNSAT_CORE_PREFIX + i;
                 i++;
                 ass = SExprs.named(ass, label);
             }
@@ -179,6 +201,27 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett
         return sb;
     }
 
+    // Adds all taclets that start with the given prefix as axioms to the MasterHandler.
+    private void addAxioms(String prefix, Goal goal, Services services, MasterHandler master) {
+        Set<NoPosTacletApp> set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps();
+        List<NoPosTacletApp> filtered = set.stream()
+                .filter(t -> t.taclet().name().toString().startsWith(prefix))
+                .toList();
+        for (NoPosTacletApp npta : filtered) {
+            Taclet taclet = npta.taclet();
+            SMTTacletTranslator tacletTranslator = new SMTTacletTranslator(services);
+            try {
+                Term formula = tacletTranslator.translate(taclet);
+                SExpr smt = master.translate(formula);
+                // we name assertions just for the user, so that it is easier to find them
+                smt = SExprs.named(smt, taclet.name().toString());
+                master.addAxiom(SExprs.assertion(smt));
+            } catch (SMTTranslationException e) {
+                throw new RuntimeException(e);
+            }
+        }
+    }
+
     /**
      * precompute the information on the required sources from the translation.
      */

key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java

@@ -72,7 +72,7 @@ private Term variablify(Term term, Map<OperatorSV, LogicVariable> variables)
 
         Operator op = term.op();
         if (op instanceof OperatorSV sv) {
-            if (!(sv instanceof TermSV || sv instanceof FormulaSV)) {
+            if (!(sv instanceof TermSV || sv instanceof FormulaSV || sv instanceof VariableSV)) {
                 throw new SMTTranslationException("Only a few schema variables can be translated. "
                     + "This one cannot. Type " + sv.getClass());
             }
@@ -93,18 +93,20 @@ private Term variablify(Term term, Map<OperatorSV, LogicVariable> variables)
         }
 
         List<QuantifiableVariable> qvars = new ArrayList<>();
-        if (op instanceof Quantifier) {
-            for (QuantifiableVariable boundVar : term.boundVars()) {
-                if (boundVar instanceof OperatorSV sv) {
-                    LogicVariable lv =
-                        variables.computeIfAbsent(sv, x -> new LogicVariable(x.name(), x.sort()));
-                    qvars.add(lv);
-                    changes = true;
-                } else {
-                    qvars.add(boundVar);
-                }
+        // Probably works for binding operators other than Quantifier, such as bsum. It would be
+        // desirable to not create incorrect terms here.
+        // if (op instanceof Quantifier) {
+        for (QuantifiableVariable boundVar : term.boundVars()) {
+            if (boundVar instanceof OperatorSV sv) {
+                LogicVariable lv =
+                    variables.computeIfAbsent(sv, x -> new LogicVariable(x.name(), x.sort()));
+                qvars.add(lv);
+                changes = true;
+            } else {
+                qvars.add(boundVar);
             }
         }
+        // }
 
         if (changes) {
             var bvars = new ImmutableArray<>(qvars);

key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java

@@ -152,7 +152,7 @@ public record TestData(String name, Path path, LineProperties props, String tran
 
                 ModularSMTLib2Translator translator = new ModularSMTLib2Translator();
                 var translation =
-                        translator.translateProblem(sequent, env.getServices(), settings).toString();
+                        translator.translateProblem(proof.getOpenGoal(proof.root()), env.getServices(), settings).toString();
                 return new TestData(name, path, props, translation);
             }