diff --git a/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java b/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java index 12c4e366..211d4ae0 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java +++ b/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) { diff --git a/modules/core/src/edu/kit/iti/algover/rules/Parameters.java b/modules/core/src/edu/kit/iti/algover/rules/Parameters.java index a0f1b077..b9b4b8d9 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/Parameters.java +++ b/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, null if no such - * value + * @return the value stored for that variable, {@link ParameterDescription#getDefaultValue()}, if value not + * explicitly specified, null if no such value. * @throws ClassCastException if the value is not assign-compatible with the * type in the parameter description. */ diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java b/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java index 56dd935d..466252c9 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java +++ b/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 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; } diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java b/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java index 4ca3bbf6..2f1ef7dc 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java +++ b/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 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) { diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java b/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java index acb40faa..aac78b82 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java +++ b/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java @@ -101,10 +101,18 @@ public Term visit(ApplTerm applTerm, Map 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 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 diff --git a/modules/fxgui/ListExample/AlgoVerList.dfy b/modules/fxgui/ListExample/AlgoVerList.dfy index 33bf5a9d..794587bb 100644 --- a/modules/fxgui/ListExample/AlgoVerList.dfy +++ b/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; ghost var nodeseqq: seq; ghost var footprint: set; + 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; - } -} \ No newline at end of file diff --git a/modules/fxgui/ListExample/AlgoVerList.dfy.proofs b/modules/fxgui/ListExample/AlgoVerList.dfy.proofs index 8ea0245d..8e6777e8 100644 --- a/modules/fxgui/ListExample/AlgoVerList.dfy.proofs +++ b/modules/fxgui/ListExample/AlgoVerList.dfy.proofs @@ -1,7 +1,7 @@ -Created by DIVE at Thu Apr 01 09:05:25 CEST 2021 +Created by DIVE at Tue Mar 08 09:27:04 CET 2022 boogie; boogie; boogie; @@ -12,18 +12,44 @@ boogie; boogie; boogie; -skip; -expand on='_ |-'; -vsasad -expand on='_ |-'; -skip;fwef - +boogie; +boogie; boogie; boogie; boogie; boogie; boogie; - +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 >= 0 && j < |this.nodeseqq| - 1 ==> this.nodeseqq[j].next == this.nodeseqq[(j + 1)])' with='idx₁'; + impLeft on='_ ==> _ |-'; + cases { + "mainBranch": + inst on='(forall n:int :: n >= 0 && n < |this.nodeseqq| ==> this.nodeseqq[n] != null)' with='pos'; + impLeft on='_ ==> _ |-'; + cases { + "mainBranch": + "": + } + "": + notLeft on='!(idx₁ >= 0 && idx₁ < |this.nodeseqq| - 1)'; + andRight on='|- _ && _'; + cases { + "case 1": + z3; + "case 2": + } + } +} boogie; boogie; boogie; @@ -45,7 +71,7 @@ skip;fwef boogie; boogie; boogie; -expand on='_.Valid()@_'; +boogie; boogie; boogie; boogie; @@ -53,55 +79,63 @@ skip;fwef boogie; boogie; - - +andRight on='|- _';cases { + "case 1": + z3; + "case 2": +} +andRight on='|- _';cases { + "case 1": + z3; + "case 2": +} boogie; boogie; - - - - - +boogie; +boogie; +boogie; +prop;skip; +boogie; boogie; boogie; boogie; boogie; - - - - - +boogie; +prop;skip; +boogie; +boogie; +boogie; boogie; boogie; boogie; boogie; boogie; - +boogie; boogie; - - - - - - - +prop;skip; +boogie; +boogie; +boogie; +boogie; +prop;boogie; +boogie; boogie; boogie; -expand on='_.Valid()@_'; +boogie; boogie; boogie; boogie; -skip;skip;skip;skip;expand on='_ |-';prop;skip;boogie; +boogie; boogie; boogie; boogie; boogie; - +prop;skip;boogie; boogie; - - - +boogie; +boogie; +prop;skip;expand on='this.Valid()'; boogie; diff --git a/modules/fxgui/src/edu/kit/iti/algover/MainController.java b/modules/fxgui/src/edu/kit/iti/algover/MainController.java index d16503bd..46d2f146 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/MainController.java +++ b/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."); } } diff --git a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java index e0e4adde..709966a4 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java +++ b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java @@ -156,7 +156,7 @@ public RuleApplicationController(ExecutorService executor, RuleApplicationListen })); - scriptRepText.getView().textProperty().addListener((observable, oldValue, newValue) -> { + /*scriptRepText.getView().textProperty().addListener((observable, oldValue, newValue) -> { String pvcIdentifier = PropertyManager.getInstance().currentProof.get().getPVC().getIdentifier(); String inFile = ""; try { @@ -168,7 +168,7 @@ public RuleApplicationController(ExecutorService executor, RuleApplicationListen inFile = inFile.replaceAll("[\\n\\t ]", ""); String textFieldReference = newValue.replaceAll("[\\n\\t ]", ""); lbUnsavedScript.setVisible(!inFile.equals(textFieldReference)); - }); + });*/ PropertyManager.getInstance().currentlyDisplayedView.addListener((observable, oldValue, newValue) -> { if (newValue.intValue() == TimelineFactory.DefaultViewPosition.SEQUENT_RULE.index) { @@ -241,6 +241,7 @@ public void addProofRule(ProofRule rule) { public void considerApplication(ProofNode target, Sequent selection, TermSelector selector) { if(target != null) { + // isValidForSequent could be avoided if selector is properly reset on proofchange if (selector != null && selector.isValidForSequent(selection)) { try { Term term = selector.selectSubterm(selection); diff --git a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java index f2473aa2..58fb66d1 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java +++ b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java @@ -90,15 +90,14 @@ public RuleViewOverlay(ProofRuleApplication application, RuleApplicationListener private void onRuleApplication(MouseEvent mouseEvent) { int requiredParams = 0; + + for(ParameterDescription p : application.getRule().getAllParameters().values()) { - if(p.isRequired() && p.getDefaultValue().isEmpty()) { + if(p.isRequired() && application.getParameters().getValue(p) == null) { requiredParams++; } } - if (mouseEvent.isShiftDown() || (requiredParams > 0 && - (application.getRule().getAllParameters().size() == 1 && - (!application.getRule().getAllParameters().containsValue(FocusProofRule.ON_PARAM_REQ) && - !application.getRule().getAllParameters().containsValue(DefaultFocusProofRule.ON_PARAM_OPT))))) { + if (mouseEvent.isShiftDown() || (requiredParams > 0 )) { String on; try { PrettyPrint pp = new PrettyPrint();