src/HOL/Library/sum_of_squares.ML
author chaieb
Tue, 12 May 2009 17:32:49 +0100
changeset 31119 2532bb2d65c7
child 31131 d9752181691a
permissions -rw-r--r--
A decision method for universal multivariate real arithmetic with add ition, multiplication and ordering using semidefinite programming
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31119
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     1
structure Sos = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     2
struct
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     3
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     4
val rat_0 = Rat.zero;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     5
val rat_1 = Rat.one;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     6
val rat_2 = Rat.two;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     7
val rat_10 = Rat.rat_of_int 10;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     8
val rat_1_2 = rat_1 // rat_2;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
     9
val max = curry IntInf.max;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    10
val min = curry IntInf.min;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    11
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    12
val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    13
val numerator_rat = Rat.quotient_of_rat #> fst #> Rat.rat_of_int;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    14
fun int_of_rat a = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    15
    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    16
fun lcm_rat x y = Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    17
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    18
fun rat_pow r i = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    19
 let fun pow r i = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    20
   if i = 0 then rat_1 else 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    21
   let val d = pow r (i div 2)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    22
   in d */ d */ (if i mod 2 = 0 then rat_1 else r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    23
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    24
 in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    25
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    26
fun round_rat r = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    27
 let val (a,b) = Rat.quotient_of_rat (Rat.abs r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    28
     val d = a div b
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    29
     val s = if r </ rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    30
     val x2 = 2 * (a - (b * d))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    31
 in s (if x2 >= b then d + 1 else d) end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    32
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    33
val abs_rat = Rat.abs;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    34
val pow2 = rat_pow rat_2;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    35
val pow10 = rat_pow rat_10;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    36
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    37
val debugging = ref false;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    38
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    39
exception Sanity;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    40
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    41
exception Unsolvable;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    42
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    43
(* Turn a rational into a decimal string with d sig digits.                  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    44
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    45
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    46
fun normalize y =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    47
  if abs_rat y </ (rat_1 // rat_10) then normalize (rat_10 */ y) - 1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    48
  else if abs_rat y >=/ rat_1 then normalize (y // rat_10) + 1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    49
  else 0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    50
 in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    51
fun decimalize d x =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    52
  if x =/ rat_0 then "0.0" else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    53
  let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    54
   val y = Rat.abs x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    55
   val e = normalize y
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    56
   val z = pow10(~ e) */ y +/ rat_1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    57
   val k = int_of_rat (round_rat(pow10 d */ z))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    58
  in (if x </ rat_0 then "-0." else "0.") ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    59
     implode(tl(explode(string_of_int k))) ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    60
     (if e = 0 then "" else "e"^string_of_int e)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    61
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    62
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    63
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    64
(* Iterations over numbers, and lists indexed by numbers.                    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    65
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    66
fun itern k l f a =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    67
  case l of
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    68
    [] => a
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    69
  | h::t => itern (k + 1) t f (f h k a);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    70
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    71
fun iter (m,n) f a =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    72
  if n < m then a
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    73
  else iter (m+1,n) f (f m a);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    74
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    75
(* The main types.                                                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    76
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    77
fun strict_ord ord (x,y) = case ord (x,y) of LESS => LESS | _ => GREATER
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    78
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    79
structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    80
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    81
type vector = int* Rat.rat Intfunc.T;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    82
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    83
type matrix = (int*int)*(Rat.rat Intpairfunc.T);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    84
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    85
type monomial = int Ctermfunc.T;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    86
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    87
val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    88
 fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    89
structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    90
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    91
type poly = Rat.rat Monomialfunc.T;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    92
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    93
 fun iszero (k,r) = r =/ rat_0;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    94
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    95
fun fold_rev2 f l1 l2 b =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    96
  case (l1,l2) of
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    97
    ([],[]) => b
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    98
  | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    99
  | _ => error "fold_rev2";
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   100
 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   101
(* Vectors. Conventionally indexed 1..n.                                     *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   102
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   103
fun vector_0 n = (n,Intfunc.undefined):vector;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   104
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   105
fun dim (v:vector) = fst v;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   106
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   107
fun vector_const c n =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   108
  if c =/ rat_0 then vector_0 n
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   109
  else (n,fold_rev (fn k => Intfunc.update (k,c)) (1 upto n) Intfunc.undefined) :vector;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   110
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   111
val vector_1 = vector_const rat_1;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   112
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   113
fun vector_cmul c (v:vector) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   114
 let val n = dim v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   115
 in if c =/ rat_0 then vector_0 n
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   116
    else (n,Intfunc.mapf (fn x => c */ x) (snd v))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   117
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   118
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   119
fun vector_neg (v:vector) = (fst v,Intfunc.mapf Rat.neg (snd v)) :vector;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   120
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   121
fun vector_add (v1:vector) (v2:vector) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   122
 let val m = dim v1  
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   123
     val n = dim v2 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   124
 in if m <> n then error "vector_add: incompatible dimensions"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   125
    else (n,Intfunc.combine (curry op +/) (fn x => x =/ rat_0) (snd v1) (snd v2)) :vector 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   126
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   127
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   128
fun vector_sub v1 v2 = vector_add v1 (vector_neg v2);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   129
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   130
fun vector_dot (v1:vector) (v2:vector) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   131
 let val m = dim v1 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   132
     val n = dim v2 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   133
 in if m <> n then error "vector_dot: incompatible dimensions" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   134
    else Intfunc.fold (fn (i,x) => fn a => x +/ a) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   135
        (Intfunc.combine (curry op */) (fn x => x =/ rat_0) (snd v1) (snd v2)) rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   136
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   137
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   138
fun vector_of_list l =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   139
 let val n = length l 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   140
 in (n,fold_rev2 (curry Intfunc.update) (1 upto n) l Intfunc.undefined) :vector
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   141
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   142
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   143
(* Matrices; again rows and columns indexed from 1.                          *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   144
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   145
fun matrix_0 (m,n) = ((m,n),Intpairfunc.undefined):matrix;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   146
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   147
fun dimensions (m:matrix) = fst m;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   148
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   149
fun matrix_const c (mn as (m,n)) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   150
  if m <> n then error "matrix_const: needs to be square"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   151
  else if c =/ rat_0 then matrix_0 mn
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   152
  else (mn,fold_rev (fn k => Intpairfunc.update ((k,k), c)) (1 upto n) Intpairfunc.undefined) :matrix;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   153
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   154
val matrix_1 = matrix_const rat_1;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   155
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   156
fun matrix_cmul c (m:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   157
 let val (i,j) = dimensions m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   158
 in if c =/ rat_0 then matrix_0 (i,j)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   159
    else ((i,j),Intpairfunc.mapf (fn x => c */ x) (snd m))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   160
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   161
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   162
fun matrix_neg (m:matrix) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   163
  (dimensions m, Intpairfunc.mapf Rat.neg (snd m)) :matrix;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   164
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   165
fun matrix_add (m1:matrix) (m2:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   166
 let val d1 = dimensions m1 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   167
     val d2 = dimensions m2 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   168
 in if d1 <> d2 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   169
     then error "matrix_add: incompatible dimensions"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   170
    else (d1,Intpairfunc.combine (curry op +/) (fn x => x =/ rat_0) (snd m1) (snd m2)) :matrix
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   171
 end;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   172
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   173
fun matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   174
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   175
fun row k (m:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   176
 let val (i,j) = dimensions m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   177
 in (j,
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   178
   Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then Intfunc.update (j,c) a else a) (snd m) Intfunc.undefined ) : vector
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   179
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   180
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   181
fun column k (m:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   182
  let val (i,j) = dimensions m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   183
  in (i,
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   184
   Intpairfunc.fold (fn ((i,j), c) => fn a => if j = k then Intfunc.update (i,c) a else a) (snd m)  Intfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   185
   : vector
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   186
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   187
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   188
fun transp (m:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   189
  let val (i,j) = dimensions m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   190
  in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   191
  ((j,i),Intpairfunc.fold (fn ((i,j), c) => fn a => Intpairfunc.update ((j,i), c) a) (snd m) Intpairfunc.undefined) :matrix
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   192
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   193
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   194
fun diagonal (v:vector) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   195
 let val n = dim v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   196
 in ((n,n),Intfunc.fold (fn (i, c) => fn a => Intpairfunc.update ((i,i), c) a) (snd v) Intpairfunc.undefined) : matrix
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   197
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   198
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   199
fun matrix_of_list l =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   200
 let val m = length l 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   201
 in if m = 0 then matrix_0 (0,0) else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   202
   let val n = length (hd l) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   203
   in ((m,n),itern 1 l (fn v => fn i => itern 1 v (fn c => fn j => Intpairfunc.update ((i,j), c))) Intpairfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   204
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   205
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   206
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   207
(* Monomials.                                                                *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   208
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   209
fun monomial_eval assig (m:monomial) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   210
  Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (Ctermfunc.apply assig x) k)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   211
        m rat_1;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   212
val monomial_1 = (Ctermfunc.undefined:monomial);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   213
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   214
fun monomial_var x = Ctermfunc.onefunc (x, 1) :monomial;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   215
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   216
val (monomial_mul:monomial->monomial->monomial) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   217
  Ctermfunc.combine (curry op +) (K false);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   218
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   219
fun monomial_pow (m:monomial) k =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   220
  if k = 0 then monomial_1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   221
  else Ctermfunc.mapf (fn x => k * x) m;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   222
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   223
fun monomial_divides (m1:monomial) (m2:monomial) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   224
  Ctermfunc.fold (fn (x, k) => fn a => Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   225
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   226
fun monomial_div (m1:monomial) (m2:monomial) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   227
 let val m = Ctermfunc.combine (curry op +) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   228
   (fn x => x = 0) m1 (Ctermfunc.mapf (fn x => ~ x) m2) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   229
 in if Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   230
  else error "monomial_div: non-divisible"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   231
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   232
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   233
fun monomial_degree x (m:monomial) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   234
  Ctermfunc.tryapplyd m x 0;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   235
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   236
fun monomial_lcm (m1:monomial) (m2:monomial) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   237
  fold_rev (fn x => Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   238
          (gen_union (is_equal o  cterm_ord) (Ctermfunc.dom m1, Ctermfunc.dom m2)) (Ctermfunc.undefined :monomial);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   239
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   240
fun monomial_multidegree (m:monomial) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   241
 Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   242
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   243
fun monomial_variables m = Ctermfunc.dom m;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   244
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   245
(* Polynomials.                                                              *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   246
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   247
fun eval assig (p:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   248
  Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   249
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   250
val poly_0 = (Monomialfunc.undefined:poly);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   251
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   252
fun poly_isconst (p:poly) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   253
  Monomialfunc.fold (fn (m, c) => fn a => Ctermfunc.is_undefined m andalso a) p true;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   254
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   255
fun poly_var x = Monomialfunc.onefunc (monomial_var x,rat_1) :poly;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   256
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   257
fun poly_const c =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   258
  if c =/ rat_0 then poly_0 else Monomialfunc.onefunc(monomial_1, c);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   259
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   260
fun poly_cmul c (p:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   261
  if c =/ rat_0 then poly_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   262
  else Monomialfunc.mapf (fn x => c */ x) p;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   263
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   264
fun poly_neg (p:poly) = (Monomialfunc.mapf Rat.neg p :poly);;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   265
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   266
fun poly_add (p1:poly) (p2:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   267
  (Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2 :poly);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   268
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   269
fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   270
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   271
fun poly_cmmul (c,m) (p:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   272
 if c =/ rat_0 then poly_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   273
 else if Ctermfunc.is_undefined m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   274
      then Monomialfunc.mapf (fn d => c */ d) p
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   275
      else Monomialfunc.fold (fn (m', d) => fn a => (Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   276
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   277
fun poly_mul (p1:poly) (p2:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   278
  Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   279
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   280
fun poly_div (p1:poly) (p2:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   281
 if not(poly_isconst p2) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   282
 then error "poly_div: non-constant" else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   283
 let val c = eval Ctermfunc.undefined p2 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   284
 in if c =/ rat_0 then error "poly_div: division by zero"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   285
    else poly_cmul (Rat.inv c) p1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   286
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   287
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   288
fun poly_square p = poly_mul p p;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   289
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   290
fun poly_pow p k =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   291
 if k = 0 then poly_const rat_1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   292
 else if k = 1 then p
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   293
 else let val q = poly_square(poly_pow p (k div 2)) in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   294
      if k mod 2 = 1 then poly_mul p q else q end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   295
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   296
fun poly_exp p1 p2 =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   297
  if not(poly_isconst p2) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   298
  then error "poly_exp: not a constant" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   299
  else poly_pow p1 (int_of_rat (eval Ctermfunc.undefined p2));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   300
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   301
fun degree x (p:poly) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   302
 Monomialfunc.fold (fn (m,c) => fn a => max (monomial_degree x m) a) p 0;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   303
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   304
fun multidegree (p:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   305
  Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   306
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   307
fun poly_variables (p:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   308
  sort cterm_ord (Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o  cterm_ord)) (monomial_variables m)) p []);;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   309
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   310
(* Order monomials for human presentation.                                   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   311
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   312
fun cterm_ord (t,t') = TermOrd.fast_term_ord (term_of t, term_of t');
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   313
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   314
val humanorder_varpow = prod_ord cterm_ord (rev_order o int_ord);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   315
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   316
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   317
 fun ord (l1,l2) = case (l1,l2) of
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   318
  (_,[]) => LESS 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   319
 | ([],_) => GREATER
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   320
 | (h1::t1,h2::t2) => 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   321
   (case humanorder_varpow (h1, h2) of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   322
     LESS => LESS
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   323
   | EQUAL => ord (t1,t2)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   324
   | GREATER => GREATER)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   325
in fun humanorder_monomial m1 m2 = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   326
 ord (sort humanorder_varpow (Ctermfunc.graph m1),
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   327
  sort humanorder_varpow (Ctermfunc.graph m2))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   328
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   329
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   330
fun fold1 f l =  case l of
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   331
   []     => error "fold1"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   332
 | [x]    => x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   333
 | (h::t) => f h (fold1 f t);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   334
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   335
(* Conversions to strings.                                                   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   336
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   337
fun string_of_vector min_size max_size (v:vector) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   338
 let val n_raw = dim v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   339
 in if n_raw = 0 then "[]" else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   340
  let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   341
   val n = max min_size (min n_raw max_size) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   342
   val xs = map (Rat.string_of_rat o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   343
  in "[" ^ fold1 (fn s => fn t => s ^ ", " ^ t) xs ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   344
  (if n_raw > max_size then ", ...]" else "]")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   345
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   346
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   347
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   348
fun string_of_matrix max_size (m:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   349
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   350
  val (i_raw,j_raw) = dimensions m
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   351
  val i = min max_size i_raw 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   352
  val j = min max_size j_raw
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   353
  val rstr = map (fn k => string_of_vector j j (row k m)) (1 upto i) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   354
 in "["^ fold1 (fn s => fn t => s^";\n "^t) rstr ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   355
  (if j > max_size then "\n ...]" else "]")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   356
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   357
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   358
fun string_of_term t = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   359
 case t of
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   360
   a$b => "("^(string_of_term a)^" "^(string_of_term b)^")"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   361
 | Abs x => 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   362
    let val (xn, b) = Term.dest_abs x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   363
    in "(\\"^xn^"."^(string_of_term b)^")"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   364
    end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   365
 | Const(s,_) => s
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   366
 | Free (s,_) => s
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   367
 | Var((s,_),_) => s
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   368
 | _ => error "string_of_term";
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   369
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   370
val string_of_cterm = string_of_term o term_of;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   371
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   372
fun string_of_varpow x k =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   373
  if k = 1 then string_of_cterm x 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   374
  else string_of_cterm x^"^"^string_of_int k;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   375
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   376
fun string_of_monomial m =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   377
 if Ctermfunc.is_undefined m then "1" else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   378
 let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   379
  (sort humanorder_varpow (Ctermfunc.graph m)) [] 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   380
 in fold1 (fn s => fn t => s^"*"^t) vps
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   381
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   382
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   383
fun string_of_cmonomial (c,m) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   384
 if Ctermfunc.is_undefined m then Rat.string_of_rat c
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   385
 else if c =/ rat_1 then string_of_monomial m
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   386
 else Rat.string_of_rat c ^ "*" ^ string_of_monomial m;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   387
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   388
fun string_of_poly (p:poly) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   389
 if Monomialfunc.is_undefined p then "<<0>>" else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   390
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   391
  val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (Monomialfunc.graph p)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   392
  val s = fold (fn (m,c) => fn a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   393
             if c </ rat_0 then a ^ " - " ^ string_of_cmonomial(Rat.neg c,m)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   394
             else a ^ " + " ^ string_of_cmonomial(c,m))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   395
          cms ""
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   396
  val s1 = String.substring (s, 0, 3)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   397
  val s2 = String.substring (s, 3, String.size s - 3) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   398
 in "<<" ^(if s1 = " + " then s2 else "-"^s2)^">>"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   399
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   400
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   401
(* Conversion from HOL term.                                                 *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   402
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   403
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   404
 val neg_tm = @{cterm "uminus :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   405
 val add_tm = @{cterm "op + :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   406
 val sub_tm = @{cterm "op - :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   407
 val mul_tm = @{cterm "op * :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   408
 val inv_tm = @{cterm "inverse :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   409
 val div_tm = @{cterm "op / :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   410
 val pow_tm = @{cterm "op ^ :: real => _"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   411
 val zero_tm = @{cterm "0:: real"}
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   412
 val is_numeral = can (HOLogic.dest_number o term_of)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   413
 fun is_comb t = case t of _$_ => true | _ => false
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   414
 fun poly_of_term tm =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   415
  if tm aconvc zero_tm then poly_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   416
  else if RealArith.is_ratconst tm 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   417
       then poly_const(RealArith.dest_ratconst tm)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   418
  else 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   419
  (let val (lop,r) = Thm.dest_comb tm
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   420
   in if lop aconvc neg_tm then poly_neg(poly_of_term r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   421
      else if lop aconvc inv_tm then
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   422
       let val p = poly_of_term r 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   423
       in if poly_isconst p 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   424
          then poly_const(Rat.inv (eval Ctermfunc.undefined p))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   425
          else error "poly_of_term: inverse of non-constant polyomial"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   426
       end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   427
   else (let val (opr,l) = Thm.dest_comb lop
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   428
         in 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   429
          if opr aconvc pow_tm andalso is_numeral r 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   430
          then poly_pow (poly_of_term l) ((snd o HOLogic.dest_number o term_of) r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   431
          else if opr aconvc add_tm 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   432
           then poly_add (poly_of_term l) (poly_of_term r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   433
          else if opr aconvc sub_tm 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   434
           then poly_sub (poly_of_term l) (poly_of_term r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   435
          else if opr aconvc mul_tm 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   436
           then poly_mul (poly_of_term l) (poly_of_term r)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   437
          else if opr aconvc div_tm 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   438
           then let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   439
                  val p = poly_of_term l 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   440
                  val q = poly_of_term r 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   441
                in if poly_isconst q then poly_cmul (Rat.inv (eval Ctermfunc.undefined q)) p
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   442
                   else error "poly_of_term: division by non-constant polynomial"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   443
                end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   444
          else poly_var tm
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   445
 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   446
         end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   447
         handle CTERM ("dest_comb",_) => poly_var tm)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   448
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   449
   handle CTERM ("dest_comb",_) => poly_var tm)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   450
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   451
val poly_of_term = fn tm =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   452
 if type_of (term_of tm) = @{typ real} then poly_of_term tm
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   453
 else error "poly_of_term: term does not have real type"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   454
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   455
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   456
(* String of vector (just a list of space-separated numbers).                *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   457
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   458
fun sdpa_of_vector (v:vector) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   459
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   460
  val n = dim v
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   461
  val strs = map (decimalize 20 o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   462
 in fold1 (fn x => fn y => x ^ " " ^ y) strs ^ "\n"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   463
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   464
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   465
fun increasing f ord (x,y) = ord (f x, f y);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   466
fun triple_int_ord ((a,b,c),(a',b',c')) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   467
 prod_ord int_ord (prod_ord int_ord int_ord) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   468
    ((a,(b,c)),(a',(b',c')));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   469
structure Inttriplefunc = FuncFun(type key = int*int*int val ord = triple_int_ord);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   470
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   471
(* String for block diagonal matrix numbered k.                              *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   472
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   473
fun sdpa_of_blockdiagonal k m =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   474
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   475
  val pfx = string_of_int k ^" "
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   476
  val ents =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   477
    Inttriplefunc.fold (fn ((b,i,j), c) => fn a => if i > j then a else ((b,i,j),c)::a) m []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   478
  val entss = sort (increasing fst triple_int_ord ) ents
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   479
 in  fold_rev (fn ((b,i,j),c) => fn a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   480
     pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   481
     " " ^ decimalize 20 c ^ "\n" ^ a) entss ""
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   482
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   483
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   484
(* String for a matrix numbered k, in SDPA sparse format.                    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   485
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   486
fun sdpa_of_matrix k (m:matrix) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   487
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   488
  val pfx = string_of_int k ^ " 1 "
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   489
  val ms = Intpairfunc.fold (fn ((i,j), c) => fn  a => if i > j then a else ((i,j),c)::a) (snd m) [] 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   490
  val mss = sort (increasing fst (prod_ord int_ord int_ord)) ms 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   491
 in fold_rev (fn ((i,j),c) => fn a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   492
     pfx ^ string_of_int i ^ " " ^ string_of_int j ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   493
     " " ^ decimalize 20 c ^ "\n" ^ a) mss ""
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   494
 end;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   495
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   496
(* ------------------------------------------------------------------------- *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   497
(* String in SDPA sparse format for standard SDP problem:                    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   498
(*                                                                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   499
(*    X = v_1 * [M_1] + ... + v_m * [M_m] - [M_0] must be PSD                *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   500
(*    Minimize obj_1 * v_1 + ... obj_m * v_m                                 *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   501
(* ------------------------------------------------------------------------- *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   502
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   503
fun sdpa_of_problem comment obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   504
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   505
  val m = length mats - 1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   506
  val (n,_) = dimensions (hd mats) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   507
 in "\"" ^ comment ^ "\"\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   508
  string_of_int m ^ "\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   509
  "1\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   510
  string_of_int n ^ "\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   511
  sdpa_of_vector obj ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   512
  fold_rev2 (fn k => fn m => fn a => sdpa_of_matrix (k - 1) m ^ a) (1 upto length mats) mats ""
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   513
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   514
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   515
fun index_char str chr pos =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   516
  if pos >= String.size str then ~1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   517
  else if String.sub(str,pos) = chr then pos
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   518
  else index_char str chr (pos + 1);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   519
fun rat_of_quotient (a,b) = if b = 0 then rat_0 else Rat.rat_of_quotient (a,b);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   520
fun rat_of_string s = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   521
 let val n = index_char s #"/" 0 in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   522
  if n = ~1 then s |> IntInf.fromString |> valOf |> Rat.rat_of_int
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   523
  else 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   524
   let val SOME numer = IntInf.fromString(String.substring(s,0,n))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   525
       val SOME den = IntInf.fromString (String.substring(s,n+1,String.size s - n - 1))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   526
   in rat_of_quotient(numer, den)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   527
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   528
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   529
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   530
fun isspace x = x = " " ;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   531
fun isnum x = x mem_string ["0","1","2","3","4","5","6","7","8","9"]
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   532
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   533
(* More parser basics.                                                       *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   534
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   535
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   536
 open Scan
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   537
in 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   538
 val word = this_string
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   539
 fun token s =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   540
  repeat ($$ " ") |-- word s --| repeat ($$ " ")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   541
 val numeral = one isnum
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   542
 val decimalint = bulk numeral >> (rat_of_string o implode)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   543
 val decimalfrac = bulk numeral
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   544
    >> (fn s => rat_of_string(implode s) // pow10 (length s))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   545
 val decimalsig =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   546
    decimalint -- option (Scan.$$ "." |-- decimalfrac)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   547
    >> (fn (h,NONE) => h | (h,SOME x) => h +/ x)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   548
 fun signed prs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   549
       $$ "-" |-- prs >> Rat.neg 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   550
    || $$ "+" |-- prs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   551
    || prs;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   552
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   553
fun emptyin def xs = if null xs then (def,xs) else Scan.fail xs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   554
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   555
 val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   556
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   557
 val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   558
    >> (fn (h, x) => h */ pow10 (int_of_rat x));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   559
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   560
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   561
 fun mkparser p s =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   562
  let val (x,rst) = p (explode s) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   563
  in if null rst then x 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   564
     else error "mkparser: unparsed input"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   565
  end;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   566
val parse_decimal = mkparser decimal;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   567
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   568
fun fix err prs = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   569
  prs || (fn x=> error err);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   570
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   571
fun listof prs sep err =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   572
  prs -- Scan.bulk (sep |-- fix err prs) >> uncurry cons;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   573
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   574
(* Parse back a vector.                                                      *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   575
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   576
 val vector = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   577
    token "{" |-- listof decimal (token ",") "decimal" --| token "}"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   578
               >> vector_of_list 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   579
 val parse_vector = mkparser vector
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   580
 fun skipupto dscr prs inp =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   581
   (dscr |-- prs 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   582
    || Scan.one (K true) |-- skipupto dscr prs) inp 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   583
 fun ignore inp = ((),[])
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   584
 fun sdpaoutput inp =  skipupto (word "xVec" -- token "=")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   585
             (vector --| ignore) inp
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   586
 fun csdpoutput inp =  ((decimal -- Scan.bulk (Scan.$$ " " |-- Scan.option decimal) >> (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   587
 val parse_sdpaoutput = mkparser sdpaoutput
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   588
 val parse_csdpoutput = mkparser csdpoutput
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   589
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   590
(* Also parse the SDPA output to test success (CSDP yields a return code).   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   591
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   592
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   593
 val prs = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   594
  skipupto (word "phase.value" -- token "=")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   595
   (Scan.option (Scan.$$ "p") -- Scan.option (Scan.$$ "d") 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   596
    -- (word "OPT" || word "FEAS")) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   597
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   598
 fun sdpa_run_succeeded s = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   599
  (prs (explode s); true) handle _ => false
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   600
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   601
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   602
(* The default parameters. Unfortunately this goes to a fixed file.          *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   603
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   604
val sdpa_default_parameters =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   605
"100     unsigned int maxIteration; \n1.0E-7  double 0.0 < epsilonStar;\n1.0E2   double 0.0 < lambdaStar;\n2.0     double 1.0 < omegaStar;\n-1.0E5  double lowerBound;\n1.0E5   double upperBound;\n0.1     double 0.0 <= betaStar <  1.0;\n0.2     double 0.0 <= betaBar  <  1.0, betaStar <= betaBar;\n0.9     double 0.0 < gammaStar  <  1.0;\n1.0E-7  double 0.0 < epsilonDash;\n";;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   606
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   607
(* These were suggested by Makoto Yamashita for problems where we are        *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   608
(* right at the edge of the semidefinite cone, as sometimes happens.         *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   609
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   610
val sdpa_alt_parameters =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   611
"1000    unsigned int maxIteration;\n1.0E-7  double 0.0 < epsilonStar;\n1.0E4   double 0.0 < lambdaStar;\n2.0     double 1.0 < omegaStar;\n-1.0E5  double lowerBound;\n1.0E5   double upperBound;\n0.1     double 0.0 <= betaStar <  1.0;\n0.2     double 0.0 <= betaBar  <  1.0, betaStar <= betaBar;\n0.9     double 0.0 < gammaStar  <  1.0;\n1.0E-7  double 0.0 < epsilonDash;\n";;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   612
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   613
val sdpa_params = sdpa_alt_parameters;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   614
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   615
(* CSDP parameters; so far I'm sticking with the defaults.                   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   616
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   617
val csdp_default_parameters =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   618
"axtol=1.0e-8\natytol=1.0e-8\nobjtol=1.0e-8\npinftol=1.0e8\ndinftol=1.0e8\nmaxiter=100\nminstepfrac=0.9\nmaxstepfrac=0.97\nminstepp=1.0e-8\nminstepd=1.0e-8\nusexzgap=1\ntweakgap=0\naffine=0\nprintlevel=1\n";;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   619
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   620
val csdp_params = csdp_default_parameters;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   621
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   622
fun tmp_file pre suf =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   623
 let val i = string_of_int (round (random()))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   624
   val name = Path.append (Path.variable "ISABELLE_TMP") (Path.explode (pre ^ i ^ suf))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   625
 in 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   626
   if File.exists name then tmp_file pre suf 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   627
   else name 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   628
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   629
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   630
(* Now call SDPA on a problem and parse back the output.                     *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   631
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   632
fun run_sdpa dbg obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   633
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   634
  val input_file = tmp_file "sos" ".dat-s"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   635
  val output_file = tmp_file "sos" ".out"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   636
  val params_file = tmp_file "param" ".sdpa" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   637
  val current_dir = File.pwd()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   638
  val _ = File.write input_file 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   639
                         (sdpa_of_problem "" obj mats)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   640
  val _ = File.write params_file sdpa_params
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   641
  val _ = File.cd (Path.variable "ISABELLE_TMP")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   642
  val _ = File.system_command ("sdpa "^ (Path.implode input_file) ^ " " ^ 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   643
                               (Path.implode output_file) ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   644
                               (if dbg then "" else "> /dev/null"))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   645
  val opr = File.read output_file 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   646
 in if not(sdpa_run_succeeded opr) then error "sdpa: call failed" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   647
    else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   648
      let val res = parse_sdpaoutput opr 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   649
      in ((if dbg then ()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   650
           else (File.rm input_file; File.rm output_file ; File.cd current_dir));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   651
          res)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   652
      end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   653
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   654
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   655
fun sdpa obj mats = run_sdpa (!debugging) obj mats;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   656
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   657
(* The same thing with CSDP.                                                 *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   658
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   659
fun run_csdp dbg obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   660
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   661
  val input_file = tmp_file "sos" ".dat-s"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   662
  val output_file = tmp_file "sos" ".out"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   663
  val params_file = tmp_file "param" ".csdp"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   664
  val current_dir = File.pwd()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   665
  val _ = File.write input_file (sdpa_of_problem "" obj mats)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   666
  val _ = File.write params_file csdp_params
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   667
  val _ = File.cd (Path.variable "ISABELLE_TMP")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   668
  val rv = system ("csdp "^(Path.implode input_file) ^ " " 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   669
                   ^ (Path.implode output_file) ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   670
                   (if dbg then "" else "> /dev/null"))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   671
  val  opr = File.read output_file 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   672
  val res = parse_csdpoutput opr 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   673
 in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   674
    ((if dbg then ()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   675
      else (File.rm input_file; File.rm output_file ; File.cd current_dir));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   676
     (rv,res))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   677
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   678
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   679
fun csdp obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   680
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   681
  val (rv,res) = run_csdp (!debugging) obj mats 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   682
 in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   683
   ((if rv = 1 orelse rv = 2 then error "csdp: Problem is infeasible"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   684
    else if rv = 3 then writeln "csdp warning: Reduced accuracy"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   685
    else if rv <> 0 then error ("csdp: error "^string_of_int rv)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   686
    else ());
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   687
   res)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   688
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   689
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   690
(* Try some apparently sensible scaling first. Note that this is purely to   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   691
(* get a cleaner translation to floating-point, and doesn't affect any of    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   692
(* the results, in principle. In practice it seems a lot better when there   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   693
(* are extreme numbers in the original problem.                              *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   694
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   695
  (* Version for (int*int) keys *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   696
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   697
  fun max_rat x y = if x </ y then y else x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   698
  fun common_denominator fld amat acc =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   699
      fld (fn (m,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   700
  fun maximal_element fld amat acc =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   701
    fld (fn (m,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   702
fun float_of_rat x = let val (a,b) = Rat.quotient_of_rat x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   703
                     in Real.fromLargeInt a / Real.fromLargeInt b end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   704
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   705
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   706
fun pi_scale_then solver (obj:vector)  mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   707
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   708
  val cd1 = fold_rev (common_denominator Intpairfunc.fold) mats (rat_1)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   709
  val cd2 = common_denominator Intfunc.fold (snd obj)  (rat_1) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   710
  val mats' = map (Intpairfunc.mapf (fn x => cd1 */ x)) mats
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   711
  val obj' = vector_cmul cd2 obj
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   712
  val max1 = fold_rev (maximal_element Intpairfunc.fold) mats' (rat_0)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   713
  val max2 = maximal_element Intfunc.fold (snd obj') (rat_0) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   714
  val scal1 = pow2 (20 - trunc(Math.ln (float_of_rat max1) / Math.ln 2.0))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   715
  val scal2 = pow2 (20 - trunc(Math.ln (float_of_rat max2) / Math.ln 2.0)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   716
  val mats'' = map (Intpairfunc.mapf (fn x => x */ scal1)) mats'
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   717
  val obj'' = vector_cmul scal2 obj' 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   718
 in solver obj'' mats''
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   719
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   720
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   721
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   722
(* Try some apparently sensible scaling first. Note that this is purely to   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   723
(* get a cleaner translation to floating-point, and doesn't affect any of    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   724
(* the results, in principle. In practice it seems a lot better when there   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   725
(* are extreme numbers in the original problem.                              *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   726
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   727
  (* Version for (int*int*int) keys *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   728
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   729
  fun max_rat x y = if x </ y then y else x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   730
  fun common_denominator fld amat acc =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   731
      fld (fn (m,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   732
  fun maximal_element fld amat acc =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   733
    fld (fn (m,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   734
fun float_of_rat x = let val (a,b) = Rat.quotient_of_rat x
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   735
                     in Real.fromLargeInt a / Real.fromLargeInt b end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   736
fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   737
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   738
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   739
fun tri_scale_then solver (obj:vector)  mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   740
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   741
  val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   742
  val cd2 = common_denominator Intfunc.fold (snd obj)  (rat_1) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   743
  val mats' = map (Inttriplefunc.mapf (fn x => cd1 */ x)) mats
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   744
  val obj' = vector_cmul cd2 obj
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   745
  val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   746
  val max2 = maximal_element Intfunc.fold (snd obj') (rat_0) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   747
  val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   748
  val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   749
  val mats'' = map (Inttriplefunc.mapf (fn x => x */ scal1)) mats'
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   750
  val obj'' = vector_cmul scal2 obj' 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   751
 in solver obj'' mats''
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   752
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   753
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   754
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   755
(* Round a vector to "nice" rationals.                                       *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   756
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   757
fun nice_rational n x = round_rat (n */ x) // n;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   758
fun nice_vector n ((d,v) : vector) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   759
 (d, Intfunc.fold (fn (i,c) => fn a => 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   760
   let val y = nice_rational n c 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   761
   in if c =/ rat_0 then a 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   762
      else Intfunc.update (i,y) a end) v Intfunc.undefined):vector
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   763
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   764
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   765
(* Reduce linear program to SDP (diagonal matrices) and test with CSDP. This *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   766
(* one tests A [-1;x1;..;xn] >= 0 (i.e. left column is negated constants).   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   767
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   768
fun linear_program_basic a =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   769
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   770
  val (m,n) = dimensions a
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   771
  val mats =  map (fn j => diagonal (column j a)) (1 upto n)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   772
  val obj = vector_const rat_1 m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   773
  val (rv,res) = run_csdp false obj mats 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   774
 in if rv = 1 orelse rv = 2 then false
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   775
    else if rv = 0 then true
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   776
    else error "linear_program: An error occurred in the SDP solver"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   777
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   778
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   779
(* Alternative interface testing A x >= b for matrix A, vector b.            *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   780
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   781
fun linear_program a b =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   782
 let val (m,n) = dimensions a 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   783
 in if dim b <> m then error "linear_program: incompatible dimensions" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   784
    else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   785
    let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   786
     val mats = diagonal b :: map (fn j => diagonal (column j a)) (1 upto n)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   787
     val obj = vector_const rat_1 m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   788
     val (rv,res) = run_csdp false obj mats 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   789
    in if rv = 1 orelse rv = 2 then false
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   790
       else if rv = 0 then true
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   791
       else error "linear_program: An error occurred in the SDP solver"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   792
    end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   793
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   794
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   795
(* Test whether a point is in the convex hull of others. Rather than use     *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   796
(* computational geometry, express as linear inequalities and call CSDP.     *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   797
(* This is a bit lazy of me, but it's easy and not such a bottleneck so far. *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   798
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   799
fun in_convex_hull pts pt =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   800
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   801
  val pts1 = (1::pt) :: map (fn x => 1::x) pts 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   802
  val pts2 = map (fn p => map (fn x => ~x) p @ p) pts1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   803
  val n = length pts + 1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   804
  val v = 2 * (length pt + 1)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   805
  val m = v + n - 1 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   806
  val mat = ((m,n),
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   807
  itern 1 pts2 (fn pts => fn j => itern 1 pts 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   808
               (fn x => fn i => Intpairfunc.update ((i,j), Rat.rat_of_int x)))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   809
  (iter (1,n) (fn i => Intpairfunc.update((v + i,i+1), rat_1)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   810
      Intpairfunc.undefined))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   811
 in linear_program_basic mat
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   812
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   813
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   814
(* Filter down a set of points to a minimal set with the same convex hull.   *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   815
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   816
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   817
 fun augment1 (m::ms) = if in_convex_hull ms m then ms else ms@[m]
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   818
 fun augment m ms = funpow 3 augment1 (m::ms)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   819
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   820
fun minimal_convex_hull mons =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   821
 let val mons' = fold_rev augment (tl mons) [hd mons] 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   822
 in funpow (length mons') augment1 mons'
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   823
 end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   824
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   825
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   826
fun dest_ord f x = is_equal (f x);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   827
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   828
(* Stuff for "equations" ((int*int*int)->num functions).                         *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   829
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   830
fun tri_equation_cmul c eq =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   831
  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (fn d => c */ d) eq;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   832
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   833
fun tri_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   834
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   835
fun tri_equation_eval assig eq =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   836
 let fun value v = Inttriplefunc.apply assig v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   837
 in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   838
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   839
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   840
(* Eliminate among linear equations: return unconstrained variables and      *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   841
(* assignments for the others in terms of them. We give one pseudo-variable  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   842
(* "one" that's used for a constant term.                                    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   843
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   844
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   845
  fun extract_first p l = case l of  (* FIXME : use find_first instead *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   846
   [] => error "extract_first"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   847
 | h::t => if p h then (h,t) else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   848
          let val (k,s) = extract_first p t in (k,h::s) end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   849
fun eliminate vars dun eqs = case vars of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   850
  [] => if forall Inttriplefunc.is_undefined eqs then dun
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   851
        else raise Unsolvable
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   852
 | v::vs =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   853
  ((let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   854
    val (eq,oeqs) = extract_first (fn e => Inttriplefunc.defined e v) eqs 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   855
    val a = Inttriplefunc.apply eq v
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   856
    val eq' = tri_equation_cmul ((Rat.neg rat_1) // a) (Inttriplefunc.undefine v eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   857
    fun elim e =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   858
     let val b = Inttriplefunc.tryapplyd e v rat_0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   859
     in if b =/ rat_0 then e else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   860
        tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   861
     end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   862
   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.mapf elim dun)) (map elim oeqs)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   863
   end)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   864
  handle ERROR _ => eliminate vs dun eqs)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   865
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   866
fun tri_eliminate_equations one vars eqs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   867
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   868
  val assig = eliminate vars Inttriplefunc.undefined eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   869
  val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   870
  in (distinct (dest_ord triple_int_ord) vs, assig)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   871
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   872
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   873
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   874
(* Eliminate all variables, in an essentially arbitrary order.               *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   875
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   876
fun tri_eliminate_all_equations one =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   877
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   878
  fun choose_variable eq =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   879
   let val (v,_) = Inttriplefunc.choose eq 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   880
   in if is_equal (triple_int_ord(v,one)) then
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   881
      let val eq' = Inttriplefunc.undefine v eq 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   882
      in if Inttriplefunc.is_undefined eq' then error "choose_variable" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   883
         else fst (Inttriplefunc.choose eq')
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   884
      end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   885
    else v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   886
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   887
  fun eliminate dun eqs = case eqs of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   888
    [] => dun
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   889
  | eq::oeqs =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   890
    if Inttriplefunc.is_undefined eq then eliminate dun oeqs else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   891
    let val v = choose_variable eq
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   892
        val a = Inttriplefunc.apply eq v
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   893
        val eq' = tri_equation_cmul ((Rat.rat_of_int ~1) // a) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   894
                   (Inttriplefunc.undefine v eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   895
        fun elim e =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   896
         let val b = Inttriplefunc.tryapplyd e v rat_0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   897
         in if b =/ rat_0 then e 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   898
            else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   899
         end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   900
    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.mapf elim dun)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   901
                 (map elim oeqs) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   902
    end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   903
in fn eqs =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   904
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   905
  val assig = eliminate Inttriplefunc.undefined eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   906
  val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   907
 in (distinct (dest_ord triple_int_ord) vs,assig)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   908
 end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   909
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   910
 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   911
(* Solve equations by assigning arbitrary numbers.                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   912
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   913
fun tri_solve_equations one eqs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   914
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   915
  val (vars,assigs) = tri_eliminate_all_equations one eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   916
  val vfn = fold_rev (fn v => Inttriplefunc.update(v,rat_0)) vars 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   917
            (Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   918
  val ass =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   919
    Inttriplefunc.combine (curry op +/) (K false) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   920
    (Inttriplefunc.mapf (tri_equation_eval vfn) assigs) vfn 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   921
 in if forall (fn e => tri_equation_eval ass e =/ rat_0) eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   922
    then Inttriplefunc.undefine one ass else raise Sanity
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   923
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   924
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   925
(* Multiply equation-parametrized poly by regular poly and add accumulator.  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   926
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   927
fun tri_epoly_pmul p q acc =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   928
 Monomialfunc.fold (fn (m1, c) => fn a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   929
  Monomialfunc.fold (fn (m2,e) => fn b =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   930
   let val m =  monomial_mul m1 m2
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   931
       val es = Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   932
   in Monomialfunc.update (m,tri_equation_add (tri_equation_cmul c e) es) b 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   933
   end) q a) p acc ;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   934
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   935
(* Usual operations on equation-parametrized poly.                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   936
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   937
fun tri_epoly_cmul c l =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   938
  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (tri_equation_cmul c) l;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   939
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   940
val tri_epoly_neg = tri_epoly_cmul (Rat.rat_of_int ~1);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   941
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   942
val tri_epoly_add = Inttriplefunc.combine tri_equation_add Inttriplefunc.is_undefined;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   943
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   944
fun tri_epoly_sub p q = tri_epoly_add p (tri_epoly_neg q);;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   945
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   946
(* Stuff for "equations" ((int*int)->num functions).                         *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   947
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   948
fun pi_equation_cmul c eq =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   949
  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (fn d => c */ d) eq;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   950
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   951
fun pi_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   952
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   953
fun pi_equation_eval assig eq =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   954
 let fun value v = Inttriplefunc.apply assig v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   955
 in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   956
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   957
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   958
(* Eliminate among linear equations: return unconstrained variables and      *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   959
(* assignments for the others in terms of them. We give one pseudo-variable  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   960
(* "one" that's used for a constant term.                                    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   961
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   962
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   963
fun extract_first p l = case l of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   964
   [] => error "extract_first"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   965
 | h::t => if p h then (h,t) else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   966
          let val (k,s) = extract_first p t in (k,h::s) end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   967
fun eliminate vars dun eqs = case vars of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   968
  [] => if forall Inttriplefunc.is_undefined eqs then dun
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   969
        else raise Unsolvable
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   970
 | v::vs =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   971
   let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   972
    val (eq,oeqs) = extract_first (fn e => Inttriplefunc.defined e v) eqs 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   973
    val a = Inttriplefunc.apply eq v
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   974
    val eq' = pi_equation_cmul ((Rat.neg rat_1) // a) (Inttriplefunc.undefine v eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   975
    fun elim e =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   976
     let val b = Inttriplefunc.tryapplyd e v rat_0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   977
     in if b =/ rat_0 then e else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   978
        pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   979
     end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   980
   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.mapf elim dun)) (map elim oeqs)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   981
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   982
  handle ERROR _ => eliminate vs dun eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   983
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   984
fun pi_eliminate_equations one vars eqs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   985
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   986
  val assig = eliminate vars Inttriplefunc.undefined eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   987
  val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   988
  in (distinct (dest_ord triple_int_ord) vs, assig)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   989
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   990
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   991
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   992
(* Eliminate all variables, in an essentially arbitrary order.               *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   993
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   994
fun pi_eliminate_all_equations one =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   995
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   996
  fun choose_variable eq =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   997
   let val (v,_) = Inttriplefunc.choose eq 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   998
   in if is_equal (triple_int_ord(v,one)) then
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
   999
      let val eq' = Inttriplefunc.undefine v eq 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1000
      in if Inttriplefunc.is_undefined eq' then error "choose_variable" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1001
         else fst (Inttriplefunc.choose eq')
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1002
      end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1003
    else v 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1004
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1005
  fun eliminate dun eqs = case eqs of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1006
    [] => dun
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1007
  | eq::oeqs =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1008
    if Inttriplefunc.is_undefined eq then eliminate dun oeqs else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1009
    let val v = choose_variable eq
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1010
        val a = Inttriplefunc.apply eq v
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1011
        val eq' = pi_equation_cmul ((Rat.rat_of_int ~1) // a) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1012
                   (Inttriplefunc.undefine v eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1013
        fun elim e =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1014
         let val b = Inttriplefunc.tryapplyd e v rat_0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1015
         in if b =/ rat_0 then e 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1016
            else pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1017
         end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1018
    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.mapf elim dun)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1019
                 (map elim oeqs) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1020
    end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1021
in fn eqs =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1022
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1023
  val assig = eliminate Inttriplefunc.undefined eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1024
  val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1025
 in (distinct (dest_ord triple_int_ord) vs,assig)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1026
 end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1027
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1028
 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1029
(* Solve equations by assigning arbitrary numbers.                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1030
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1031
fun pi_solve_equations one eqs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1032
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1033
  val (vars,assigs) = pi_eliminate_all_equations one eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1034
  val vfn = fold_rev (fn v => Inttriplefunc.update(v,rat_0)) vars 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1035
            (Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1036
  val ass =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1037
    Inttriplefunc.combine (curry op +/) (K false) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1038
    (Inttriplefunc.mapf (pi_equation_eval vfn) assigs) vfn 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1039
 in if forall (fn e => pi_equation_eval ass e =/ rat_0) eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1040
    then Inttriplefunc.undefine one ass else raise Sanity
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1041
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1042
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1043
(* Multiply equation-parametrized poly by regular poly and add accumulator.  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1044
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1045
fun pi_epoly_pmul p q acc =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1046
 Monomialfunc.fold (fn (m1, c) => fn a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1047
  Monomialfunc.fold (fn (m2,e) => fn b =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1048
   let val m =  monomial_mul m1 m2
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1049
       val es = Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1050
   in Monomialfunc.update (m,pi_equation_add (pi_equation_cmul c e) es) b 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1051
   end) q a) p acc ;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1052
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1053
(* Usual operations on equation-parametrized poly.                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1054
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1055
fun pi_epoly_cmul c l =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1056
  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (pi_equation_cmul c) l;;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1057
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1058
val pi_epoly_neg = pi_epoly_cmul (Rat.rat_of_int ~1);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1059
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1060
val pi_epoly_add = Inttriplefunc.combine pi_equation_add Inttriplefunc.is_undefined;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1061
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1062
fun pi_epoly_sub p q = pi_epoly_add p (pi_epoly_neg q);;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1063
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1064
fun allpairs f l1 l2 =  fold_rev (fn x => (curry (op @)) (map (f x) l2)) l1 [];
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1065
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1066
(* Hence produce the "relevant" monomials: those whose squares lie in the    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1067
(* Newton polytope of the monomials in the input. (This is enough according  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1068
(* to Reznik: "Extremal PSD forms with few terms", Duke Math. Journal,       *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1069
(* vol 45, pp. 363--374, 1978.                                               *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1070
(*                                                                           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1071
(* These are ordered in sort of decreasing degree. In particular the         *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1072
(* constant monomial is last; this gives an order in diagonalization of the  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1073
(* quadratic form that will tend to display constants.                       *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1074
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1075
fun newton_polytope pol =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1076
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1077
  val vars = poly_variables pol
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1078
  val mons = map (fn m => map (fn x => monomial_degree x m) vars) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1079
             (Monomialfunc.dom pol)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1080
  val ds = map (fn x => (degree x pol + 1) div 2) vars
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1081
  val all = fold_rev (fn n => allpairs cons (0 upto n)) ds [[]]
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1082
  val mons' = minimal_convex_hull mons
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1083
  val all' =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1084
    filter (fn m => in_convex_hull mons' (map (fn x => 2 * x) m)) all 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1085
 in map (fn m => fold_rev2 (fn v => fn i => fn a => if i = 0 then a else Ctermfunc.update (v,i) a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1086
                        vars m monomial_1) (rev all')
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1087
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1088
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1089
(* Diagonalize (Cholesky/LDU) the matrix corresponding to a quadratic form.  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1090
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1091
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1092
fun diagonalize n i m =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1093
 if Intpairfunc.is_undefined (snd m) then [] 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1094
 else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1095
  let val a11 = Intpairfunc.tryapplyd (snd m) (i,i) rat_0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1096
  in if a11 </ rat_0 then error "diagonalize: not PSD"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1097
    else if a11 =/ rat_0 then
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1098
          if Intfunc.is_undefined (snd (row i m)) then diagonalize n (i + 1) m
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1099
          else error "diagonalize: not PSD ___ "
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1100
    else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1101
     let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1102
      val v = row i m
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1103
      val v' = (fst v, Intfunc.fold (fn (i, c) => fn a => 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1104
       let val y = c // a11 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1105
       in if y = rat_0 then a else Intfunc.update (i,y) a 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1106
       end)  (snd v) Intfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1107
      fun upt0 x y a = if y = rat_0 then a else Intpairfunc.update (x,y) a
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1108
      val m' =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1109
      ((n,n),
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1110
      iter (i+1,n) (fn j =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1111
          iter (i+1,n) (fn k =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1112
              (upt0 (j,k) (Intpairfunc.tryapplyd (snd m) (j,k) rat_0 -/ Intfunc.tryapplyd (snd v) j rat_0 */ Intfunc.tryapplyd (snd v') k rat_0))))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1113
          Intpairfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1114
     in (a11,v')::diagonalize n (i + 1) m' 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1115
     end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1116
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1117
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1118
fun diag m =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1119
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1120
   val nn = dimensions m 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1121
   val n = fst nn 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1122
 in if snd nn <> n then error "diagonalize: non-square matrix" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1123
    else diagonalize n 1 m
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1124
 end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1125
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1126
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1127
fun gcd_rat a b = Rat.rat_of_int (Integer.gcd (int_of_rat a) (int_of_rat b));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1128
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1129
(* Adjust a diagonalization to collect rationals at the start.               *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1130
  (* FIXME : Potentially polymorphic keys, but here only: integers!! *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1131
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1132
 fun upd0 x y a = if y =/ rat_0 then a else Intfunc.update(x,y) a;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1133
 fun mapa f (d,v) = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1134
  (d, Intfunc.fold (fn (i,c) => fn a => upd0 i (f c) a) v Intfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1135
 fun adj (c,l) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1136
 let val a = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1137
  Intfunc.fold (fn (i,c) => fn a => lcm_rat a (denominator_rat c)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1138
    (snd l) rat_1 //
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1139
  Intfunc.fold (fn (i,c) => fn a => gcd_rat a (numerator_rat c)) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1140
    (snd l) rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1141
  in ((c // (a */ a)),mapa (fn x => a */ x) l)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1142
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1143
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1144
fun deration d = if null d then (rat_0,d) else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1145
 let val d' = map adj d
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1146
     val a = fold (lcm_rat o denominator_rat o fst) d' rat_1 //
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1147
          fold (gcd_rat o numerator_rat o fst) d' rat_0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1148
 in ((rat_1 // a),map (fn (c,l) => (a */ c,l)) d')
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1149
 end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1150
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1151
 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1152
(* Enumeration of monomials with given multidegree bound.                    *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1153
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1154
fun enumerate_monomials d vars = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1155
 if d < 0 then []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1156
 else if d = 0 then [Ctermfunc.undefined]
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1157
 else if null vars then [monomial_1] else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1158
 let val alts =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1159
  map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1160
               in map (fn ks => if k = 0 then ks else Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1161
 in fold1 (curry op @) alts
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1162
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1163
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1164
(* Enumerate products of distinct input polys with degree <= d.              *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1165
(* We ignore any constant input polynomials.                                 *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1166
(* Give the output polynomial and a record of how it was derived.            *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1167
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1168
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1169
 open RealArith
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1170
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1171
fun enumerate_products d pols =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1172
if d = 0 then [(poly_const rat_1,Rational_lt rat_1)] 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1173
else if d < 0 then [] else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1174
case pols of 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1175
   [] => [(poly_const rat_1,Rational_lt rat_1)]
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1176
 | (p,b)::ps => 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1177
    let val e = multidegree p 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1178
    in if e = 0 then enumerate_products d ps else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1179
       enumerate_products d ps @
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1180
       map (fn (q,c) => (poly_mul p q,Product(b,c)))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1181
         (enumerate_products (d - e) ps)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1182
    end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1183
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1184
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1185
(* Convert regular polynomial. Note that we treat (0,0,0) as -1.             *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1186
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1187
fun epoly_of_poly p =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1188
  Monomialfunc.fold (fn (m,c) => fn a => Monomialfunc.update (m, Inttriplefunc.onefunc ((0,0,0), Rat.neg c)) a) p Monomialfunc.undefined;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1189
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1190
(* String for block diagonal matrix numbered k.                              *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1191
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1192
fun sdpa_of_blockdiagonal k m =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1193
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1194
  val pfx = string_of_int k ^" "
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1195
  val ents =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1196
    Inttriplefunc.fold 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1197
      (fn ((b,i,j),c) => fn a => if i > j then a else ((b,i,j),c)::a) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1198
      m [] 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1199
  val entss = sort (increasing fst triple_int_ord) ents 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1200
 in fold_rev (fn ((b,i,j),c) => fn a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1201
     pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1202
     " " ^ decimalize 20 c ^ "\n" ^ a) entss ""
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1203
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1204
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1205
(* SDPA for problem using block diagonal (i.e. multiple SDPs)                *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1206
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1207
fun sdpa_of_blockproblem comment nblocks blocksizes obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1208
 let val m = length mats - 1 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1209
 in  "\"" ^ comment ^ "\"\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1210
  string_of_int m ^ "\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1211
  string_of_int nblocks ^ "\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1212
  (fold1 (fn s => fn t => s^" "^t) (map string_of_int blocksizes)) ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1213
  "\n" ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1214
  sdpa_of_vector obj ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1215
  fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1216
    (1 upto length mats) mats ""
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1217
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1218
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1219
(* Hence run CSDP on a problem in block diagonal form.                       *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1220
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1221
fun run_csdp dbg nblocks blocksizes obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1222
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1223
  val input_file = tmp_file "sos" ".dat-s" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1224
  val output_file = tmp_file "sos" ".out"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1225
  val params_file = tmp_file "param" ".csdp" 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1226
  val _ = File.write input_file
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1227
   (sdpa_of_blockproblem "" nblocks blocksizes obj mats)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1228
  val _ = File.write params_file csdp_params
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1229
  val current_dir = File.pwd()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1230
  val _ = File.cd (Path.variable "ISABELLE_TMP")
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1231
  val rv = system ("csdp "^(Path.implode input_file) ^ " " 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1232
                   ^ (Path.implode output_file) ^
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1233
                   (if dbg then "" else "> /dev/null"))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1234
  val  opr = File.read output_file 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1235
  val res = parse_csdpoutput opr 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1236
 in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1237
   ((if dbg then ()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1238
     else (File.rm input_file ; File.rm output_file ; File.cd current_dir));
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1239
    (rv,res))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1240
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1241
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1242
fun csdp nblocks blocksizes obj mats =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1243
 let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1244
  val (rv,res) = run_csdp (!debugging) nblocks blocksizes obj mats 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1245
 in ((if rv = 1 orelse rv = 2 then error "csdp: Problem is infeasible"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1246
     else if rv = 3 then writeln "csdp warning: Reduced accuracy"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1247
     else if rv <> 0 then error ("csdp: error "^string_of_int rv)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1248
     else ());
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1249
     res)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1250
 end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1251
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1252
(* 3D versions of matrix operations to consider blocks separately.           *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1253
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1254
val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1255
fun bmatrix_cmul c bm =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1256
  if c =/ rat_0 then Inttriplefunc.undefined
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1257
  else Inttriplefunc.mapf (fn x => c */ x) bm;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1258
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1259
val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1260
fun bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1261
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1262
(* Smash a block matrix into components.                                     *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1263
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1264
fun blocks blocksizes bm =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1265
 map (fn (bs,b0) =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1266
      let val m = Inttriplefunc.fold
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1267
          (fn ((b,i,j),c) => fn a => if b = b0 then Intpairfunc.update ((i,j),c) a else a) bm Intpairfunc.undefined
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1268
          val d = Intpairfunc.fold (fn ((i,j),c) => fn a => max a (max i j)) m 0 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1269
      in (((bs,bs),m):matrix) end)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1270
 (blocksizes ~~ (1 upto length blocksizes));;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1271
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1272
(* FIXME : Get rid of this !!!*)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1273
fun tryfind f [] = error "tryfind"
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1274
  | tryfind f (x::xs) = (f x handle ERROR _ => tryfind f xs);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1275
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1276
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1277
(* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1278
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1279
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1280
local
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1281
 open RealArith
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1282
in
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1283
fun real_positivnullstellensatz_general linf d eqs leqs pol =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1284
let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1285
 val vars = fold_rev (curry (gen_union (op aconvc)) o poly_variables) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1286
              (pol::eqs @ map fst leqs) []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1287
 val monoid = if linf then 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1288
      (poly_const rat_1,Rational_lt rat_1)::
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1289
      (filter (fn (p,c) => multidegree p <= d) leqs)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1290
    else enumerate_products d leqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1291
 val nblocks = length monoid
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1292
 fun mk_idmultiplier k p =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1293
  let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1294
   val e = d - multidegree p
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1295
   val mons = enumerate_monomials e vars
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1296
   val nons = mons ~~ (1 upto length mons) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1297
  in (mons,
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1298
      fold_rev (fn (m,n) => Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons Monomialfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1299
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1300
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1301
 fun mk_sqmultiplier k (p,c) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1302
  let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1303
   val e = (d - multidegree p) div 2
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1304
   val mons = enumerate_monomials e vars
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1305
   val nons = mons ~~ (1 upto length mons) 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1306
  in (mons, 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1307
      fold_rev (fn (m1,n1) =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1308
       fold_rev (fn (m2,n2) => fn  a =>
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1309
        let val m = monomial_mul m1 m2 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1310
        in if n1 > n2 then a else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1311
          let val c = if n1 = n2 then rat_1 else rat_2
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1312
              val e = Monomialfunc.tryapplyd a m Inttriplefunc.undefined 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1313
          in Monomialfunc.update(m, tri_equation_add (Inttriplefunc.onefunc((k,n1,n2), c)) e) a
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1314
          end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1315
        end)  nons)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1316
       nons Monomialfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1317
  end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1318
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1319
  val (sqmonlist,sqs) = split_list (map2 mk_sqmultiplier (1 upto length monoid) monoid)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1320
  val (idmonlist,ids) =  split_list(map2 mk_idmultiplier (1 upto length eqs) eqs)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1321
  val blocksizes = map length sqmonlist
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1322
  val bigsum =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1323
    fold_rev2 (fn p => fn q => fn a => tri_epoly_pmul p q a) eqs ids
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1324
            (fold_rev2 (fn (p,c) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1325
                     (epoly_of_poly(poly_neg pol)))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1326
  val eqns = Monomialfunc.fold (fn (m,e) => fn a => e::a) bigsum []
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1327
  val (pvs,assig) = tri_eliminate_all_equations (0,0,0) eqns
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1328
  val qvars = (0,0,0)::pvs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1329
  val allassig = fold_rev (fn v => Inttriplefunc.update(v,(Inttriplefunc.onefunc(v,rat_1)))) pvs assig
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1330
  fun mk_matrix v =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1331
    Inttriplefunc.fold (fn ((b,i,j), ass) => fn m => 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1332
        if b < 0 then m else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1333
         let val c = Inttriplefunc.tryapplyd ass v rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1334
         in if c = rat_0 then m else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1335
            Inttriplefunc.update ((b,j,i), c) (Inttriplefunc.update ((b,i,j), c) m)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1336
         end)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1337
          allassig Inttriplefunc.undefined
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1338
  val diagents = Inttriplefunc.fold
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1339
    (fn ((b,i,j), e) => fn a => if b > 0 andalso i = j then tri_equation_add e a else a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1340
    allassig Inttriplefunc.undefined
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1341
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1342
  val mats = map mk_matrix qvars
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1343
  val obj = (length pvs,
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1344
            itern 1 pvs (fn v => fn i => Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1345
                        Intfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1346
  val raw_vec = if null pvs then vector_0 0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1347
                else tri_scale_then (csdp nblocks blocksizes) obj mats
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1348
  fun int_element (d,v) i = Intfunc.tryapplyd v i rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1349
  fun cterm_element (d,v) i = Ctermfunc.tryapplyd v i rat_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1350
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1351
  fun find_rounding d =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1352
   let 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1353
    val _ = if !debugging 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1354
          then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n") 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1355
          else ()
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1356
    val vec = nice_vector d raw_vec
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1357
    val blockmat = iter (1,dim vec)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1358
     (fn i => fn a => bmatrix_add (bmatrix_cmul (int_element vec i) (nth mats i)) a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1359
     (bmatrix_neg (nth mats 0))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1360
    val allmats = blocks blocksizes blockmat 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1361
   in (vec,map diag allmats)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1362
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1363
  val (vec,ratdias) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1364
    if null pvs then find_rounding rat_1
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1365
    else tryfind find_rounding (map Rat.rat_of_int (1 upto 31) @
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1366
                                map pow2 (5 upto 66))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1367
  val newassigs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1368
    fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1369
           (1 upto dim vec) (Inttriplefunc.onefunc ((0,0,0), Rat.rat_of_int ~1))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1370
  val finalassigs =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1371
    Inttriplefunc.fold (fn (v,e) => fn a => Inttriplefunc.update(v, tri_equation_eval newassigs e) a) allassig newassigs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1372
  fun poly_of_epoly p =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1373
    Monomialfunc.fold (fn (v,e) => fn a => Monomialfunc.updatep iszero (v,tri_equation_eval finalassigs e) a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1374
          p Monomialfunc.undefined
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1375
  fun  mk_sos mons =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1376
   let fun mk_sq (c,m) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1377
    (c,fold_rev (fn k=> fn a => Monomialfunc.updatep iszero (nth mons (k - 1), int_element m k) a)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1378
                 (1 upto length mons) Monomialfunc.undefined)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1379
   in map mk_sq
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1380
   end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1381
  val sqs = map2 mk_sos sqmonlist ratdias
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1382
  val cfs = map poly_of_epoly ids
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1383
  val msq = filter (fn (a,b) => not (null b)) (map2 pair monoid sqs)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1384
  fun eval_sq sqs = fold_rev (fn (c,q) => poly_add (poly_cmul c (poly_mul q q))) sqs poly_0
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1385
  val sanity =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1386
    fold_rev (fn ((p,c),s) => poly_add (poly_mul p (eval_sq s))) msq
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1387
           (fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1388
                    (poly_neg pol))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1389
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1390
in if not(Monomialfunc.is_undefined sanity) then raise Sanity else
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1391
  (cfs,map (fn (a,b) => (snd a,b)) msq)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1392
 end
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1393
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1394
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1395
end;
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1396
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1397
(* Iterative deepening.                                                      *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1398
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1399
fun deepen f n = 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1400
  (writeln ("Searching with depth limit " ^ string_of_int n) ; (f n handle ERROR s => (writeln ("failed with message: " ^ s) ; deepen f (n+1))))
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1401
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1402
(* The ordering so we can create canonical HOL polynomials.                  *)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1403
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1404
fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1405
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1406
fun monomial_order (m1,m2) =
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1407
 if Ctermfunc.is_undefined m2 then LESS 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
  1408
 else if Ctermfunc.is_undefined m1 then GREATER 
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb