example1.cpp

/* ********************************************************************** */
/* example1.c: using APRON library  */
/* ********************************************************************** */

/* We illustrate here the use of the APRON interface, at level 1 */

#include "ap_global0.h"
#include "ap_global1.h"

#include "box.h"
#include "oct.h"
#include "pk.h"
#include "pkeq.h"
//#include "apron_ppl.h"

void ex1(ap_manager_t* man)
{
  printf("******************************\n");
  printf("ex1\n");
  printf("Library %s, version %s\n",man->library,man->version);
  printf("******************************\n");

  ap_var_t name_of_dim[6] = {    
    "x","y","z","u","w","v"
  };
  ap_environment_t* env = ap_environment_alloc(&name_of_dim[0],3,&name_of_dim[3],3);

  /* =================================================================== */
  /* Creation of polyhedra 
     1/2x+2/3y=1, [1,2]<=z+2w<=4 */
  /* =================================================================== */

  /* 0. Create the array */
  ap_lincons1_array_t array = ap_lincons1_array_make(env,3);

  /* 1.a Creation of an equality constraint 1/2x+2/3y=1 */
  ap_linexpr1_t expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  ap_lincons1_t cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
    /* Now expr is memory-managed by cons */ 

  /* 1.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_FRAC,1,2,"x",
		       AP_COEFF_S_FRAC,2,3,"y",
		       AP_CST_S_INT,1,
		       AP_END);
  /* 1.c Put in the array */
  ap_lincons1_array_set(&array,0,&cons);
    /* Now cons is memory-managed by array */ 

  /* 2.a Creation of an inequality constraint [1,2]<=z+2w */
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
    /* The old cons is not lost, because it is stored in the array.
       It would be an error to clear it (same for expr). */
  /* 2.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,1,"z",
		       AP_COEFF_S_DOUBLE,2.0,"w",
		       AP_CST_I_INT,-2,-1,
		       AP_END);
  /* 2.c Put in the array */
  ap_lincons1_array_set(&array,1,&cons);
  
//  /* 2.a Creation of an inequality constraint */
//  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
//  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
//    /* The old cons is not lost, because it is stored in the array.
//       It would be an error to clear it (same for expr). */
//  /* 2.b Fill the constraint */ 
//  ap_lincons1_set_list(&cons,
//		       AP_COEFF_S_INT,1,"z",
//		       AP_COEFF_S_DOUBLE,2.0,"w",
//		       AP_CST_I_INT,-2,-1,
//		       AP_END);
//  /* 2.c Put in the array */
//  ap_lincons1_array_set(&array,1,&cons);
//  
  /* 3.a Creation of an inequality constraint by duplication and
       modification z+2w<=4 */
  cons = ap_lincons1_copy(&cons);
  /* 3.b Fill the constraint (by negating the existing coefficients) */ 
  expr = ap_lincons1_linexpr1ref(&cons);
  {
    ap_coeff_t* pcoeff;
    ap_var_t var;
    size_t i;
    ap_linexpr1_ForeachLinterm1(&expr,i,var,pcoeff){
      ap_coeff_neg(pcoeff,pcoeff);
    }
  }
  ap_linexpr1_set_cst_scalar_int(&expr,4);
  /* 3.c Put in the array */
  ap_lincons1_array_set(&array,2,&cons);

  /* 4. Creation of an abstract value */
  ap_abstract1_t abs = ap_abstract1_of_lincons_array(man,env,&array);
  
  fprintf(stdout,"Abstract value:\n");
  ap_abstract1_fprint(stdout,man,&abs);

  /* deallocation */
  ap_lincons1_array_clear(&array);
  
  /* =================================================================== */
  /* Creation of polyhedra 
     x+y+z+w+u=0, 0<= w <= 5, -5<=u<=0, x+y-z-w>=0, */
  /* =================================================================== */
  array = ap_lincons1_array_make(env,6);
  expr = ap_linexpr1_make(env,AP_LINEXPR_DENSE,0);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_linexpr1_set_list(&expr,
		       AP_COEFF_S_INT,1,"x",
		       AP_COEFF_S_INT,1,"y",
		       AP_COEFF_S_INT,1,"z",
		       AP_COEFF_S_INT,1,"w",
		       AP_COEFF_S_INT,1,"u",
		       AP_END);
  ap_lincons1_array_set(&array,0,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,0);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
  ap_linexpr1_set_list(&expr, AP_COEFF_S_INT,1,"w",AP_END);
  ap_lincons1_array_set(&array,1,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,0);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
  ap_linexpr1_set_list(&expr, AP_COEFF_S_INT,-1,"w",AP_CST_S_INT,5, AP_END);
  ap_lincons1_array_set(&array,2,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,0);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
  ap_linexpr1_set_list(&expr, AP_COEFF_S_INT,1,"u",AP_CST_S_INT,5, AP_END);
  ap_lincons1_array_set(&array,3,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,0);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
  ap_linexpr1_set_list(&expr, AP_COEFF_S_INT,-1,"u",AP_END);
  ap_lincons1_array_set(&array,4,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_DENSE,0);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_linexpr1_set_list(&expr,
		       AP_COEFF_S_INT,1,"x",
		       AP_COEFF_S_INT,1,"y",
		       AP_COEFF_S_INT,-1,"z",
		       AP_COEFF_S_INT,-1,"w",
		       AP_END);
  ap_lincons1_array_set(&array,5,&cons);

  ap_abstract1_t abs2 = ap_abstract1_of_lincons_array(man,env,&array);
  
  fprintf(stdout,"Abstract value 2:\n");
  ap_abstract1_fprint(stdout,man,&abs2);

  ap_lincons1_array_clear(&array);

  /* =================================================================== */
  /* Meet and Join */
  /* =================================================================== */
 
  ap_abstract1_t res = ap_abstract1_meet(man,false,&abs,&abs2);
  fprintf(stdout,"Meet:\n");
  ap_abstract1_fprint(stdout,man,&res);
  ap_abstract1_clear(man,&res);

  res = ap_abstract1_join(man,false,&abs,&abs2);
  fprintf(stdout,"Join:\n");
  ap_abstract1_fprint(stdout,man,&res);
  ap_abstract1_clear(man,&res);

  /* =================================================================== */
  /* Assignement */
  /* =================================================================== */
 
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,0);
  ap_linexpr1_set_list(&expr,
		       AP_COEFF_S_INT,-3,"w",
		       AP_COEFF_S_DOUBLE,2.625,"z",
		       AP_CST_I_INT,0,3,
		       AP_END);
  fprintf(stdout,"Assignement (side-effect) in abstract value of u by expression:\n");
  ap_linexpr1_fprint(stdout,&expr);

  abs = ap_abstract1_assign_linexpr(man,true,&abs,"u",&expr,NULL);
  fprintf(stdout,"\n");
  ap_abstract1_fprint(stdout,man,&abs);
  ap_linexpr1_clear(&expr);

  /* deallocation */
  ap_abstract1_clear(man,&abs);
  ap_abstract1_clear(man,&abs2);

  ap_environment_free(env);
}




