(************************************************************ * * PolyOp * * National University of Singapore * * Author: Etienne ANDRE * Created: 2011/04/27 * Last modified: 2011/05/30 * ************************************************************) (* WARNING: only one instruction at a time can be uncommented to call PolyOp *) (************************************************************ NON RECURSIVE ************************************************************) (* nothing *) (* and (p1 <= p2, p2 <= p1) *) (* and ((p1 <= p2), (p2 <= p1)) *) (* elapsing (p1) in (p1 = 1 & p2 = 2) *) (* elapsing (p1) in (p1 = 5 & p2 >= 2) *) (* elapsing (p1) in (p1 = 5 & p2 >= p1) *) (* elapsing (p1, p3) in (p1 = 5 & p2 >= p1 & p3 = 0) *) (* elapsing (x1) in (p1 <= x1 & x1 <= p2 ) *) (* equal (true, True) *) (* equal (true, false) *) (* equal (true, p1 = p1) *) (* equal (true, p1 = 57) *) (* equal (p1 = p2, (p1 <= p2 & p2 <= p1 + 1 & p2 - 2 <= p1 - 2)) *) (* equal (p1 = p2, (p1 <= p2 & p2 <= p1 + 1 & p2 - 2 < p1 - 2)) *) (* equal true, True *) (* included true in false *) (* included false in true *) (* included p1 = p2 in (p1 <= p2 & p2 <= p1 + 1 & p2 - 2 < p1 - 2) *) (* included (p1 <= p2 & p2 <= p1 + 1 & p2 - 2 < p1 - 2) in (p1 = p2) *) (* included (p1 <= p2 & p3 >= 2) in (p3 >= 1) *) (* included p1 <= p2 & p3 >= 2 in p3 >= 1 *) (* included (p3 >= 1) in (p1 <= p2 & p3 >= 2) *) (* hide p1 in true *) (* hide p1 in False *) (* hide (p1) in (False) *) (* hide p1 in p1 = 0 *) (* hide p1 in p1 = 0 & p2 = 5 *) (* hide p2 in (p1 <= p2 & p2 <= p3) *) (* satisfiable True *) (* satisfiable (False) *) (* satisfiable (p1 <= p2 & p2 <= p3) *) (* satisfiable p1 <= p2 & p2 <= p1 & true *) (* satisfiable p1 <= p2 & p1 > p2 *) (* simplify True *) (* simplify p1 = p2 *) (* simplify p1 = p2 & p2 = p3 *) (* simplify p1 <= p2 & p2 >= p3 *) (* simplify p1 <= p2 & p1 > p2 *) (* simplify p1 <= p3 & p1 > p2 & p1 > 2 *) (* simplify (p1 <= p3 & p1 > p2 & (p1 > 2)) *) (* simplify p1 <= p2 & p2 <= p1 *) (* simplify p1 <= p2 & p2 <= p1 & true *) (************************************************************ RECURSIVE ************************************************************) (* and (p1 <= p2, and (true & p2 <= p1)) *) (* and (p2 <= p1, hide p3 in (p1 <= p3 & p3 <= p2)) *) (*and ( p1 <= x1 & x1 <= p2 & p4 <= p1 , hide p3 in (p1 <= p3 & p3 <= p4) )*) (*elapsing (x1) in ( elapsing (x2) in (x1 = p1 & x2 = p2) )*) (*equal simplify p1 <= p2 & p2 <= p1 & true , hide (x1, p4) in and ( p1 <= x1 & x1 <= p2 & p4 <= p1 , hide p3 in (p2 <= p3 & p3 <= p1) )*) (*included hide (x1, p4) in and ( p1 <= x1 & x1 <= p2 & p4 <= p1 , hide p3 in (p2 <= p3 & p3 <= p1) ) in simplify p1 <= p2 & p2 <= p1 & true*) (* hide p1 in (hide p1 in true) *) (* satisfiable hide p1 in true *) (* satisfiable (hide p1 in true) *) (* included hide p1 in true in hide p1 in true *) (* included (hide p1 in true) in (hide p1 in true) *) (* included (hide p1 in true) in (and (p2 = p3, p3 = p4)) *) (*simplify hide (x1, p4) in and ( p1 <= x1 & x1 <= p2 & p4 <= p1 , hide p3 in (p2 <= p3 & p3 <= p1) )*)