Commit e3b05097 authored by Sarah Grebing's avatar Sarah Grebing

Matchings with quantifiablevars is working again

parent b44624c5
Pipeline #20982 canceled with stages
......@@ -3,6 +3,8 @@ package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.LogicVariable;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.ApplyStrategy;
......@@ -174,7 +176,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
//System.out.println("Signature " + sig.toString());
Matchings m = kmf.matches(pattern, sig);
if (m.isEmpty()) {
if (m.isNoMatch()) {
LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());
return Collections.emptyList();
} else {
......@@ -182,8 +184,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
VariableAssignment va = new VariableAssignment(null);
for (String s : firstMatch.keySet()) {
MatchPath matchPath = firstMatch.get(s);
if (!s.equals("EMPTY_MATCH")) {
Term matched = (Term) matchPath.getUnit();
//if (!s.equals("EMPTY_MATCH")) {
Term matched;
try {
matched = (Term) matchPath.getUnit();
if (s.startsWith("?")) {
s = s.replaceFirst("\\?", "");
......@@ -192,8 +196,23 @@ public class KeYMatcher implements MatcherApi<KeyData> {
Value<String> value = toValueTerm(currentState.getData(), matched);
va.declare(s, value.getType());
va.assign(s, value);
//LOGGER.info("Variables to match " + s + " : " + value);
} catch (ClassCastException e){
LogicVariable var = (LogicVariable) matchPath.getUnit();
String reprTerm = var.name().toString();
Value<String> value = new Value<>(
new TermType(new SortType(var.sort())),
reprTerm);
if (s.startsWith("?")) {
s = s.replaceFirst("\\?", "");
}
va.declare(s, value.getType());
va.assign(s, value);
}
//LOGGER.info("Variables to match " + s + " : " + value);
//}
}
List<VariableAssignment> retList = new LinkedList();
LOGGER.info("Matched Variables " + va.toString());
......
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.AbstractSortedOperator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.parser.DefaultTermParser;
import de.uka.ilkd.key.parser.ParserException;
import edu.kit.iti.formal.psdbg.parser.ast.Operator;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import lombok.Builder;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableArray;
import java.io.Reader;
import java.io.StringReader;
import java.util.ArrayList;
import java.util.List;
import java.util.function.Function;
@Builder
public class KeyMatcherFacade {
......@@ -23,6 +30,7 @@ public class KeyMatcherFacade {
private final KeYEnvironment environment;
private final Sequent sequent;
public Matchings matches(String pattern, Signature sig) {
if(pattern.contains("==>")) {
return matchesSequent(pattern, sig);
......@@ -84,4 +92,6 @@ public class KeyMatcherFacade {
StringReader sr = new StringReader(pattern);
return sr;
}
}
......@@ -7,6 +7,7 @@ import lombok.Getter;
import lombok.Setter;
import java.util.*;
import java.util.function.Function;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import java.util.stream.Stream;
......@@ -18,6 +19,8 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
private List<Integer> currentposition = new ArrayList<>();
@Setter @Getter private boolean catchAll = false;
@Setter
java.util.function.BiFunction<QuantifiableVariable, Term, Term> parseQuantVar;
public Matchings matchesToplevel(Sequent sequent, List<Term> patternTerms) {
......@@ -52,6 +55,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
private Matchings matchesSemisequent(MatchPath.MPSemiSequent peek, List<Term> patterns) {
Semisequent semiSeq = peek.getUnit();
if (semiSeq.isEmpty()) {
if(patterns.isEmpty()){
return MutableMatchings.emptySingleton();
......@@ -78,6 +82,10 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
List<Matchings> matchings = new ArrayList<>();
reduceDisjoint(map, patterns, matchings);
if (map.values().stream().allMatch(Map::isEmpty))
return NoMatch.INSTANCE;
Matchings ret = new MutableMatchings();
//.filter(x -> !x.equals(EmptyMatch.INSTANCE))
matchings.forEach(ret::addAll);
......@@ -151,7 +159,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
} else {
name = pv.name().toString();
}
MatchPath mp = new MatchPath.MPQuantifiableVariable(subject, bv, -i);
MatchPath mp = new MatchPath.MPQuantifiableVariable(subject, bv, -i);
mPaths.put(name, mp);
// mPaths.put(name, subject);
} else if (!pv.name().equals(bv.name())) {
......
......@@ -73,7 +73,7 @@ public class MutableMatchings implements Matchings {
@Override
public Matchings reduceConform(Matchings other) {
//shortcuts
if(other.isNoMatch()) return other.reduceConform(this);
if(other.isNoMatch()) return NoMatch.INSTANCE;
if(other.isEmpty()) return other.reduceConform(this);
if(this.inner.size() == 0) return other;
MutableMatchings mother = (MutableMatchings) other;
......
package edu.kit.iti.formal.psdbg.examples;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import org.apache.commons.io.IOUtils;
import java.io.File;
import java.io.IOException;
import java.io.*;
import java.net.URL;
import java.nio.charset.Charset;
......@@ -24,6 +26,12 @@ public class JavaExample extends Example {
protected URL javaFile;
protected URL settingsFile;
public void setSettingsFile(URL settingsFile) {
this.settingsFile = settingsFile;
}
@Override
public void open(DebuggerMain debuggerMain) {
//TODO should be reworked if we have an example
......@@ -39,7 +47,11 @@ public class JavaExample extends Example {
//System.out.println(java.getAbsolutePath());
//debuggerMain.openKeyFile(key);
debuggerMain.openJavaFile(java);
if (settingsFile != null) {
File settings = newTempFile(settingsFile, getName() + ".props");
ProofListener pl = new ProofListener(debuggerMain, settings);
debuggerMain.getFacade().proofProperty().addListener(pl);
}
debuggerMain.showActiveInspector(null);
if (helpText != null) {
String content = IOUtils.toString(helpText, Charset.defaultCharset());
......@@ -49,4 +61,31 @@ public class JavaExample extends Example {
e.printStackTrace();
}
}
public class ProofListener implements ChangeListener<Proof> {
File settingsFile;
DebuggerMain debuggerMain;
public ProofListener(DebuggerMain debuggerMain, File settingsFile) {
this.debuggerMain = debuggerMain;
this.settingsFile = settingsFile;
}
@Override
public void changed(ObservableValue<? extends Proof> observable, Proof oldValue, Proof newValue) {
if (newValue != null) {
try {
BufferedReader reader = new BufferedReader(new FileReader(settingsFile));
newValue.getSettings().loadSettingsFromStream(reader);
} catch (FileNotFoundException e) {
e.printStackTrace();
}
debuggerMain.getFacade().proofProperty().removeListener(this);
}
}
}
}
......@@ -8,7 +8,7 @@ public class QuickSort extends JavaExample {
setName("Quicksort example");
setSettingsFile(getClass().getResource("proof-settings.props"));
setHelpText(getClass().getResource("help.html"));
setJavaFile(getClass().
......
#Proof-Settings-Config-File
#Mon Feb 05 16:31:07 CET 2018
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , runtimeExceptions-runtimeExceptions\:allow , JavaCard-JavaCard\:off , Strings-Strings\:on , modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:on , reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
......@@ -10,12 +10,14 @@ script split_from_quicksort() {
}
cases{
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
cases{
case match `? ==> seqDef{?;}(?,?,?) = seqDef{?;}(?, ?, ?)`:
__KEY_MAX_STEPS:=10000;
auto;
case match `==> (\exists ?X (\exists ?Y _))`:
case match `? ==> (\exists ?X:int; (\exists ?Y:int; ?))`:
instantiate var=X with=`i_0`;
instantiate var=Y with=`j_0`;
__KEY_MAX_STEPS:=60000;
auto;
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment