// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************

module Presburger(
    int x, y, z
)  {
    nothing;
} satisfies {

    // --- " <= " is a total order
    ord01 : assert x <= x;
    ord02 : assert x<=y & y<=x -> x==y;
    ord03 : assert (x <= y) & (y <= z) -> (x <= z);
    ord04 : assert (x <= y) | (y <= x);

    // --- "<" is a strict total order
    ord05 : assert !(x < x);
    ord06 : assert (x < y) -> !(y < x);
    ord07 : assert (x < y) & (y < z) -> (x<z);
    ord08 : assert (x < y) | (x==y) | (y<x);

    // --- defining numeric relations by "<"
    ord09 : assert (x <= y) <-> (x<y) | (x==y);
    ord10 : assert (x>y) <-> (y<x);
    ord11 : assert (x>=y) <-> !(x<y);
    ord12 : assert (x==y) <-> !(x<y) & !(y<x);

    // --- defining numeric relations by " <= "
    ord13 : assert (x<y) <-> (x <= y) & !(y <= x);
    ord14 : assert (x>y) <-> !(x <= y);
    ord15 : assert (x>=y) <-> (y <= x);
    ord16 : assert (x==y) <-> (x <= y) & (y <= x);

    // --- ring axioms ---------------------
    r01 : assert x+0==x;
    r02 : assert x+y==y+x;
    r03 : assert (x+y)+z == x+(y+z);
    r04 : assert x+(0-x)==0;

    // --- arithmetic laws ---------------------
    arith00 : assert x*0==0;
    arith01 : assert (x+y)-x==y;
    arith03 : assert x-(y+z) == x-y-z;
    arith04 : assert 1*x == x;
    arith05 : assert 2*x == x+x;
    arith06 : assert 3*x == x+x+x;

    // --- monotonicity ------------------------
    mono00 : assert (x==y) <-> (x+z==y+z);
    mono01 : assert (x <= y) <-> (x+z <= y+z);
    mono02 : assert (x<y) <-> (x+z<y+z);
    mono03 : assert (x+y==0) & (0 <= x) & (0 <= y) -> (x==0) & (y==0);
    mono04 : assert (x+y==x) -> (y==0);
    mono05 : assert (x<y) & (0 <= z) -> (x<y+z);
    mono06 : assert (x<y) & (y <= z) -> (x<z);

    // --- other stuff ------------------------
    div2 : assert exists y:int. ((x == y+y) | (x == y+y+1));
    div3 : assert exists y:int. ((x == y+y+y) | (x == y+y+y+1) | (x == y+y+y+2));
    div4 : assert exists y:int. ((x == y+y+y+y) | (x == y+y+y+y+1) | (x == y+y+y+y+2) | (x == y+y+y+y+3));
    div5 : assert exists y:int. ((x == y+y+y+y+y) | (x == y+y+y+y+y+1) | (x == y+y+y+y+y+2) | (x == y+y+y+y+y+3) | (x == y+y+y+y+y+4));
    unbounded : assert exists y:int. (x<y);
}