Parameterise fixpoint and strategy improvement

(command-line arguments specify which to use)

Also:
 - Fix up Complete<T> to work comparing `inf` to 1 (stupid bug)
 - Clean up the systems/ folder a bit
 - Change the printed output to differentiate variables and constants
   (!v/!c, respectively)
 - Perform a slight optimisation to the strategy-iteration process

1 files changed, 34 insertions, 10 deletions

diff --git a/impl/main.cpp b/impl/main.cpp
index 40cae42..6546444 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -93,13 +93,33 @@ void treeToSystem(pANTLR3_BASE_TREE node, ConcreteEquationSystem<T>& system) {
 
 typedef Complete<int> ZBar;
 int main (int argc, char* argv[]) {
+  if (argc <= 3) {
+    cout << "Usage: " << argv[0] << " filename naive|smart naive|repeat" << endl;
+    exit(1);
+  }
   FixpointAlgorithm<ZBar>* algorithm = NULL;
-  if (argc > 2 && !strcmp(argv[2], "naive")) {
+  if (!strcmp(argv[2], "naive")) {
     algorithm = new NaiveFixpointAlgorithm<ZBar>();
     cout << "Naive fixpoint" << endl;
-  } else {
+  } else if (!strcmp(argv[2], "smart")) {
     algorithm = new SmartFixpointAlgorithm<ZBar>();
     cout << "Smart fixpoint" << endl;
+  } else {
+    cout << "Unknown fixpoint algorithm." << endl;
+  }
+  MaxStrategy<ZBar>::ImprovementOperator* naiveImprovement = new MaxStrategy<ZBar>::NaiveImprovementOperator();
+  MaxStrategy<ZBar>::ImprovementOperator* improvement = NULL;
+  if (!strcmp(argv[3], "repeat")) {
+    improvement = new MaxStrategy<ZBar>::RepeatedImprovementOperator(*naiveImprovement);
+    cout << "Repeated strategy improvement" << endl;
+  } else if (!strcmp(argv[3], "naive")) {
+    improvement = naiveImprovement;
+    cout << "Naive strategy improvement" << endl;
+  } else {
+    cout << "Unknown strategy improvement algorithm." << endl;
+  }
+  if (!improvement || !algorithm) {
+    exit(1);
   }
 
   pANTLR3_INPUT_STREAM input;
@@ -119,21 +139,19 @@ int main (int argc, char* argv[]) {
   // DO MORE HERE
 
   cout << system << endl;
-  VariableAssignment<ZBar>* prev = NULL;
-  VariableAssignment<ZBar>* result = system.assignment(-infinity<ZBar>());
+  VariableAssignment<ZBar>* result = NULL;
   MaxStrategy<ZBar> strategy(system);
+  bool changed;
   do {
-    if (prev) delete prev;
-    prev = result;
+    if (result) delete result;
+    result = algorithm->maxFixpoint(strategy);
     /*for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
       cout << var.name() << " = " << (*result)[var] << ", ";
     }
     cout << endl;*/
-    strategy.improve(*prev);
-    result = algorithm->maxFixpoint(strategy);
-  } while(!system.equalAssignments(*prev, *result));
-  if (prev) delete prev;
+    changed = strategy.improve(*improvement, *result);
+  } while(changed);
 
   VariableAssignment<ZBar>* rho = result;
 
@@ -143,6 +161,12 @@ int main (int argc, char* argv[]) {
     cout << var.name() << " = " << (*rho)[var] << endl;
   }
 
+  delete result;
+  delete algorithm;
+  if (naiveImprovement != improvement)
+    delete improvement;
+  delete naiveImprovement;
+
   parser -> free(parser);
   tokens -> free(tokens);
   lex -> free(lex);