diff options
Diffstat (limited to 'impl/main.cpp')
-rw-r--r-- | impl/main.cpp | 61 |
1 files changed, 40 insertions, 21 deletions
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; } |