void ex2(ap_manager_t* man)
{
  printf("******************************\n");
  printf("ex2\n");
  printf("Library %s, version %s\n",man->library,man->version);
  printf("******************************\n");
  ap_var_t name_of_dim[6] = {    
    "x","y","z","u","w","v"
  };
  ap_var_t tab[2] = {    
    "x","y"
  };
  ap_environment_t* env = ap_environment_alloc(&name_of_dim[0],3,&name_of_dim[3],3);

  /* =================================================================== */
  /* Creation of polyhedra 
     -39x + 40y >= 0
     -6x - 20y + 85 >= 0
     x >= 0  */
  /* =================================================================== */

  /* 0. Create the array */
  ap_lincons1_array_t array = ap_lincons1_array_make(env,3);

  /* 1.a Creation of constraint -39x + 40y >= 0 */
  ap_linexpr1_t expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  ap_lincons1_t cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
    /* Now expr is memory-managed by cons */ 

  /* 1.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-39,"x",
		       AP_COEFF_S_INT,40,"y",
		       AP_CST_S_INT,0,
		       AP_END);
  /* 1.c Put in the array */
  ap_lincons1_array_set(&array,0,&cons);
    /* Now cons is memory-managed by array */ 

  /* 2.a Creation of an inequality constraint -6x - 20y + 85 >= 0 */
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
    /* The old cons is not lost, because it is stored in the array.
       It would be an error to clear it (same for expr). */
  /* 2.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-6,"x",
		       AP_COEFF_S_INT,-20,"y",
		       AP_CST_S_INT,85,
		       AP_END);
  /* 2.c Put in the array */
  ap_lincons1_array_set(&array,1,&cons);

  /* 3.a Creation of an inequality constraint x >= 0 */
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,1);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
    /* The old cons is not lost, because it is stored in the array.
       It would be an error to clear it (same for expr). */
  /* 3.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,1,"x",
		       AP_CST_S_INT,0,
		       AP_END);
  /* 3.c Put in the array */
  ap_lincons1_array_set(&array,2,&cons);
  
  ap_abstract1_t abs = ap_abstract1_of_lincons_array(man,env,&array);
  fprintf(stdout,"Abstract value:\n");
  ap_abstract1_fprint(stdout,man,&abs);
  ap_abstract1_t abs2 = ap_abstract1_fold(man,false,&abs,tab,2);
  fprintf(stdout,"Abstract value 2:\n");
  ap_abstract1_fprint(stdout,man,&abs2);

  ap_lincons1_array_clear(&array);
  ap_abstract1_clear(man,&abs);
  ap_abstract1_clear(man,&abs2);
  ap_environment_free(env);
}




