Evaluator.java.orig 2.92 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
package edu.kit.formal.interpreter;

import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter;
import lombok.Setter;

import java.util.List;

/**
 * Class handling evaluation of expressions (visitor for expressions)
 *
 * @author S.Grebing
 */
public class Evaluator extends DefaultASTVisitor<Value> {
<<<<<<< Updated upstream
    private State currentState;
    private Stack<List<GoalNode>> matchedGoals = new Stack<>();
    private EvaluatorABI abi;
=======
    private GoalNode currentState;
    private List<VariableAssignment> matchedVariables = new ArrayList<>();
    @Getter
    @Setter
    private MatcherApi matcher;
>>>>>>> Stashed changes

    public Evaluator(State s) {
        this.currentState = s;
    }

    /**
     * Evaluation of an expression.
     *
     * @param truth
     * @return
     */
    public Value eval(Expression truth) {
        return (Value) truth.accept(this);
    }

    @Override
    public Value visit(BinaryExpression e) {
        Value v1 = (Value) e.getLeft().accept(this);
        Value v2 = (Value) e.getRight().accept(this);
        Operator op = e.getOperator();
        return op.evaluate(v1, v2);
    }

    /**
     * TODO Connect with KeY
     *
     * @param match
     * @return
     */
    @Override
    public Value visit(MatchExpression match) {
<<<<<<< Updated upstream

=======
        Value pattern = (Value) match.getPattern().accept(this);
>>>>>>> Stashed changes

        List<VariableAssignment> va = null;
        if (pattern.getType() == Type.STRING) {
            va = matcher.matchLabel(currentState, (String) pattern.getData());
        } else if (pattern.getType() == Type.TERM) {
            va = matcher.matchSeq(currentState, (String) pattern.getData());
        }

        return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
    }

    /**
     * TODO Connect with KeY
     *
     * @param term
     * @return
     */
    @Override
    public Value visit(TermLiteral term) {
        return null;
    }

    @Override
    public Value visit(StringLiteral string) {
        return Value.from(string);
    }

    @Override
    public Value visit(Variable variable) {
        //get variable value
        String id = variable.getIdentifier();
        Value v = currentState.lookupVarValue(id);
        if (v != null) {
            return v;
        } else {
            throw new RuntimeException("Variable " + variable + " was not initialized");
        }

    }

    @Override
    public Value visit(BooleanLiteral bool) {
        return bool.isValue() ? Value.TRUE : Value.FALSE;
    }


    @Override
    public Value visit(IntegerLiteral integer) {
        return Value.from(integer);
    }

    @Override
    public Value visit(UnaryExpression e) {
        Operator op = e.getOperator();
        Expression expr = e.getExpression();
        Value exValue = (Value) expr.accept(this);
        return op.evaluate(exValue);
    }


}