Vs rule params (WIP)

modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java

@@ -29,6 +29,7 @@ public final ProofRuleApplication considerApplication(ProofNode target, Sequent
 
         try {
             Parameters params = new Parameters();
+
             ProofRuleApplication result = makeApplication(target, params);
             return result;
         } catch (NotApplicableException e) {

modules/core/src/edu/kit/iti/algover/rules/Parameters.java

@@ -87,8 +87,8 @@ public boolean hasValue(@NonNull ParameterDescription<?> param) {
      * via {@link ParameterDescription#getName()}.
      *
      * @param param the parameter description to look up.
-     * @return the value stored for that variable, <code>null</code> if no such
-     * value
+     * @return the value stored for that variable, {@link ParameterDescription#getDefaultValue()}, if value not
+     * explicitly specified, <code>null</code> if no such value.
      * @throws ClassCastException if the value is not assign-compatible with the
      *                            type in the parameter description.
      */

modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java

@@ -33,6 +33,7 @@
 import edu.kit.iti.algover.util.Util;
 
 import java.util.*;
+import java.util.stream.Collectors;
 
 /**
  * This proof rule allows one to expand an application of a function symbol to
@@ -244,12 +245,29 @@ private static Term instantiate(Term call, DafnyFunction function, DafnyTree tre
         }
 
         Term translation = ttt.build(tree);
-        translation = new LetTerm(assignments, translation);
+        LetTerm letTranslation = new LetTerm(assignments, translation);
+        /**
+         * Use {@link SubstitutionVisitor} that introduces bugfix for heap updates.
+         */
         if(inline) {
-            translation = LetInlineVisitor.inline(translation);
+            Map<String, Term> substitutionMap =
+                    letTranslation.getSubstitutions()
+                            .stream()
+                            .collect(Collectors.toMap(pair -> pair.fst.getName(), pair -> pair.snd));
+
+            Term inner = letTranslation.getTerm(0);
+            try {
+                Term result = inner.accept(new SubstitutionVisitor(), substitutionMap);
+                result = AlphaNormalisation.normalise(result);
+
+                return result;
+            }
+            catch(RuleException re) {
+                re.printStackTrace();
+            }
         }
 
-        return translation;
+        return letTranslation;
 
     }
 

modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java

@@ -8,18 +8,8 @@
 import de.uka.ilkd.pp.NoExceptions;
 import edu.kit.iti.algover.proof.ProofFormula;
 import edu.kit.iti.algover.proof.ProofNode;
-import edu.kit.iti.algover.rules.DefaultFocusProofRule;
-import edu.kit.iti.algover.rules.NoFocusProofRule;
-import edu.kit.iti.algover.rules.NotApplicableException;
-import edu.kit.iti.algover.rules.ParameterDescription;
-import edu.kit.iti.algover.rules.ParameterType;
-import edu.kit.iti.algover.rules.Parameters;
-import edu.kit.iti.algover.rules.ProofRuleApplication;
+import edu.kit.iti.algover.rules.*;
 import edu.kit.iti.algover.rules.ProofRuleApplication.Applicability;
-import edu.kit.iti.algover.rules.ProofRuleApplicationBuilder;
-import edu.kit.iti.algover.rules.RuleException;
-import edu.kit.iti.algover.rules.TermParameter;
-import edu.kit.iti.algover.rules.TermSelector;
 import edu.kit.iti.algover.rules.TermSelector.SequentPolarity;
 import edu.kit.iti.algover.term.ApplTerm;
 import edu.kit.iti.algover.term.DefaultTermVisitor;
@@ -36,7 +26,7 @@
 /**
  * Created by jklamroth on 10/25/18.
  */
-public class QuantifierInstantiation extends NoFocusProofRule {
+public class QuantifierInstantiation extends FocusProofRule {
 
     public static final ParameterDescription<TermParameter> WITH_PARAM =
             new ParameterDescription<>("with", ParameterType.TERM, true);
@@ -45,7 +35,7 @@ public class QuantifierInstantiation extends NoFocusProofRule {
             new ParameterDescription<>("var", ParameterType.STRING, false);
 
     public QuantifierInstantiation() {
-        super(DefaultFocusProofRule.ON_PARAM_OPT, WITH_PARAM);
+        super(ON_PARAM_REQ, WITH_PARAM);
     }
 
     @Override
@@ -56,7 +46,7 @@ public String getName() {
     @Override
     protected ProofRuleApplication makeApplicationImpl(ProofNode target, Parameters parameters) throws RuleException {
 
-        TermParameter onParam = parameters.getValue(DefaultFocusProofRule.ON_PARAM_OPT);
+        TermParameter onParam = parameters.getValue(ON_PARAM_REQ);
         TermParameter withParam = parameters.getValue(WITH_PARAM);
 
         if(onParam == null) {

modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java

@@ -101,10 +101,18 @@ public Term visit(ApplTerm applTerm, Map<String, Term> substitutions) throws Rul
             Term inner = applTerm.getTerm(i);
             Term innerReplaced = inner.accept(this, substitutions);
             subterms[i] = innerReplaced;
-
-            anythingNew |= inner != innerReplaced; // So that we know, when we cannot preserve identity anymore
+            anythingNew |= !inner.equals(innerReplaced); // So that we know, when we cannot preserve identity anymore
         }
         if (!anythingNew) {
+            // $heap() is a ApplTerm. Updates are handled by substitution. I. e., heap() is
+            // substituted by Store(heap,...). If the heap is updated a substition of the for
+            // "heap" -> .. is in the substitutions map.
+            // So this is a quick fix (tests pass)
+            if (subterms.length == 0) {
+                Term sub = substitutions.get(applTerm.getSort().getName());
+                if (sub != null)
+                    return sub;
+            }
             return applTerm;
         } else {
             try {
@@ -129,11 +137,11 @@ public Term visit(LetTerm letTerm, Map<String, Term> substitutions) throws RuleE
             VariableTerm var = pair.fst;
             Term letSubst = pair.snd;
             // No need to shadow yet.
-            // (Valentin) Why not?
             Term letSubstChanged = letSubst.accept(this, substitutions);
+
             substitutedLetSubstitutions.add(new Pair<>(var, letSubstChanged));
 
-            substitutionsChanged |= letSubst != letSubstChanged;
+            substitutionsChanged |= !letSubst.equals(letSubstChanged);
         }
 
         // Substitute the inner of the let

modules/fxgui/ListExample/AlgoVerList.dfy

@@ -1,3 +1,11 @@
+// ---- Automatically generated settings ----
+//> settings {
+//>    "KeY Timeout" = "10",
+//>    "Dafny Timeout" = "5",
+//>    "SMT Timeout" = "10",
+//>    "Sequent Generation Type" = "inline"
+//> }
+// ---- End of settings ----
 
 class Node {
   var value: int
@@ -15,9 +23,12 @@ class List {
   ghost var seqq: seq<int>;
   ghost var nodeseqq: seq<Node>;
   ghost var footprint: set<object>;
+
 
   var head: Node;
+
   function Valid() : bool
+    reads this
   {
     |seqq| == |nodeseqq| &&
     |seqq| >= 1 &&
@@ -51,7 +62,7 @@ class List {
   //currently inserting at position 0 is not supported (but should be an easy extension)
   method insertAt(pos: int, value: int)
     requires 0 <= pos < |seqq| && Valid()
-    ensures seqq == old(seqq[..pos] + [value] + seqq[pos..]) 
+    ensures seqq == old(seqq[..pos]) + [value] + old(seqq[pos..]) 
     ensures Valid()
     modifies footprint
   {
@@ -65,8 +76,7 @@ class List {
       node := node.next;
       idx := idx + 1;
     }
-    var newNode := new Node;
-    newNode.Init(value, node.next);
+    var newNode := new Node.Init(value, node.next);
     node.next := newNode;
     nodeseqq := nodeseqq[..pos] + [newNode] + nodeseqq[pos..];
     seqq := seqq[..pos] + [value] + seqq[pos..];
@@ -121,15 +131,3 @@ class List {
       v := node.value;
   }
 }
-
-class Node {
-  var value: int
-  var next: Node
-
-  method Init(value: int, next : Node) 
-    modifies this;
-  {
-    this.value := value;
-    this.next := next;
-  }
-}

modules/fxgui/ListExample/AlgoVerList.dfy.proofs

@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE properties SYSTEM "http://java.sun.com/dtd/properties.dtd">
 <properties>
-<comment>Created by DIVE at Thu Apr 01 09:05:25 CEST 2021</comment>
+<comment>Created by DIVE at Tue Mar 08 09:27:04 CET 2022</comment>
 <entry key="List.removeAt/then/else/Bounds">boogie;</entry>
 <entry key="List.insertAt/loop_exit/Post.1">boogie;</entry>
 <entry key="List.getAt/InitInv">boogie;</entry>
@@ -12,18 +12,44 @@
 <entry key="List.size/loop_exit/Post">boogie;</entry>
 <entry key="List.removeAt/then/then/Post.1">boogie;</entry>
 <entry key="List.getAt/loop/Inv.1">boogie;</entry>
-<entry key="List.size/InitInv.2">skip;
-expand on='_ |-';
-vsasad</entry>
-<entry key="List.size/InitInv.1">expand on='_ |-';
-skip;fwef
-</entry>
+<entry key="List.size/InitInv.2">boogie;</entry>
+<entry key="List.size/InitInv.1">boogie;</entry>
 <entry key="List.removeAt/else/loop/Inv.1">boogie;</entry>
 <entry key="List.removeAt/then/then/Post">boogie;</entry>
 <entry key="List.getAt/loop/Inv">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/Modifies">boogie;</entry>
 <entry key="List.insertAt/loop_exit/Modifies[Init]">boogie;</entry>
-<entry key="List.insertAt/loop_exit/Bounds"></entry>
+<entry key="List.insertAt/loop_exit/Bounds">andRight on='|- _';cases {
+  "case 1":
+    z3;
+  "case 2":
+    notLeft on='!$isCreated($heap, $new₁)';
+    notLeft on='!_';
+    prop;
+    skip;
+    expand on='this.Valid()';
+    prop;
+    skip;
+    inst on='(forall j:int :: j &gt;= 0 &amp;&amp; j &lt; |this.nodeseqq| - 1 ==&gt; this.nodeseqq[j].next == this.nodeseqq[(j + 1)])' with='idx₁';
+    impLeft on='_ ==&gt; _ |-';
+    cases {
+      "mainBranch":
+        inst on='(forall n:int :: n &gt;= 0 &amp;&amp; n &lt; |this.nodeseqq| ==&gt; this.nodeseqq[n] != null)' with='pos';
+        impLeft on='_ ==&gt; _ |-';
+        cases {
+          "mainBranch":
+          "":
+        }
+      "":
+        notLeft on='!(idx₁ &gt;= 0 &amp;&amp; idx₁ &lt; |this.nodeseqq| - 1)';
+        andRight on='|- _ &amp;&amp; _';
+        cases {
+          "case 1":
+            z3;
+          "case 2":
+        }
+    }
+}</entry>
 <entry key="List.removeAt/then/then/Bounds.1">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/else/Post">boogie;</entry>
 <entry key="List.Valid/Bounds.7">boogie;</entry>
@@ -45,63 +71,71 @@ skip;fwef
 <entry key="List.Valid/Bounds.3">boogie;</entry>
 <entry key="List.Valid/Bounds.2">boogie;</entry>
 <entry key="List.removeAt/else/InitInv">boogie;</entry>
-<entry key="List.size/loop/Inv">expand on='_.Valid()@_';</entry>
+<entry key="List.size/loop/Inv">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/else/Bounds.3">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/else/Bounds.1">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/else/Bounds.2">boogie;</entry>
 <entry key="List.removeAt/then/else/Post">boogie;</entry>
 <entry key="List.insertAt/InitInv.1">boogie;</entry>
 <entry key="List.size/loop/Dec">boogie;</entry>
 <entry key="List.insertAt/loop_exit/Bounds.1"></entry>
-<entry key="List.insertAt/loop_exit/Bounds.2"></entry>
-<entry key="List.insertAt/loop_exit/Bounds.3"></entry>
+<entry key="List.insertAt/loop_exit/Bounds.2">andRight on='|- _';cases {
+  "case 1":
+    z3;
+  "case 2":
+}</entry>
+<entry key="List.insertAt/loop_exit/Bounds.3">andRight on='|- _';cases {
+  "case 1":
+    z3;
+  "case 2":
+}</entry>
 <entry key="List.removeAt/else/loop_exit/then/Bounds">boogie;</entry>
 <entry key="List.insertAt/loop/Dec">boogie;</entry>
-<entry key="List.Valid/Reads.14"></entry>
-<entry key="List.Valid/Reads.13"></entry>
-<entry key="List.Valid/Reads.12"></entry>
-<entry key="List.Valid/Reads.11"></entry>
-<entry key="List.Valid/Reads.10"></entry>
+<entry key="List.Valid/Reads.14">boogie;</entry>
+<entry key="List.Valid/Reads.13">boogie;</entry>
+<entry key="List.Valid/Reads.12">boogie;</entry>
+<entry key="List.Valid/Reads.11">prop;skip;</entry>
+<entry key="List.Valid/Reads.10">boogie;</entry>
 <entry key="List.removeAt/then/else/Bounds.1">boogie;</entry>
 <entry key="List.removeAt/then/else/Bounds.2">boogie;</entry>
 <entry key="List.removeAt/then/else/Bounds.3">boogie;</entry>
 <entry key="List.getAt/loop_exit/Post">boogie;</entry>
-<entry key="List.Valid/Reads"></entry>
-<entry key="List.Valid/Reads.19"></entry>
-<entry key="List.Valid/Reads.18"></entry>
-<entry key="List.Valid/Reads.17"></entry>
-<entry key="List.Valid/Reads.16"></entry>
+<entry key="List.Valid/Reads">boogie;</entry>
+<entry key="List.Valid/Reads.19">prop;skip;</entry>
+<entry key="List.Valid/Reads.18">boogie;</entry>
+<entry key="List.Valid/Reads.17">boogie;</entry>
+<entry key="List.Valid/Reads.16">boogie;</entry>
 <entry key="List.insertAt/loop/Inv">boogie;</entry>
 <entry key="List.Valid/Reads.15"></entry>
 <entry key="List.getAt/loop/Null">boogie;</entry>
 <entry key="List.removeAt/else/loop/Null">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/then/Post">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/Null">boogie;</entry>
-<entry key="List.Valid/Reads.9"></entry>
+<entry key="List.Valid/Reads.9">boogie;</entry>
 <entry key="List.insertAt/loop_exit/Null">boogie;</entry>
-<entry key="List.Valid/Reads.8"></entry>
-<entry key="List.Valid/Reads.7"></entry>
-<entry key="List.Valid/Reads.21"></entry>
-<entry key="List.Valid/Reads.6"></entry>
-<entry key="List.Valid/Reads.20"></entry>
-<entry key="List.Valid/Reads.5"></entry>
-<entry key="List.Valid/Reads.4"></entry>
+<entry key="List.Valid/Reads.8">prop;skip;</entry>
+<entry key="List.Valid/Reads.7">boogie;</entry>
+<entry key="List.Valid/Reads.21">boogie;</entry>
+<entry key="List.Valid/Reads.6">boogie;</entry>
+<entry key="List.Valid/Reads.20">boogie;</entry>
+<entry key="List.Valid/Reads.5">prop;boogie;</entry>
+<entry key="List.Valid/Reads.4">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/then/Post.1">boogie;</entry>
 <entry key="List.removeAt/else/InitInv.1">boogie;</entry>
 <entry key="List.insertAt/loop_exit/Modifies"></entry>
-<entry key="List.size/Null">expand on='_.Valid()@_';</entry>
+<entry key="List.size/Null">boogie;</entry>
 <entry key="List.Valid/Null">boogie;</entry>
 <entry key="List.size/loop/Inv.1">boogie;</entry>
 <entry key="List.size/loop/Inv.2">boogie;</entry>
-<entry key="List.size/InitInv">skip;skip;skip;skip;expand on='_ |-';prop;skip;boogie;</entry>
+<entry key="List.size/InitInv">boogie;</entry>
 <entry key="List.removeAt/else/loop_exit/then/Bounds.1">boogie;</entry>
 <entry key="List.removeAt/then/then/Bounds">boogie;</entry>
 <entry key="List.Valid/Bounds">boogie;</entry>
 <entry key="List.insertAt/InitInv">boogie;</entry>
-<entry key="List.Valid/Reads.3"></entry>
+<entry key="List.Valid/Reads.3">prop;skip;boogie;</entry>
 <entry key="List.size/loop/Null">boogie;</entry>
-<entry key="List.Valid/Reads.2"></entry>
-<entry key="List.Valid/Reads.1"></entry>
-<entry key="List.insertAt/loop_exit/Post"></entry>
+<entry key="List.Valid/Reads.2">boogie;</entry>
+<entry key="List.Valid/Reads.1">boogie;</entry>
+<entry key="List.insertAt/loop_exit/Post">prop;skip;expand on='this.Valid()';</entry>
 <entry key="List.removeAt/else/loop/Inv">boogie;</entry>
 </properties>

modules/fxgui/src/edu/kit/iti/algover/MainController.java

@@ -650,14 +650,20 @@ public void onRuleApplication(ProofRuleApplication application) {
 
     @Override
     public void onScriptSave() {
-        String pvcIdentifier = PropertyManager.getInstance().currentProof.get().getPVC().getIdentifier();
-        try {
-            //manager.saveProofScriptForPVC(pvcIdentifier, PropertyManager.getInstance().currentProof.get());
-            manager.saveProofScripts();
-            Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).info("Successfully saved script " + pvcIdentifier + ".");
-        } catch (IOException e) {
-            Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).severe("Error saving script.");
-            e.printStackTrace();
+        Proof curP = PropertyManager.getInstance().currentProof.get();
+        String pvcIdentifier = "";
+        if (curP != null) {
+            pvcIdentifier = curP.getPVC().getIdentifier();
+            try {
+                //manager.saveProofScriptForPVC(pvcIdentifier, PropertyManager.getInstance().currentProof.get());
+                manager.saveProofScripts();
+                Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).info("Successfully saved script " + pvcIdentifier + ".");
+            } catch (IOException e) {
+                Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).severe("Error saving script.");
+                e.printStackTrace();
+            }
+        } else {
+            Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).info("No PVC selected.");
         }
     }