summaryrefslogtreecommitdiff
path: root/impl/FixpointAlgorithm.hpp
blob: b39a915f562ea1f57b4c50d29c59dd70dfb94500 (about) (plain)
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
#ifndef FIXPOINT_ALGORITHM_HPP
#define FIXPOINT_ALGORITHM_HPP

#include "IdSet.hpp"
#include "IdMap.hpp"
#include "VariableAssignment.hpp"
#include "EquationSystem.hpp"

template<typename Domain>
struct FixpointAlgorithm {
  virtual ~FixpointAlgorithm() { }
  virtual VariableAssignment<Domain>* maxFixpoint(const EquationSystem<Domain>&) const = 0;
};

template<typename Domain>
struct NaiveFixpointAlgorithm : public FixpointAlgorithm<Domain> {
  virtual VariableAssignment<Domain>* maxFixpoint(const EquationSystem<Domain>& system) const {
    VariableAssignment<Domain>* rho = NULL;
    VariableAssignment<Domain>* result = system.assignment(infinity<Domain>());
    do {
      if (rho) delete rho;
      rho = result;
      result = system.eval(*rho);
    } while (!system.equalAssignments(*rho, *result));
    if (rho) delete rho;
    return result;
  }
};

template<typename Domain>
struct SmartFixpointAlgorithm : public FixpointAlgorithm<Domain> {
  struct DynamicVariableAssignment : public VariableAssignment<Domain> {
    DynamicVariableAssignment(const EquationSystem<Domain>& system)
      : _system(system),
        _values(system.variableCount(), infinity<Domain>()),
        _stable(system.variableCount()),
        _influence(system.variableCount(), IdSet<Variable<Domain> >(system.variableCount())) { }

    const Domain& operator[](const Variable<Domain>& var) const {
      solve(var);
      //std::cout << _values << std::endl;
      return _values[var];
    }

    private:

    void solve(const Variable<Domain>& x) const {
      if (!_stable.contains(x)) {
        _stable.insert(x);

        Domain val = _system[x]->eval(DependencyAssignment(*this, x));

        if (val != _values[x]) {
          IdSet<Variable<Domain> > oldInfluence = _influence[x];
          _influence[x].clear();
          _values[x] = val;

          _stable.filter(oldInfluence);

          for (typename IdSet<Variable<Domain> >::iterator it = oldInfluence.begin();
               it != oldInfluence.end();
               ++it) {
            solve(_system.variable(*it));
          }
        }
      }
    }

    struct DependencyAssignment : public VariableAssignment<Domain> {
      DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable<Domain>& var)
        : _assignment(assignment), _var(var) { }
      const Domain& operator[](const Variable<Domain>& x) const {
        const Domain& result = _assignment[x];
        _assignment._influence[x].insert(_var);
        return result;
      }
      private:
      const DynamicVariableAssignment& _assignment;
      const Variable<Domain>& _var;
    };

    const EquationSystem<Domain>& _system;
    mutable IdMap<Variable<Domain>,Domain> _values;
    mutable IdSet<Variable<Domain> > _stable;
    mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
  };

  virtual VariableAssignment<Domain>* maxFixpoint(const EquationSystem<Domain>& system) const {
    return new DynamicVariableAssignment(system);
  }
};

#endif