Simple structure sharing

This button checks the two examples in this page:
In this example the intermediary terms are irellevant. b must be instantiated to true. Consequently it simplifies in 0.810 seconds. 

value f,g,h : int * int --> int;

Exists b : bool . Forall x0 : int . 
  let
      x1 = f(x0,x0);

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);		 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);		

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);		

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);		

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);	

      x2 = g(x1,x1);
      x3 = if b then h(x0,x2) else g(x2,x2);
  in
      (x0 = x2 --> x3 = h(x0,x0))
This formula makes essential use of all equalities. A congruence closure directing equalities the wrong direction can suffer from exponential run times. Our implementation does not suffer from this problem. It is verified in 0.32 seconds. 
Forall x0 : int . 
  let
      x1 = f(x0,x0);
      y  = x1;

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1); 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1); 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1); 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1); 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1); 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      
      x1 = f(x1,x1); 

      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1);
      x1 = f(x1,x1);      x1 = f(x1,x1);      x1 = f(x1,x1); 
      x1 = f(x1,x1);      x1 = f(x1,x1); 
  in
      (x0 = y --> x0 = x1)
Back to the top of this page.