LP_arith/lp_tests.ml

   1 let rec_seq = ` !x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
   2   x3 = abs(x2) - x1 /\ x4 = abs(x3) - x2 /\ x5 = abs(x4) - x3 /\
   3   x6 = abs(x5) - x4 /\ x7 = abs(x6) - x5 /\
   4   x8 = abs(x7) - x6 /\ x9 = abs(x8) - x7 /\ x10 = abs(x9) - x8 /\
   5   x11 = abs(x10) - x9 ==> x1 = x10 /\ x2 = x11`;;
   6
   7 let test_std =  `!a b c d.
   8   ((&0 + &1 * a + &0 * b + &0 * c + &0 * d >= &0)
   9    /\
  10    (&0 + &0 * a + &1 * b + &0 * c + &0 * d >= &0)
  11    /\
  12    (&0 + &0 * a + &0 * b + &1 * c + &0 * d >= &0)
  13    /\
  14    (&0 + &0 * a + &0 * b + &0 * c + &1 * d >= &0)
  15    /\
  16    (&0 + &3008 * a + &20980 * b + (-- &97775) * c + (-- &101225) * d >= &0)
  17    /\
  18    (&0 + &3985 * a + &25643 * b + (-- &135871) * c + (-- &130580) * d >= &0)
  19    /\
  20    (&0 + &4324 * a + &26978 * b + (-- &133655) * c + (-- &168473) * d >= &0)
  21    /\
  22    (&0 + &3534 * a + &25361 * b + (-- &46243) * c + (-- &100407) * d >= &0)
  23    /\
  24 (&0 + &8836 * a + &40796 * b + (-- &176661) * c + (-- &215616) * d >= &0)
  25    /\
  26    (&0 + &5376 * a + &37562 * b + (-- &182576) * c + (-- &217615) * d >= &0)
  27    /\
  28    (&0 + &4982 * a + &33088 * b + (-- &98880) * c + (-- &167278) * d >= &0)
  29    /\
  30    (&0 + &4775 * a + &39122 * b + (-- &136701) * c + (-- &193393) * d >= &0)
  31    /\
  32    (&0 + &8046 * a + &42958 * b + (-- &225138) * c + (-- &256575) * d >= &0)
  33    /\
  34    (&0 + &8554 * a + &48955 * b + (-- &257370) * c + (-- &312877) * d >= &0)
  35    /\
  36    (&0 + &6147 * a + &45514 * b + (-- &165274) * c + (-- &227099) * d >= &0)
  37    /\
  38    (&0 + &8366 * a + &55140 * b + (-- &203989) * c + (-- &321623) * d >= &0)
  39    /\
  40    (&0 + &13479 * a + &68037 * b + (-- &174270) * c + (-- &341743) * d >= &0)
  41    /\
  42    (&0 + &21808 * a + &78302 * b + (-- &322990) * c + (-- &487539) * d >= &0)
  43    /\
  44    (&1 + (-- &8554 / &10000) * a + (-- &48955 / &10000) * b + &0 * c + &0 * d >= &0)
  45    /\
  46    (&1 + &0 * a + &0 * b + (-- &257370 / &10000) * c + (-- &312877 / &10000) * d >= &0)) ==>
  47   &1 * a + &1 / &2 * b + &1 / &3 * c + &1 / &4 * d <= &2057990000 / &1743360801`;;
  48
  49 let gale = `~(?T14 T24 T25 T35 T46 T47 T57 T58.
  50                 T14 < &20 /\
  51                 T24 + T25 < &20 /\
  52                 T35 < &20 /\
  53                 T14 + T24 - T46 - T47 = &0 /\
  54     T25 + T35 - T57 - T58 = &0 /\
  55     T46 > &10 /\
  56     T47 + T57 > &20 /\
  57     T58 > &30 /\
  58     T14 < &30 /\
  59     T24 < &20 /\
  60     T25 < &10 /\
  61     T35 < &10 /\
  62     T46 < &10 /\
  63     T47 < &2 /\
  64     T57 < &20 /\
  65     T58 < &30)`;;