diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java index 8c69ce9973b..89932b8637d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java +++ b/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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java index 4a20c0867c4..c678fc9b81d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java +++ b/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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java index c4deeec5e98..edfbf27771b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index cf920273d82..7bd4ad3aa06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java @@ -332,7 +332,8 @@ 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; @@ -340,7 +341,7 @@ private String[] translateToCommand(Sequent sequent) throws IllegalFormulaExcept } 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. diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTTranslator.java index f0add2519af..31ec4737145 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTTranslator.java +++ b/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 * translate(Term t, Services services) 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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java index fc459866dd8..b08bc04dbba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java +++ b/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,8 +126,7 @@ 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); @@ -117,7 +134,7 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett throw new RuntimeException(ex); } - List sequentAsserts = getTermsFromSequent(sequent, services); + List sequentAsserts = getTermsFromSequent(goal.sequent(), services); List 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 set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps(); + List 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. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java index d2c6db2cdbc..c5bf2259a12 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java @@ -72,7 +72,7 @@ private Term variablify(Term term, Map 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 variables) } List 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); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java index bdd9db8c2fa..14b9bf5ce37 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java +++ b/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); }