Commit 71831907 authored by Sarah Grebing's avatar Sarah Grebing

interim term

parent 06b8d82a
Pipeline #16937 passed with stages
in 10 minutes and 23 seconds
......@@ -79,17 +79,28 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
private boolean catchAll = false;
private static HashMap<String, MatchPath> reduceConform(Map<String, MatchPath> h1, Map<String, MatchPath> h2) {
HashMap<String, MatchPath> listOfElementsofH1 = new HashMap<>(h1);
HashMap<String, MatchPath> h3 = new HashMap<>(h1);
for (String s1 : listOfElementsofH1.keySet()) {
for (String s1 : h3.keySet()) {
if (!s1.equals("EMPTY_MATCH") && (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1)))) {
return null;
}
if (!s1.equals("EMPTY_MATCH") && h2.containsKey(s1)) {
if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable &&
!((QuantifiableVariable) h2.get(s1).getUnit()).name().toString().equals(h1.get(s1).toString())) {
return null;
}
if (h1.get(s1) instanceof MatchPath.MPQuantifiableVariable &&
!((QuantifiableVariable) h1.get(s1).getUnit()).name().toString().equals(h2.get(s1).toString())) {
return null;
}
if (!h2.get(s1).equals(h1.get(s1))) {
return null;
}
}
}
h3.putAll(h2);
return h3;
listOfElementsofH1.putAll(h2);
return listOfElementsofH1;
}
/**
......@@ -122,6 +133,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return oneMatch ? m3 : NO_MATCH;
}
/**
* Transform a number term into an int value.
* <p>
......@@ -449,11 +461,12 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
QuantifiableVariable qv = toMatch.boundVars().get(i);
if (qfPattern.getType() == MatchPatternLexer.DONTCARE) {
match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
//match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
match = reduceConform(match, EMPTY_MATCH);
continue;
}
if (qfPattern.getType() == MatchPatternLexer.SID) {
match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVariable(peek, qv, i)));
} else {
if (!qv.name().toString().equals(qfPattern.getText())) {
return NO_MATCH;
......@@ -464,8 +477,17 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
Matchings fromTerm = accept(ctx.skope, create(peek, 0));
//return handleBindClause(ctx.bindClause(), path, m);
Matchings retM = reduceConformQuant(fromTerm, match);
Matchings retM = reduceConform(fromTerm, match);
retM.forEach(stringMatchPathMap -> {
stringMatchPathMap.forEach((s, matchPath) -> {
if (matchPath instanceof MatchPath.MPQuantifiableVariable) {
//create term from variablename and put instead into map
}
}
);
});
return handleBindClause(ctx.bindClause(), peek, retM);
}
......@@ -532,32 +554,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) {
Matchings ret = new Matchings();
Map<String, MatchPath> quantifiedVarMap = match.first();
List<Map<String, MatchPath>> list = fromTerm.stream().filter(
map -> map.entrySet().stream().allMatch(
entry -> {
if (entry.getValue() != null) {
MatchPath mp = (MatchPath) entry.getValue();
Term mterm = (Term) mp.getUnit();
if (quantifiedVarMap.containsKey(entry.getKey())) {
return ((QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit()).name().toString().
equals(mterm.op().name().toString());
} else {
return true;
}
} else {
return true;
}
}
)
).collect(Collectors.toList());
ret.addAll(list);
return ret;
}
@Override
......@@ -621,3 +618,36 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return random.nextInt();
}
}
/* private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) {
Matchings ret = new Matchings();
Map<String, MatchPath> quantifiedVarMap = match.first();
System.out.println("quantifiedVarMap = " + quantifiedVarMap);
List<Map<String, MatchPath>> list = fromTerm.stream().filter(
map -> map.entrySet().stream().allMatch(
entry -> {
System.out.println("entry = " + entry);
if (entry.getValue() != null) {
MatchPath mp = (MatchPath) entry.getValue();
Term mterm = (Term) mp.getUnit();
if (quantifiedVarMap.containsKey(entry.getKey())) {
QuantifiableVariable unit = (QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit();
return unit.name().toString().
equals(mterm.op().name().toString());
} else {
return true;
}
} else {
//in this case we have an empty match, however, we may have bound quantVars, we need to add them
System.out.println("entry.getKey() = " + entry.getKey());
return true;
}
}
)
).collect(Collectors.toList());
ret.addAll(list);
return ret;
}*/
\ No newline at end of file
......@@ -47,9 +47,9 @@ public abstract class MatchPath<T, P> {
return unit.toString();
}
public static final class MPQuantifiableVarible extends MatchPath<QuantifiableVariable, Object> {
public static final class MPQuantifiableVariable extends MatchPath<QuantifiableVariable, Object> {
public MPQuantifiableVarible(MatchPath<? extends Object, ?> parent, QuantifiableVariable unit, int pos) {
public MPQuantifiableVariable(MatchPath<? extends Object, ?> parent, QuantifiableVariable unit, int pos) {
super(parent, unit, pos);
}
......
......@@ -59,7 +59,11 @@ public class MatcherFacadeTest {
shouldMatchForm("fint2(1,i)", "fint2(1,i)");
shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists _ _)");
shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists _ ?Term)");
shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X _)");
shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X (fint2(1,?X)))");
shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i (\\exists j _))");
......
......@@ -15,5 +15,6 @@ public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
info("There is no previous state to the current one.");
}
dbg.setStatePointer(stepBack);
}
}
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import lombok.val;
public class StepOverReverseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
val statePointer = dbg.getCurrentStatePointer();
PTreeNode<T> stepOverReverse = statePointer.getStepInvInto() != null ?
statePointer.getStepInvInto() :
statePointer.getStepInvOver();
if (stepOverReverse == null) {
info("There is no previous state to the current one.");
}
dbg.setStatePointer(stepOverReverse);
}
}
......@@ -926,6 +926,17 @@ public class DebuggerMain implements Initializable {
}
}
public void stepOverReverse(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepBack");
try {
model.getDebuggerFramework().execute(new StepOverReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}
}
public void stepIntoReverse(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepOverReverse");
try {
......@@ -1114,7 +1125,9 @@ public class DebuggerMain implements Initializable {
return FACADE.getContractsForJavaFileTask(model.getJavaFile());
}
}
//endregion
//region: StepIntoHandlers
@RequiredArgsConstructor
private class StepIntoHandler implements java.util.function.Consumer<PTreeNode<KeyData>> {
private final PTreeNode<KeyData> original;
......@@ -1169,8 +1182,7 @@ public class DebuggerMain implements Initializable {
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
}
}
//endregion
//endregion
}
//deprecated
/* @FXML
......
script split_from_quicksort_nice1() {
autopilot_prep;
foreach{
tryclose;
}
foreach{
simp_upd;
seqPermFromSwap;
andRight;
}
cases{
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
auto;
case match `==> (\exists ?X (\exists ?Y _))`: //this should match
instantiate var=`?X`[?X \ X] with=`i_0`;
instantiate var=`?Y`[?Y \ Y] with=`j_0`;
auto;
}
}
script split_from_quicksort_nice() {
autopilot_prep;
foreach{
......
......@@ -113,10 +113,20 @@
</graphic>
</MenuItem>
<MenuItem onAction="#stepBack"
<MenuItem onAction="#stepOverReverse"
accelerator="F7"
text="Step Back"
text="Step Over Reverse"
disable="${controller.stepNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/>
</graphic>
</MenuItem>
<MenuItem onAction="#stepIntoReverse"
accelerator="F8"
text="Step Into Reverse"
disable="${controller.stepNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/>
......@@ -125,7 +135,7 @@
<MenuItem disable="${controller.stepNotPossible}"
accelerator="F8"
accelerator="F9"
text="Step Out">
<graphic>
<MaterialDesignIconView glyphName="DEBUG_STEP_OUT" size="24.0"/>
......@@ -266,7 +276,7 @@
</tooltip>
</Button>
<Button onAction="#stepBack" disable="${controller.stepNotPossible}">
<Button onAction="#stepOverReverse" disable="${controller.stepNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0" scaleX="-1"/>
</graphic>
......
# Language Constructs
Proof scripts are textual representations of rule applications, settings changes
and macro invocations.
and strategy invocations (in the case of KeY as underlying verification
system also referred to as macros).
## Variables and Types
We need to distinguish between: logic, program, and script variables.
* **logic variable**: Occurs on sequences, only bounded to an quantifier
* **logic variable**: Occur on sequents, bounded by a quantifier or in an update
* **program variable**: declared and used in Java programs. They are constants
on the sequence.
on the sequent.
* **script variable**: declared and assignable within a script
......
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