formal_lp/lp_example/out_test.hl

   1 module Lp = struct
   2 let target = `&3 * zz_x + -- &1 * zz_y`;;
   3 let target_bound = `-- &6938 / &10000`;;
   4 let precision_constant = Int 100000;;
   5 let ineqs = [
   6 ASSUME (mk_le_ineq (mk_linear [(mk_real_int64 100000L); (mk_real_int64 100000L); (mk_real_int64 100000L); ] ["zz_x"; "zz_y"; "z"; ])(mk_real_int64 314160L)), (mk_real_int64 150000L);
   7 ASSUME (mk_le_ineq (mk_linear [(mk_real_int64 100000L); (mk_real_int64 141421L); (negate (mk_real_int64 100000L)); ] ["zz_x"; "zz_y"; "z"; ])(mk_real_int64 173206L)), (mk_real_int64 150000L);
   8 ];;
   9 let target_vars = [
  10 ASSUME (mk_le_ineq (mk_linear [(mk_real_int64 100000L); ] ["zz_y"; ])(mk_real_int64 1000000L)), (mk_real_int64 50000L);
  11 ASSUME (mk_le_ineq (mk_linear [(negate (mk_real_int64 100000L)); ] ["zz_y"; ])(negate (mk_real_int64 173205L))), (mk_real_int64 46213200000L);
  12 ];;
  13
  14
  15 let var_ineqs = [
  16 ];;
  17 let start = Sys.time();;
  18 let result = prove_lp ineqs var_ineqs target_vars target_bound precision_constant;;
  19 end;;
  20 Sys.time() -. Lp.start;;
  21 concl (Lp.result);;