Dependency-aware smart fixpoint.

Slows it down *heaps* for the moment.
Still need to add the MaxStrategy part, which should speed it up a fair
bit. At the moment it has to do a fair bit more work for no benefit.

1 files changed, 32 insertions, 30 deletions

diff --git a/impl/main.cpp b/impl/main.cpp
index 3f47a7b..b761587 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -98,19 +98,34 @@ int main (int argc, char* argv[]) {
     exit(1);
   }
 
+  pANTLR3_INPUT_STREAM input;
+  pEquationSystemLexer lex;
+  pANTLR3_COMMON_TOKEN_STREAM tokens;
+  pEquationSystemParser parser;
+
+  input = antlr3FileStreamNew((pANTLR3_UINT8)argv[1], ANTLR3_ENC_8BIT);
+  lex = EquationSystemLexerNew(input);
+  tokens = antlr3CommonTokenStreamSourceNew(ANTLR3_SIZE_HINT, TOKENSOURCE(lex));
+  parser = EquationSystemParserNew(tokens);
 
+  EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
+
+  ConcreteEquationSystem<ZBar> system;
+  treeToSystem<ZBar>(ret.tree, system);
+
+  // PARSE ARGUMENTS - fixpoint
   FixpointAlgorithm<ZBar>* algorithm = NULL;
   if (!strcmp(argv[2], "naive")) {
-    algorithm = new NaiveFixpointAlgorithm<ZBar>();
+    algorithm = new NaiveFixpointAlgorithm<ZBar>(system);
     cout << "Naive fixpoint" << endl;
   } else if (!strcmp(argv[2], "smart")) {
-    algorithm = new SmartFixpointAlgorithm<ZBar>();
+    algorithm = new SmartFixpointAlgorithm<ZBar>(system);
     cout << "Smart fixpoint" << endl;
   } else {
     cout << "Unknown fixpoint algorithm." << endl;
   }
 
-
+  // PARSE ARGUMENTS - strat improvement
   MaxStrategy<ZBar>::ImprovementOperator* naiveImprovement = new MaxStrategy<ZBar>::NaiveImprovementOperator();
   MaxStrategy<ZBar>::ImprovementOperator* improvement = NULL;
   if (!strcmp(argv[3], "repeat")) {
@@ -126,46 +141,33 @@ int main (int argc, char* argv[]) {
     exit(1);
   }
 
-  pANTLR3_INPUT_STREAM input;
-  pEquationSystemLexer lex;
-  pANTLR3_COMMON_TOKEN_STREAM tokens;
-  pEquationSystemParser parser;
-
-  input = antlr3FileStreamNew((pANTLR3_UINT8)argv[1], ANTLR3_ENC_8BIT);
-  lex = EquationSystemLexerNew(input);
-  tokens = antlr3CommonTokenStreamSourceNew(ANTLR3_SIZE_HINT, TOKENSOURCE(lex));
-  parser = EquationSystemParserNew(tokens);
-
-  EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
-
-  ConcreteEquationSystem<ZBar> system;
-  treeToSystem<ZBar>(ret.tree, system);
-  // DO MORE HERE
-
   cout << system << endl;
-  VariableAssignment<ZBar>* result = NULL;
+  StableVariableAssignment<ZBar> result(system.variableCount(), infinity<ZBar>());
   MaxStrategy<ZBar> strategy(system);
-  bool changed;
+  IdSet<Variable<ZBar> > s1(system.variableCount());
+  IdSet<Variable<ZBar> > s2(system.variableCount());
+  bool changed = false;
   do {
-    if (result) delete result;
-    result = algorithm->maxFixpoint(strategy);
+    s2.clear();
+    s2.invert();
+    algorithm->maxFixpoint(strategy, result, s2, s1);
+
     /*for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      cout << var.name() << " = " << (*result)[var] << ", ";
+      cout << var.name() << " = " << result[var] << ", " << endl;
     }
-    cout << endl;*/
-    changed = strategy.improve(*improvement, *result);
-  } while(changed);
+    cout << endl;
+    exit(0);*/
 
-  VariableAssignment<ZBar>* rho = result;
+    changed = strategy.improve(*improvement, result, s1, s2);
+  } while(changed);
 
   cout << endl;
   for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
     Variable<ZBar>& var = system.variable(i);
-    cout << var.name() << " = " << (*rho)[var] << endl;
+    cout << var.name() << " = " << result[var] << endl;
   }
 
-  delete result;
   delete algorithm;
   if (naiveImprovement != improvement)
     delete improvement;