add_infl x y for side x y to deal with cycles between globals

TODO: this makes every y immediately a wpoint :(

~~~ globs.c
int a, b; // globals, initial value 0
int main(){
  /* 1 */ a = b+1;
  /* 2 */ b = a+1;
}
~~~
Currently does not terminate with td3 b/c of how we do cycle detection in destabilize
`./goblint -v --enable ana.int.interval --html --sets solver td3 --enable exp.earlyglobs globs.c`
Terminates with td3 with space b/c the cycle is reduced?
`./goblint -v --enable ana.int.interval --html --sets solver td3 --enable exp.earlyglobs globs.c --enable exp.solver.td3.space`
Terminates with slr3t (b/c of prios)
`./goblint -v --enable ana.int.interval --html --sets solver slr3t --enable exp.earlyglobs globs.c`

Example for td3 w/o space:
// solve 2
//   eval 2 1
//     infl 1 2
eval 1 b -> [0,0]
  infl b 1
side 1 a [1,1] -> [0,1]
  effects (1,a)
  destabilize ~side:a a // nothing to do yet
eval 2 a -> [0,1]
  infl a 2
side 2 b [1,2] -> [0,2]
  effects (2,b)
  destabilize ~side:b b
    remove stable 1
    destabilize ~side:b 1
      remove stable 2
      destabilize ~side:b 2
        add wpoint b // since mem effects (2,b)
// 1 and 2 are now not stable, and only b is a wpoint
eval 1 b -> [0,2]
  infl b 1
side 1 a [1,3] -> [0,3]
  destabilize ~side:a a
    remove stable 2
    destabilize ~side:a 2
eval 2 a -> [0,3]
  infl a 2
side 2 b [1,4] -> [0,∞]
  ..
// b stable, but a will not become a wpoint and just keep increasing

Change:
1. add `infl x y` for each `side x y`
2. make wpoint if `side-var=x` instead of `mem effects (x, side-var)`
3. also only widen for space if wpoint

Problem: This makes every y immediately a wpoint :(

The following should ideally not widen on g:

~~~ side.c
int g;
int main(){
  /* 1 */ g = 1;
  /* 2 */ g = 2;
  /* 3 */ g = 3;
}
~~~

src/solvers/td3.ml

@@ -35,7 +35,6 @@ module WP =
       let called = HM.create  10 in
       let rho    = HM.create  10 in
       let wpoint = HM.create  10 in
-      let effects = HPM.create 10 in
       let cache_sizes = ref [] in
 
       let add_infl y x =
@@ -45,7 +44,7 @@ module WP =
       let rec destabilize ?side x =
         if tracing then trace "sol2" "destabilize %a on %i\n" S.Var.pretty_trace x (S.Var.line_nr x);
         if HM.mem called x then assert (HM.find infl x = VS.empty); (* TODO if this is really true, we can remove the check below *)
-        Option.may (fun z -> if HPM.mem effects (x,z) then HM.replace wpoint z ()) side;
+        Option.may (fun z -> if S.Var.equal z x then HM.replace wpoint z ()) side;
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y ->
@@ -117,7 +116,7 @@ module WP =
         tmp
       and side x y d = (* only to variables y w/o rhs *)
         if tracing then trace "sol2" "side to %a on %i (wpx: %b) ## value: %a\n" S.Var.pretty_trace y (S.Var.line_nr y) (HM.mem rho y) S.Dom.pretty d;
-        HPM.replace effects (x,y) ();
+        add_infl x y;
         if S.system y <> None then (
           ignore @@ Pretty.printf "side-effect to unknown w/ rhs: %a, contrib: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
         );
@@ -136,7 +135,7 @@ module WP =
           (* assert (S.Dom.leq old j);
           assert (S.Dom.leq old w);
           assert (S.Dom.leq j w); *)
-          HM.replace rho y ((if HM.mem wpoint y || space then S.Dom.widen old else identity) (S.Dom.join old d));
+          HM.replace rho y ((if HM.mem wpoint y then S.Dom.widen old else identity) (S.Dom.join old d));
           HM.replace stable y ();
           if HM.mem wpoint y then
             destabilize y (* we already are a wpoint, so no need to propagate it anymore *)