From 86ca7448849aaaea6db34b1d2bcf8d99d7d7b12c Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au>
Date: Mon, 22 Oct 2012 14:44:57 +1100
Subject: Okay, the solver is now correct.

It runs in two separate passes:
 - improve strategy (for all)
 - evaluate fixpoint

Unfortunately this loses out on locality at the moment.

I really want a local solver, so I'll have to see what I can do about
that.
---
 impl/main.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'impl/main.cpp')

diff --git a/impl/main.cpp b/impl/main.cpp
index e3e0ae3..84f17dd 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -140,6 +140,20 @@ int main (int argc, char* argv[]) {
   log::debug << system << endl;
   system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
 
+  IdMap<Variable<ZBar>,ZBar> result = solve_for(system);
+  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() << " = " << result[var] << endl;
+    }
+  } else {
+    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+      Variable<ZBar>& var = system.variable(i);
+      cout << var.name() << " = " << result[var] << endl;
+    }
+  }
+  /*
   DynamicMaxStrategy<ZBar> strategy(system);
   DynamicVariableAssignment<ZBar> rho(system, strategy);
   strategy.setRho(rho);
@@ -156,6 +170,7 @@ int main (int argc, char* argv[]) {
       cout << var.name() << " = " << rho[var] << endl;
     }
   }
+  */
 
   parser -> free(parser);
   tokens -> free(tokens);
-- 
cgit v1.2.3