From a3860a4cd6ca6a1ee664634ea472b5487535b2b5 Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@carlo-laptop>
Date: Wed, 24 Oct 2012 10:34:15 +1100
Subject: Add a fix for mutually-recursive infinite things

So now it will solve correctly for
  x = y + 1
  y = max(0, x + 1)

I also added in tests for this (and a slightly different form with `x`
going through another variable, `z`, for indirection).

The tests will also stop now after five seconds of execution. If they
can't be solved in five seconds then they're considered a failure.
---
 impl/VariableAssignment.hpp | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'impl/VariableAssignment.hpp')

diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index 21226ac..19403a8 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -55,15 +55,26 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
     return _values[var];
   }
 
-  void invalidate(const Variable<Domain>& x) {
+  void invalidate(const Variable<Domain>& x, bool also_solve=true) {
     log::fixpoint << indent() << "Invalidating " << x << std::endl;
     if (_stable.contains(x)) {
       _stable.remove(x);
       _values[x] = unknown(infinity<Domain>());
 
-      solve(x);
-      if (_values[x] == infinity<Domain>())
-        _values[x] = _values[x].asKnown();
+      IdSet<Variable<Domain> > infl = _influence[x];
+      for (typename IdSet<Variable<Domain> >::iterator
+             it = infl.begin(),
+             ei = infl.end();
+           it != ei;
+           ++it) {
+        invalidate(_system.variable(*it), false);
+      }
+      
+      if (also_solve) {
+        solve(x);
+        if (_values[x] == infinity<Domain>())
+          _values[x] = _values[x].asKnown();
+      }
     }
   }
 
-- 
cgit v1.2.3