void ex3(ap_manager_t* man)
{
  printf("******************************\n");
  printf("ex3\n");
  printf("Library %s, version %s\n",man->library,man->version);
  printf("******************************\n");
  ap_var_t name_of_dim[6] = {    
    "x","y","z","u","w","v"
  };
//  ap_var_t tab[2] = {    
//    "x","y"
//  };
  ap_environment_t* env = ap_environment_alloc(&name_of_dim[0],6,NULL,0);
  /* =================================================================== */
  /* Creation of polyhedra 
     -39x + 40y = 0
     -3x - 10z + 43 = 0
     -6x - 20y + 86 >= 0 
  */
  /* =================================================================== */

  /* 0. Create the array */
  ap_lincons1_array_t array = ap_lincons1_array_make(env,1);

  /* 1.a Creation of constraint -39x + 40y = 0 */
  ap_linexpr1_t expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  ap_lincons1_t cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
    /* Now expr is memory-managed by cons */ 

  /* 1.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-39,"x",
		       AP_COEFF_S_INT,40,"y",
		       AP_CST_S_INT,0,
		       AP_END);
  /* 1.c Put in the array */
  ap_lincons1_array_set(&array,0,&cons);
    /* Now cons is memory-managed by array */ 

  ap_abstract1_t abs = ap_abstract1_of_lincons_array(man,env,&array);
  fprintf(stdout,"Abstract value:\n");
  ap_abstract1_fprint(stdout,man,&abs);
  ap_generator1_array_t garray = ap_abstract1_to_generator_array(man,&abs);
  ap_generator1_array_fprint(stdout,&garray);
  ap_generator1_array_clear(&garray);

  /* 2.a Creation of an equality constraint -3x - 10z + 43 = 0 */
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
    /* The old cons is not lost, because it is stored in the array.
       It would be an error to clear it (same for expr). */
  /* 2.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-3,"x",
		       AP_COEFF_S_INT,-10,"z",
		       AP_CST_S_INT,43,
		       AP_END);
  /* 2.c Put in the array */
  ap_lincons1_array_set(&array,0,&cons);

  fprintf(stdout,"Adding constraints:\n");
  ap_lincons1_array_fprint(stdout,&array);  
  abs = ap_abstract1_meet_lincons_array(man,true,&abs,&array);
  fprintf(stdout,"Abstract value:\n");
  ap_abstract1_fprint(stdout,man,&abs);

  /* 3.a Creation of an inequality constraint -6x - 20y + 86 >= 0 */
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_SUPEQ,&expr,NULL);
    /* The old cons is not lost, because it is stored in the array.
       It would be an error to clear it (same for expr). */
  /* 2.b Fill the constraint */ 
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-6,"x",
		       AP_COEFF_S_INT,-20,"y",
		       AP_CST_S_INT,86,
		       AP_END);
  /* 2.c Put in the array */
  ap_lincons1_array_set(&array,0,&cons);
  fprintf(stdout,"Adding constraints:\n");
  ap_lincons1_array_fprint(stdout,&array);  
  abs = ap_abstract1_meet_lincons_array(man,true,&abs,&array);
  fprintf(stdout,"Abstract value:\n");
  ap_abstract1_fprint(stdout,man,&abs);

  ap_lincons1_array_clear(&array);

     
  /* =================================================================== */
  /* Creation of polyhedra 
     -39x + 40u = 0
     u = y
     v = x+z
     -6v - 14z + 86 = 0 
  */
  /* =================================================================== */

  /* 0. Create the array */
  array = ap_lincons1_array_make(env,4);

  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-39,"x",
		       AP_COEFF_S_INT,40,"u",
		       AP_CST_S_INT,0,
		       AP_END);
  ap_lincons1_array_set(&array,0,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-1,"u",
		       AP_COEFF_S_INT,1,"y",
		       AP_CST_S_INT,0,
		       AP_END);
  ap_lincons1_array_set(&array,1,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-1,"v",
		       AP_COEFF_S_INT,1,"x",
		       AP_COEFF_S_INT,1,"y",
		       AP_CST_S_INT,0,
		       AP_END);
  ap_lincons1_array_set(&array,1,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-1,"v",
		       AP_COEFF_S_INT,1,"x",
		       AP_COEFF_S_INT,1,"z",
		       AP_CST_S_INT,0,
		       AP_END);
  ap_lincons1_array_set(&array,2,&cons);
  expr = ap_linexpr1_make(env,AP_LINEXPR_SPARSE,2);
  cons = ap_lincons1_make(AP_CONS_EQ,&expr,NULL);
  ap_lincons1_set_list(&cons,
		       AP_COEFF_S_INT,-6,"v",
		       AP_COEFF_S_INT,-14,"z",
		       AP_CST_S_INT,86,
		       AP_END);
  ap_lincons1_array_set(&array,3,&cons);

  ap_abstract1_t abs2 = ap_abstract1_of_lincons_array(man,env,&array);
  fprintf(stdout,"Abstract value 2:\n");
  ap_abstract1_fprint(stdout,man,&abs2);
  ap_lincons1_array_clear(&array);

  ap_abstract1_canonicalize(man,&abs2);
  fprintf(stdout,"Abstract value 2:\n");
  ap_abstract1_fprint(stdout,man,&abs2);

  ap_abstract1_t abs3 = ap_abstract1_join(man,false,&abs,&abs2);
  fprintf(stdout,"Abstract value 3 (join of 1 and 2):\n");
  ap_abstract1_fprint(stdout,man,&abs3);

  ap_abstract1_t abs4 = ap_abstract1_meet(man,false,&abs,&abs2);
  fprintf(stdout,"Abstract value 3 (meet of 1 and 2):\n");
  ap_abstract1_fprint(stdout,man,&abs4);


  ap_abstract1_clear(man,&abs);
  ap_abstract1_clear(man,&abs2);
  ap_abstract1_clear(man,&abs3);
  ap_abstract1_clear(man,&abs4);

  ap_environment_free(env);
}

int main()
{
  ap_manager_t* man;

  man = box_manager_alloc();
  ex1(man);
  ex2(man);
  ap_manager_free(man);

  man = oct_manager_alloc();
  ex1(man);
  ex2(man);
  ap_manager_free(man);

  man = pk_manager_alloc(true);
  ex1(man);
  ex2(man);
  ex3(man);
  ap_manager_free(man);
  
//  man = ap_ppl_poly_manager_alloc(true);
//  ex1(man);
//  ex2(man);
//  ex3(man);
//  ap_manager_free(man);
//  
  man = pkeq_manager_alloc();
  ex2(man);
  ex3(man);
  ap_manager_free(man);
  
//  man = ap_ppl_grid_manager_alloc();
//  ex2(man);
//  ex3(man);
//  ap_manager_free(man);
}
//