summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCarlo Zancanaro <carlo@carlo-laptop>2012-05-01 00:01:23 +1000
committerCarlo Zancanaro <carlo@carlo-laptop>2012-05-01 00:01:23 +1000
commit1bf6761d36d4a08c1ebe3c496cefb3c7569ba95e (patch)
tree78319a6142799639a108c2988088c44e0de3b21d
parente00c1e3f71bb1840e10a85af53469a81c73c7ef1 (diff)
Update the example to be the one from the paper.
-rw-r--r--impl/Operator.hpp7
-rw-r--r--impl/Solver.hpp17
-rw-r--r--impl/main.cpp61
-rw-r--r--impl/output.png0
4 files changed, 45 insertions, 40 deletions
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<T> {
};
template<typename T>
-struct Increment: public Operator<T> {
+struct Addition: public Operator<T> {
+ Addition(int i) : _value(i) { }
T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& 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<typename T>
-struct Solver {
- VariableAssignment<T> solveBF(const EquationSystem<T>& system) {
- VariableAssignment<T> 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<typename T>
-struct Complete {
- Complete(const T& value)
- : _value(value) { }
- private:
- bool _infinity;
- T _value;
-};*/
-
typedef std::vector<Expression<float>*> Args;
typedef Expression<float> E;
typedef Constant<float> C;
+typedef Addition<float> A;
typedef Minimum<float> Min;
std::vector< Expression<float>* > empty;
int main () {
EquationSystem<float> sys;
Variable<float>* x = sys.newVariable("x");
+ Variable<float>* y = sys.newVariable("y");
+ Variable<float>* 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<float>, 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<float> 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
--- /dev/null
+++ b/impl/output.png