Merge branch 'main' into weigl/abbrevmgr

KeYProject · Dec 3, 2023 · ee98653 · ee98653
2 parents d1c072a + c430e35
commit ee98653
Show file tree

Hide file tree

Showing 7 changed files with 57 additions and 18 deletions.
diff --git a/build.gradle b/build.gradle
@@ -21,7 +21,7 @@ plugins {
     // id "com.github.ben-manes.versions" version "0.39.0"
 
     // Code formatting
-    id "com.diffplug.spotless" version "6.22.0"
+    id "com.diffplug.spotless" version "6.23.0"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -72,7 +72,7 @@ subprojects {
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.9")
 
-        testImplementation("ch.qos.logback:logback-classic:1.4.11")
+        testImplementation("ch.qos.logback:logback-classic:1.4.12")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.1'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.1'
         testImplementation project(':key.util')

diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java
@@ -138,7 +138,6 @@ public interface SymbolIntroducer {
      * @return the S-Expression representing the translation
      */
     public SExpr translate(Term problem) {
-
         try {
             SMTHandler cached = handlerMap.get(problem.op());
             if (cached != null) {
@@ -211,11 +210,32 @@ private SExpr handleAsUnknownValue(Term problem) {
             return unknownValues.get(problem);
         }
         int number = unknownValues.size();
+        SExpr translation;
         SExpr abbr = new SExpr("unknown_" + number, Type.UNIVERSE);
-        SExpr e = new SExpr("declare-const", Type.UNIVERSE, abbr.toString(), "U");
-        addAxiom(e);
+        var freeVars = problem.freeVars();
+        if (freeVars.isEmpty()) {
+            // simple case: unknown value does not depend on anything else
+            SExpr e = new SExpr("declare-const", Type.UNIVERSE, abbr.toString(), "U");
+            addAxiom(e);
+            translation = abbr;
+        } else {
+            // unknown value depends on quantified variables
+            var names = freeVars.stream()
+                    .map(x -> new SExpr(LogicalVariableHandler.VAR_PREFIX + x.name().toString()))
+                    .toList();
+            var types = freeVars.stream()
+                    .map(x -> LogicalVariableHandler.makeVarDecl("", x.sort()).getChildren().get(0))
+                    .toList();
+            SExpr signature = new SExpr(types);
+            SExpr e = new SExpr("declare-fun", abbr, signature, new SExpr("U"));
+            addAxiom(e);
+            List<SExpr> list = new ArrayList<>();
+            list.add(abbr);
+            list.addAll(names);
+            translation = new SExpr("", Type.UNIVERSE, list);
+        }
         unknownValues.put(problem, abbr);
-        return abbr;
+        return translation;
     }
 
     /**

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
@@ -127,7 +127,7 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett
         sb.append(System.lineSeparator());
 
         sb.append("; --- Declarations\n");
-        extractSortDeclarations(sequent, services, master, sequentAsserts);
+        extractSortDeclarations(services, master);
         for (Writable decl : master.getDeclarations()) {
             decl.appendTo(sb);
             sb.append("\n");
@@ -179,16 +179,15 @@ public CharSequence translateProblem(Sequent sequent, Services services, SMTSett
         return sb;
     }
 
-    /*
+    /**
      * precompute the information on the required sources from the translation.
      */
-    private void extractSortDeclarations(Sequent sequent, Services services, MasterHandler master,
-            List<Term> sequentAsserts) {
+    private void extractSortDeclarations(Services services, MasterHandler master) {
         TypeManager tm = new TypeManager(services);
         tm.handle(master);
     }
 
-    /*
+    /**
      * extract a sequent into an SMT collection.
      *
      * The translation adds elements to the lists in the master handler on the way.
@@ -221,7 +220,7 @@ private static String readResource(String s) {
         }
     }
 
-    /*
+    /**
      * Turn a sequent to a collection of formulas. Antecedent positive, succedent negated.
      */
     private List<Term> getTermsFromSequent(Sequent seq, Services serv) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/QuantifierHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/QuantifierHandler.java
@@ -46,7 +46,6 @@ public boolean canHandle(Operator op) {
 
     @Override
     public SExpr handle(MasterHandler trans, Term term) throws SMTTranslationException {
-
         term = collectQuantifications(term);
 
         Set<Term> triggerTerms = new HashSet<>();

diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTHandler.java
@@ -26,8 +26,8 @@
  * SMT handlers are created using the default constructor without parameters They are always used
  * within the same proof, but possibly for several proof obligations.
  *
- * After creation, the {@link #init} method is called that
- * injects the {@link Services} object belonging to the proof.
+ * After creation, the {@link #init(MasterHandler, Services, Properties, String[])} method is called
+ * that injects the {@link Services} object belonging to the proof.
  *
  * During translation, an SMT handler can be asked via {@link #canHandle(Term)} if it can translate
  * a term into smt.
@@ -101,10 +101,10 @@ default Capability canHandle(Term term) {
 
     /**
      * Translate the given term into an SMT SExpression.
-     *
+     * <p>
      * This method will only be called if {@link #canHandle(Term)} returned true for the same term
      * argument.
-     *
+     * <p>
      * The translation may add to the set of assumptions and declarations using corresponding calls
      * to the {@link MasterHandler} that it receives.
      *

diff --git a/key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/unknownQuantified.props b/key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/unknownQuantified.props
@@ -0,0 +1,21 @@
+### KeY
+
+\functions {
+  Seq s1;
+  int maxx;
+}
+
+\problem {
+  \forall Seq s; (s = (seqDef{int u;}(0, s.length, any::seqGet(s, u))))
+  & seqLen(seqSub(s1, 0, maxx - 1)) = maxx - 1
+ ->
+  s1.length = maxx - 1
+}
+
+### contains.1
+
+(declare-fun unknown_0 (U) U)
+
+### expected
+
+fail
diff --git a/key.ui/build.gradle b/key.ui/build.gradle
@@ -23,7 +23,7 @@ dependencies {
     api 'com.miglayout:miglayout-swing:11.2'
 
     //logging implementation used by the slf4j
-    implementation 'ch.qos.logback:logback-classic:1.4.11'
+    implementation 'ch.qos.logback:logback-classic:1.4.12'
 
     api 'org.key-project:docking-frames-common:1.1.3p1'
     api 'org.key-project:docking-frames-core:1.1.3p1'