% =============================================================
%
% ICanSolve Demo
%
% Several of the capabilities of ICS are demonstrated.
%
% ==============================================================


% Example: Deciding equality over uninterpreted Functions (UIF)
% using congruence closure

reset.
assert f(f(f(x))) = f(x).
ctxt.
assert f(f(f(f(f(x))))) = f(x).
can f(f(f(f(f(x))))).
can f(x).


% Example: Combination of Arithmetic and UIF.

reset.
assert z = f(x - y).
assert x = z + y.
assert -y <> -(x - f(f(z))). 


% Example: Combination of Arrays, Arithmetic, and UIF.
						      
reset.								  
assert x+2=y.
assert f(a[x:=3][y - 2]) = f(y - x +1).


% Example: Combinatory Logic

reset.
def True := lambda x, y: x.
def False := lambda x, y: y.

simplify True = False.
assert True = False.

assert lambda x: x = lambda x: (x + 1).


% Example: Combination of Arithmetic, S-expressions, and UIF

reset.
assert 2 * car(x) - 3 * cdr(x) = f(cdr(x)).
can f(cons(4 * car(x) - 2 * f(cdr(x)), y)).
can f(cons(6 * cdr(x), y)).

   
% Example: Constraints

reset.
sig x : int.
assert x >= 1.
assert x <= 3.
show.
assert x <> 1.
show.
assert x <> 2.
show.

% Example: Nonlinear arithmetic

reset.
assert u = x^2 * y.
assert v = x * u^2.
assert u * y <> v * x.


% Example: Dynamic Contexts

symtab.
ctxt@s3.
assert@s3 x <> 2.
ctxt@s6.
restore s3.
ctxt.
remove s1.


% Example: Equalities, Inequalities,
%  Disequalities in the Combination of Arithmetic
%  and the theory of UIF

reset.
sig v0 : int.
sig v1 : int.
sig i : int.
assert 1 +  v0 = v1.
assert i <= v1 - 1.
assert i > v0 - 1.
assert f(v0) = 0.
assert f(i) <> 0.


% Example: Inequalities and S-expressions

reset.
assert x <= car(a).
assert car(a) >= car(cons(x,b)).


% Example: Disequalities for generating new equalities.

reset.
assert  a[j:=x] = b[k:=y].
assert i <> j.
assert i = k.
assert a[i] <> y.



% Example: Bitvectors

reset.

sig x : bitvector[7].
sig y : bitvector[5].

symtab.

can (x ++ y)[7:9].
can (y ++ x)[4:7].

sig x2 : bitvector[2].
sig x3 : bitvector[3].

solve bv x2 ++ 0b10 = 0b10 ++ x2.
solve bv x3 ++ 0b10 = 0b10 ++ x3.

assert u = v.
assert u = 0b010 ++ x3.


% Example: Gaussian Elimination  
reset.   
assert
 -6*x1 +2*x2 +7*x3 +5*x4 +2*x5 - 1*x6 - 10*x7 - 10*x8 +5*x9 +2*x10 +5*x11 - 6*x12 = 65.
assert
  0*x1 +9*x2 +0*x3 - 9*x4 +7*x5 +1*x6 - 2*x7 - 9*x8 - 5*x9 +3*x10 - 4*x11 - 8*x12 = -168.
assert
  4*x1 - 4*x2 +9*x3 +3*x4 - 6*x5 +6*x6 - 7*x7 +7*x8 +0*x9 - 5*x10 +9*x11 - 6*x12 = 6.
assert
 -6*x1 +7*x2 - 1*x3 - 8*x4 - 8*x5 +5*x6 - 7*x7 - 9*x8 - 2*x9 - 5*x10 - 4*x11 +0*x12 = -478.
assert
  1*x1 - 10*x2 +1*x3 - 8*x4 +3*x5 - 8*x6 - 8*x7 +4*x8 +8*x9 +2*x10 - 2*x11 +2*x12 = -201.
assert
 -9*x1 - 7*x2 +3*x3 - 5*x4 +7*x5 +0*x6 - 2*x7 +0*x8 +6*x9 +9*x10 +9*x11 +5*x12 = 11.
assert
 -8*x1 +1*x2 - 8*x3 - 1*x4 +8*x5 +2*x6 - 2*x7 - 9*x8 - 8*x9 - 4*x10 +1*x11 +7*x12 = -198.
assert
  4*x1 - 5*x2 - 3*x3 - 6*x4 +7*x5 - 7*x6 +6*x7 - 9*x8 +6*x9 - 8*x10 - 7*x11 +5*x12 = 103.
assert
 -5*x1 - 3*x2 - 3*x3 - 10*x4 - 10*x5 - 5*x6 - 9*x7 - 1*x8 - 3*x9 - 1*x10 - 3*x11 - 3*x12 = -736.
assert
  0*x1 +0*x2 +1*x3 +6*x4 +8*x5 +9*x6 - 1*x7 +5*x8 - 6*x9 - 10*x10 - 5*x11 +0*x12 = 181.
assert
  3*x1 - 10*x2 - 3*x3 +2*x4 +7*x5 - 8*x6 +0*x7 - 7*x8 +8*x9 - 5*x10 - 1*x11 +4*x12 = 173.
assert
  7*x1 - 1*x2 +0*x3 - 1*x4 +1*x5 +8*x6 - 10*x7 - 6*x8 +1*x9 +8*x10 - 10*x11 +1*x12 = -95.
									  
find la x1.
find la x2.


% Example: Chain of equalities

reset.
assert x0 = x1. 
assert  x1 = x2. 
assert  x2 = x3. 
assert  x3 = x4. 
assert  x4 = x5. 
assert  x5 = x6. 
assert  x6 = x7. 
assert  x7 = x8.
assert  x8 = x9. 
assert x9 = x10. 
assert  x10 = x11. 
assert  x11 = x12. 
assert  x12 = x13. 
assert  x13 = x14. 
assert  x14 = x15. 
assert  x15 = x16. 
assert x16 = x17. 
assert  x17 = x18. 
assert  x18 = x19.
assert  x19 = x20. 
assert  x20 = x21. 
assert  x21 = x22. 
assert  x22 = x23. 
assert x23 = x24. 
assert  x24 = x25. 
assert  x25 = x26.
assert  x26 = x27.
 assert  x27 = x28. 
assert  x28 = x29.
 assert  x29 = x30. 
assert x30 = x31. 
assert  x31 = x32. 
assert  x32 = x33. 
assert  x33 = x34. 
assert  x34 = x35. 
assert  x35 = x36. 
assert  x36 = x37. 
assert x37 = x38. 
assert  x38 = x39. 
assert  x39 = x40. 
assert  x40 = x41. 
assert  x41 = x42. 
assert  x42 = x43. 
assert  x43 = x44. 
assert  x44 = x45.
assert x45 = x0.

%Example: Chain of Inequalities

reset.
assert x0 < x1. 
assert x1 < x2.
assert x2 < x3.
assert x3 < x4. 
assert x4 < x5.
assert x5 < x6. 
assert x6 < x7.
assert x7 < x8.
assert x8 < x9.
assert x9 < x10.
assert x10 < x11.
assert x11 < x12.
assert x12 < x13.
assert x13 < x14.
assert x14 < x15.
assert x15 < x16. 
assert x16 < x17.
assert x17 < x18.
assert x18 < x19.
assert x19 < x0.

%Example 14 Sat solver

reset.
sat [p & q] | r.

reset.
sat [x > 2 | x < 4 | p] & 2 * x > 6.