From 5215831d65c3ac576f846b09daa49ee436245871 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 20 Feb 2025 10:03:15 +0100 Subject: [PATCH 1/6] first try for translating invariant taclets to SMT --- .../ilkd/key/smt/AbstractSMTTranslator.java | 7 +++-- .../de/uka/ilkd/key/smt/SMTObjTranslator.java | 6 ++-- .../ilkd/key/smt/SMTSolverImplementation.java | 4 +-- .../de/uka/ilkd/key/smt/SMTTranslator.java | 6 ++-- .../smt/newsmt2/ModularSMTLib2Translator.java | 28 +++++++++++++++++-- .../key/smt/newsmt2/SMTTacletTranslator.java | 1 + .../key/smt/newsmt2/MasterHandlerTest.java | 2 +- 7 files changed, 39 insertions(+), 15 deletions(-) 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..e0aca7b2fbe 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, - SMTSettings settings) throws IllegalFormulaException { + 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/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..a8fa7bb824e 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,7 @@ 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 +340,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..5475fc93d87 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..d3adbc773cc 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; @@ -108,8 +113,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 +121,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 +130,24 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett sb.append(preamble); sb.append(System.lineSeparator()); + // add invariant axioms + // TODO: static axioms, represents axioms, ... + Set set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps(); + var filtered = set.stream() + .filter(t -> t.taclet().name().toString().startsWith("Class_invariant_axiom_for_")) + .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); + master.addAxiom(SExprs.assertion(smt)); + } catch (SMTTranslationException e) { + throw new RuntimeException(e); + } + } + sb.append("; --- Declarations\n"); extractSortDeclarations(services, master); for (Writable decl : master.getDeclarations()) { 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..bdd6caade72 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 @@ -12,6 +12,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.FindTaclet; +import de.uka.ilkd.key.rule.NotFreeIn; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.smt.SMTTranslationException; import de.uka.ilkd.key.taclettranslation.DefaultTacletTranslator; 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); } From 30ed8b6b95c6d9599be8d68f7b10e0dd2ef93524 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 20 Feb 2025 10:51:53 +0100 Subject: [PATCH 2/6] named invariant taclet assertions, make VariableSVs translateable --- .../de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java | 2 ++ .../java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) 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 d3adbc773cc..78d3c563d47 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 @@ -142,6 +142,8 @@ public CharSequence translateProblem(Goal goal, Services services, SMTSettings s 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); 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 bdd6caade72..2803b30ab90 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 @@ -73,7 +73,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()); } From dfdcef1d8bf0dc031bf9ecba4b5ba866c040829d Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 20 Feb 2025 11:33:27 +0100 Subject: [PATCH 3/6] fix bug with unsat cores and named assertions for taclets --- .../src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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..3a31241be76 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 @@ -176,9 +176,11 @@ 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("L_")).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; } From a370f6cc3e91f345c9f2556188c61b240a823efe Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 20 Feb 2025 11:59:53 +0100 Subject: [PATCH 4/6] add other invariants and axioms as well --- .../smt/newsmt2/ModularSMTLib2Translator.java | 52 ++++++++++++------- 1 file changed, 34 insertions(+), 18 deletions(-) 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 78d3c563d47..f89f7c26b45 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 @@ -130,24 +130,19 @@ public CharSequence translateProblem(Goal goal, Services services, SMTSettings s sb.append(preamble); sb.append(System.lineSeparator()); - // add invariant axioms - // TODO: static axioms, represents axioms, ... - Set set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps(); - var filtered = set.stream() - .filter(t -> t.taclet().name().toString().startsWith("Class_invariant_axiom_for_")) - .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); - } + // TODO: check this list ... Represents axioms? + String[] axiomTacletPrefixes = { + "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? These contain skolem schema vars ... + }; + // add axioms for invariants, static invariants, represents axioms, ... + for (String prefix : axiomTacletPrefixes) { + addAxioms(prefix, goal, services, master); } sb.append("; --- Declarations\n"); @@ -203,6 +198,27 @@ public CharSequence translateProblem(Goal goal, Services services, SMTSettings s 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. */ From 78acf089c1ebce1e47c8349440104847deb62db0 Mon Sep 17 00:00:00 2001 From: BookWood Date: Thu, 20 Feb 2025 13:16:59 +0100 Subject: [PATCH 5/6] Remove quantifier-only translation of bound variables to enable translation for binding operators (bsum,etc) --- .../key/smt/newsmt2/SMTTacletTranslator.java | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) 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 2803b30ab90..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 @@ -12,7 +12,6 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.FindTaclet; -import de.uka.ilkd.key.rule.NotFreeIn; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.smt.SMTTranslationException; import de.uka.ilkd.key.taclettranslation.DefaultTacletTranslator; @@ -94,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); From 442abfe78e02f91fcbb652dc0e6e377dc1823e18 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 20 Feb 2025 14:19:34 +0100 Subject: [PATCH 6/6] a bit of cleanup --- .../ilkd/key/smt/AbstractSMTTranslator.java | 2 +- .../de/uka/ilkd/key/smt/SMTFocusResults.java | 6 +++- .../ilkd/key/smt/SMTSolverImplementation.java | 3 +- .../de/uka/ilkd/key/smt/SMTTranslator.java | 2 +- .../smt/newsmt2/ModularSMTLib2Translator.java | 31 ++++++++++--------- 5 files changed, 26 insertions(+), 18 deletions(-) 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 e0aca7b2fbe..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 @@ -178,7 +178,7 @@ public TacletSetTranslation getTacletSetTranslation() { @Override public final StringBuilder translateProblem(Goal goal, Services services, - SMTSettings settings) throws IllegalFormulaException { + SMTSettings settings) throws IllegalFormulaException { smtSettings = settings; Term problem = sequentToTerm(goal.sequent(), services); StringBuilder hb = translateTerm(problem, new ArrayList<>(), services); 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 3a31241be76..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; @@ -177,7 +178,9 @@ static Integer[] parseZ3Format(String lastLine) { String[] labels = lastLine.trim().split(" +"); // some labels (for non-sequent formulas) are not for the unsat core -> filter them - String[] filtered = Arrays.stream(labels).filter(s -> s.startsWith("L_")).toArray(String[]::new); + 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(filtered[i].substring(2)); @@ -203,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/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index a8fa7bb824e..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(problem.getGoal(), services, smtSettings).toString(); + problemString = + objTrans.translateProblem(problem.getGoal(), services, smtSettings).toString(); ModelExtractor transQuery = objTrans.getQuery(); getSocket().setQuery(transQuery); tacletTranslation = null; 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 5475fc93d87..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 @@ -17,7 +17,7 @@ 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 goal 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 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 f89f7c26b45..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 @@ -45,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. @@ -130,18 +143,8 @@ public CharSequence translateProblem(Goal goal, Services services, SMTSettings s sb.append(preamble); sb.append(System.lineSeparator()); - // TODO: check this list ... Represents axioms? - String[] axiomTacletPrefixes = { - "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? These contain skolem schema vars ... - }; // add axioms for invariants, static invariants, represents axioms, ... - for (String prefix : axiomTacletPrefixes) { + for (String prefix : AXIOM_TACLET_PREFIXES) { addAxioms(prefix, goal, services, master); } @@ -163,7 +166,7 @@ public CharSequence translateProblem(Goal goal, Services services, SMTSettings s 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); } @@ -202,8 +205,8 @@ public CharSequence translateProblem(Goal goal, Services services, SMTSettings s 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(); + .filter(t -> t.taclet().name().toString().startsWith(prefix)) + .toList(); for (NoPosTacletApp npta : filtered) { Taclet taclet = npta.taclet(); SMTTacletTranslator tacletTranslator = new SMTTacletTranslator(services);