Allow true in more JML expressions (#3664)

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java

@@ -90,6 +90,21 @@ public SpecMathMode replaceSpecMathMode(SpecMathMode specMathMode) {
         return overloadedFunctionHandler.replaceSpecMathMode(specMathMode);
     }
 
+    /**
+     * Ensure that <code>term</code> is a boolean term. If it is a formula, convert it to a boolean
+     * term.
+     */
+    public JTerm ensureTerm(JTerm term) {
+        if (term.sort() == JavaDLTheory.FORMULA) {
+            // bugfix (CS): t.getTerm() delivers a formula instead of a
+            // boolean term; obviously the original boolean terms are
+            // converted to formulas somewhere else; however, we need
+            // boolean terms instead of formulas here
+            return tb.convertToBoolean(term);
+        }
+        return term;
+    }
+
     // region reach
     public SLExpression reach(JTerm t, SLExpression e1, SLExpression e2, SLExpression e3) {
         final LogicVariable stepsLV = e3 == null
@@ -860,14 +875,7 @@ public SLExpression createSeqDef(SLExpression a, SLExpression b, SLExpression t,
         }
         QuantifiableVariable qv = declVars.head();
         JTerm tt = t.getTerm();
-        if (tt.sort() == JavaDLTheory.FORMULA) {
-            // bugfix (CS): t.getTerm() delivers a formula instead of a
-            // boolean term; obviously the original boolean terms are
-            // converted to formulas somewhere else; however, we need
-            // boolean terms instead of formulas here
-            tt = tb.convertToBoolean(t.getTerm());
-        }
-        JTerm resultTerm = tb.seqDef(qv, a.getTerm(), b.getTerm(), tt);
+        JTerm resultTerm = tb.seqDef(qv, a.getTerm(), b.getTerm(), ensureTerm(tt));
         final KeYJavaType seqtype = services.getJavaInfo().getPrimitiveKeYJavaType("\\seq");
         return new SLExpression(resultTerm, seqtype);
     }
@@ -973,7 +981,7 @@ public SLExpression seqConst(ImmutableList<SLExpression> exprList) {
         ImmutableList<JTerm> terms = ImmutableSLList.nil();
         for (SLExpression expr : exprList) {
             if (expr.isTerm()) {
-                JTerm t = expr.getTerm();
+                JTerm t = ensureTerm(expr.getTerm());
                 terms = terms.append(t);
             } else {
                 throw exc.createException0("Not a term: " + expr);
@@ -983,10 +991,14 @@ public SLExpression seqConst(ImmutableList<SLExpression> exprList) {
         return new SLExpression(tb.seq(terms), seqtype);
     }
 
+    public SLExpression seqUpd(JTerm seq, JTerm index, JTerm value) {
+        return new SLExpression(tb.seqUpd(seq, index, ensureTerm(value)));
+    }
+
     public SLExpression createIndexOf(JTerm seq, JTerm elem) {
         final KeYJavaType inttype =
             services.getJavaInfo().getPrimitiveKeYJavaType(PrimitiveType.JAVA_BIGINT);
-        return new SLExpression(tb.indexOf(seq, elem), inttype);
+        return new SLExpression(tb.indexOf(seq, ensureTerm(elem)), inttype);
     }
 
     public @NonNull JTerm createReturns(@Nullable JTerm term) {

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

@@ -1662,11 +1662,9 @@ public Object visitSequenceReplace(JmlParser.SequenceReplaceContext ctx) {
         SLExpression e2 = accept(ctx.expression(1));
         SLExpression e3 = accept(ctx.expression(2));
         // short for "e1[0..e2-1]+e3+e1[e2+1..e1.length-1]"
-        final JTerm minusOne = tb.zTerm("-1");
         assert e2 != null;
         assert e1 != null;
-        JTerm updated = tb.seqUpd(e1.getTerm(), e2.getTerm(), e3.getTerm());
-        return new SLExpression(updated);
+        return termFactory.seqUpd(e1.getTerm(), e2.getTerm(), e3.getTerm());
     }
 
     @Override

key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exprs.txt

@@ -14,3 +14,10 @@ this
 1.f + 2.d
 \seq()
 \locset()
+\seq_upd(\seq(), 2, true) // There were issues with true in expressions ... #3660
+\seq(true)
+\seq(true, true)
+(\seq_def int i; 0; 10; true)
+\seq_indexOf(\seq(true), true)
+true == true
+(\exists int i; true)