From 1bf6761d36d4a08c1ebe3c496cefb3c7569ba95e Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Tue, 1 May 2012 00:01:23 +1000 Subject: Update the example to be the one from the paper. --- impl/Operator.hpp | 7 +++++-- impl/Solver.hpp | 17 ---------------- impl/main.cpp | 61 ++++++++++++++++++++++++++++++++++++------------------- impl/output.png | 0 4 files changed, 45 insertions(+), 40 deletions(-) delete mode 100644 impl/Solver.hpp create mode 100644 impl/output.png diff --git a/impl/Operator.hpp b/impl/Operator.hpp index 71a1e68..2c5af75 100644 --- a/impl/Operator.hpp +++ b/impl/Operator.hpp @@ -59,10 +59,13 @@ struct Constant : public Operator { }; template -struct Increment: public Operator { +struct Addition: public Operator { + Addition(int i) : _value(i) { } T operator() (const std::vector< Expression* >& args, const VariableAssignment& ass) const { - return (*args[0])(ass) + 1; + return (*args[0])(ass) + _value; } + private: + int _value; }; #include "VariableAssignment.hpp" diff --git a/impl/Solver.hpp b/impl/Solver.hpp deleted file mode 100644 index 11369bc..0000000 --- a/impl/Solver.hpp +++ /dev/null @@ -1,17 +0,0 @@ -#ifndef SOLVER_HPP -#define SOLVER_HPP - -#include "Factory.hpp" -#include "VariableAssignment.hpp" - -template -struct Solver { - VariableAssignment solveBF(const EquationSystem& system) { - VariableAssignment result; - for (unsigned int i = 0; i < _var_count; ++i) { - result = system(result); - } - } -}; - -#endif diff --git a/impl/main.cpp b/impl/main.cpp index 579db25..db3d0f7 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -9,41 +9,60 @@ using namespace std; -/*template -struct Complete { - Complete(const T& value) - : _value(value) { } - private: - bool _infinity; - T _value; -};*/ - typedef std::vector*> Args; typedef Expression E; typedef Constant C; +typedef Addition A; typedef Minimum Min; std::vector< Expression* > empty; int main () { EquationSystem sys; Variable* x = sys.newVariable("x"); + Variable* y = sys.newVariable("y"); + Variable* z = sys.newVariable("z"); + + Args xPlusArgs; + xPlusArgs.push_back(new E(x, empty)); + Args xMinArgs; + xMinArgs.push_back(new E(new A(-1), xPlusArgs)); + xMinArgs.push_back(new E(y, empty)); + Args xMaxArgs; + xMaxArgs.push_back(new E(new C(0), empty)); + xMaxArgs.push_back(new E(new Min(), xMinArgs)); + sys[*x] = sys.newMaxExpression(xMaxArgs); + // x = max(0, min(x-1, y)) - Args incArgs; - incArgs.push_back(new E(x, empty)); + Args yPlusArgs; + yPlusArgs.push_back(new E(x, empty)); + Args yMaxArgs; + yMaxArgs.push_back(new E(new C(0), empty)); + yMaxArgs.push_back(new E(new A(5), yPlusArgs)); + yMaxArgs.push_back(new E(x, empty)); + sys[*y] = sys.newMaxExpression(yMaxArgs); + // y = max(0, x+5, x) - Args minArgs; - minArgs.push_back(new E(new Increment, incArgs)); - minArgs.push_back(new E(new C(100), empty)); + Args zPlusArgs1; + zPlusArgs1.push_back(new E(z, empty)); + Args zPlusArgs2; + zPlusArgs2.push_back(new E(x, empty)); + Args zMaxArgs; + zMaxArgs.push_back(new E(new C(0), empty)); + zMaxArgs.push_back(new E(new A(1), zPlusArgs1)); + zMaxArgs.push_back(new E(new A(0), zPlusArgs2)); + sys[*z] = sys.newMaxExpression(zMaxArgs); + // z = max(0, z+1, x) - Args maxArgs; - maxArgs.push_back(new E(new C(0), empty)); - maxArgs.push_back(new E(new Min(), minArgs)); - sys[*x] = sys.newMaxExpression(maxArgs); - // x = max(0, min(x+1, 100)) - cout << sys.minFixpoint()[*x] << endl; - // -> 100, as expected + // x = max(0, min(x-1, y)) + // y = max(0, x+5, x) + // z = max(0, z+1, x) + // => x: 0, y: 5, z: inf + VariableAssignment fixpoint = sys.minFixpoint(); + cout << "x = " << fixpoint[*x] << endl; + cout << "y = " << fixpoint[*y] << endl; + cout << "z = " << fixpoint[*z] << endl; return 0; } diff --git a/impl/output.png b/impl/output.png new file mode 100644 index 0000000..e69de29 -- cgit v1.2.3