1 files changed, 35 insertions, 76 deletions

diff --git a/impl/main.cpp b/impl/main.cpp
index 374d21f..6a786bd 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -7,8 +7,6 @@
 #include "Operator.hpp"
 #include "EquationSystem.hpp"
 #include "MaxStrategy.hpp"
-#include "ImprovementOperator.hpp"
-#include "FixpointAlgorithm.hpp"
 
 extern "C" {
 #include "parser/EquationSystemParser.h"
@@ -38,7 +36,7 @@ Expression<T>& treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
   }
 
   // anything that's not a constant/variable
-  std::vector<Expression<T>*> args;
+  vector<Expression<T>*> args;
   pANTLR3_BASE_TREE childNode;
   for (unsigned int i = 0; i < num; ++i) {
     childNode = (pANTLR3_BASE_TREE) node->getChild(node, i);
@@ -97,14 +95,6 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
 
 typedef Complete<int> ZBar;
 int main (int argc, char* argv[]) {
-  if (argc <= 3) {
-    cerr << "Usage: " << argv[0] << " filename fixpoint strategy [log]" << endl
-         << "  fixpoint: naive | smart" << endl
-         << "  strategy: naive | repeat | smart" << endl
-         << "  log: section[,section[,section[...]]]" << endl;
-    exit(1);
-  }
-
   map<string,log::Logger*> loggers;
   loggers["info"] = &log::info;
   loggers["trace"] = &log::trace;
@@ -112,13 +102,25 @@ int main (int argc, char* argv[]) {
   loggers["fixpoint"] = &log::fixpoint;
   loggers["debug"] = &log::debug;
 
-  if (argc > 3) {
-    char* arg = argv[4];
-    char* str = strtok(arg, ",");
-    do {
-      if (str && loggers[str])
-        loggers[str]->enabled(true);
-    } while ((str = strtok(NULL, ",")) != NULL);
+  set<string> variables;
+  if (argc > 2) {
+    int i = 2;
+    while (argv[i] != NULL) {
+      if (string(argv[i]) == "-v") {
+        ++i;
+        if (i < argc) {
+          char* arg = argv[i];
+          char* str = strtok(arg, ",");
+          do {
+            if (str && loggers[str])
+              loggers[str]->enabled(true);
+          } while ((str = strtok(NULL, ",")) != NULL);
+        }
+      } else {
+        variables.insert(argv[i]);
+      }
+      ++i;
+    }
   }
 
   auto input = antlr3FileStreamNew((pANTLR3_UINT8)argv[1], ANTLR3_ENC_8BIT);
@@ -131,67 +133,24 @@ int main (int argc, char* argv[]) {
   EquationSystem<ZBar> system;
   treeToSystem<ZBar>(ret.tree, system);
 
-  /*
-  // PARSE ARGUMENTS - fixpoint
-  FixpointAlgorithm<ZBar>* algorithm = NULL;
-  if (!strcmp(argv[2], "naive")) {
-    algorithm = new NaiveFixpointAlgorithm<ZBar>(system);
-    log::info << "Naive fixpoint" << endl;
-  } else if (!strcmp(argv[2], "smart")) {
-    algorithm = new SmartFixpointAlgorithm<ZBar>(system);
-    log::info << "Smart fixpoint" << endl;
-  } else {
-    cerr << "Unknown fixpoint algorithm." << endl;
-  }
-
-  // PARSE ARGUMENTS - strat improvement
-  ImprovementOperator<ZBar>* naiveImprovement = new NaiveImprovementOperator<ZBar>();
-  ImprovementOperator<ZBar>* improvement = NULL;
-  if (!strcmp(argv[3], "repeat")) {
-    improvement = new RepeatedImprovementOperator<ZBar>(*naiveImprovement);
-    log::info << "Repeated strategy improvement" << endl;
-  } else if (!strcmp(argv[3], "naive")) {
-    improvement = naiveImprovement;
-    log::info << "Naive strategy improvement" << endl;
-  } else if (!strcmp(argv[3], "smart")) {
-    improvement = new SmartImprovementOperator<ZBar>(system);
-    log::info << "Smart strategy improvement" << endl;
-  } else {
-    cerr << "Unknown strategy improvement algorithm." << endl;
-  }
-  if (!improvement || !algorithm) {
-    exit(1);
-  }
-  */
-
-  log::debug << system << std::endl;
+  log::debug << system << endl;
   system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
-  /*StableVariableAssignment<ZBar> result(system.variableCount(), infinity<ZBar>());
-  ConcreteMaxStrategy<ZBar> strategy(system);
-  IdSet<Variable<ZBar>> s1(system.variableCount());
-  IdSet<Variable<ZBar>> s2(system.variableCount());
-  bool changed = false;
-  s2.clear();
-  s2.invert();
-  do {
-    s1.clear();
-    algorithm->maxFixpoint(system, strategy, result, s2, s1);
-
-    log::debug << result << std::endl;
-
-    s2.clear();
-    changed = improvement->improve(system, strategy, result, s1, s2);
-    log::debug << "Changed: " << (changed ? "true" : "false") << std::endl;
-  } while(changed);*/
-
-
-  DynamicMaxStrategy<ZBar> strategy(system);  
-  DynamicVariableAssignment<ZBar> rho(system, strategy); 
+
+  DynamicMaxStrategy<ZBar> strategy(system);
+  DynamicVariableAssignment<ZBar> rho(system, strategy);
   strategy.setRho(rho);
 
-  for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-    Variable<ZBar>& var = system.variable(i);
-    cout << var.name() << " = " << rho[var] << endl;
+  if (variables.size() > 0) {
+    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+      Variable<ZBar>& var = system.variable(i);
+      if (variables.find(var.name()) != variables.end())
+        cout << var.name() << " = " << rho[var] << endl;
+    }
+  } else {
+    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+      Variable<ZBar>& var = system.variable(i);
+      cout << var.name() << " = " << rho[var] << endl;
+    }
   }
 
   parser -> free(parser);