author | Philipp Meyer |
Fri, 24 Jul 2009 13:56:02 +0200 | |
changeset 32268 | d50f0cb67578 |
parent 32150 | 4ed2865f3a56 |
permissions | -rw-r--r-- |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1 |
(* Title: sum_of_squares.ML |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
2 |
Authors: Amine Chaieb, University of Cambridge |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
3 |
Philipp Meyer, TU Muenchen |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
4 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
5 |
A tactic for proving nonlinear inequalities |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
6 |
*) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
7 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
8 |
signature SOS = |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
9 |
sig |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
10 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
11 |
val sos_tac : (string -> string) -> Proof.context -> int -> Tactical.tactic |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
12 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
13 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
14 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
15 |
structure Sos : SOS = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
16 |
struct |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
17 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
18 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
19 |
val rat_0 = Rat.zero; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
20 |
val rat_1 = Rat.one; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
21 |
val rat_2 = Rat.two; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
22 |
val rat_10 = Rat.rat_of_int 10; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
23 |
val rat_1_2 = rat_1 // rat_2; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
24 |
val max = curry IntInf.max; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
25 |
val min = curry IntInf.min; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
26 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
27 |
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
|
28 |
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
|
29 |
fun int_of_rat a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
30 |
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
|
31 |
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
|
32 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
33 |
fun rat_pow r i = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
34 |
let fun pow r i = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
35 |
if i = 0 then rat_1 else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
36 |
let val d = pow r (i div 2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
37 |
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
|
38 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
39 |
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
|
40 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
41 |
fun round_rat r = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
42 |
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
|
43 |
val d = a div b |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
44 |
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
|
45 |
val x2 = 2 * (a - (b * d)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
46 |
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
|
47 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
48 |
val abs_rat = Rat.abs; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
49 |
val pow2 = rat_pow rat_2; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
50 |
val pow10 = rat_pow rat_10; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
51 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
52 |
val debugging = ref false; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
53 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
54 |
exception Sanity; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
55 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
56 |
exception Unsolvable; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
57 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
58 |
(* 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
|
59 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
60 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
61 |
fun normalize y = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
else 0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
65 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
66 |
fun decimalize d x = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
67 |
if x =/ rat_0 then "0.0" else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
68 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
69 |
val y = Rat.abs x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
70 |
val e = normalize y |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
71 |
val z = pow10(~ e) */ y +/ rat_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
72 |
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
|
73 |
in (if x </ rat_0 then "-0." else "0.") ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
74 |
implode(tl(explode(string_of_int k))) ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
75 |
(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
|
76 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
77 |
end; |
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 |
(* Iterations over numbers, and lists indexed by numbers. *) |
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 |
fun itern k l f a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
82 |
case l of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
83 |
[] => a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
84 |
| 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
|
85 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
86 |
fun iter (m,n) f a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
87 |
if n < m then a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
88 |
else iter (m+1,n) f (f m a); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
89 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
90 |
(* The main types. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
91 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
92 |
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
|
93 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
94 |
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
|
95 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
96 |
type vector = int* Rat.rat Intfunc.T; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
97 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
98 |
type matrix = (int*int)*(Rat.rat Intpairfunc.T); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
99 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
100 |
type monomial = int Ctermfunc.T; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
101 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
106 |
type poly = Rat.rat Monomialfunc.T; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
107 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
108 |
fun iszero (k,r) = r =/ rat_0; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
109 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
110 |
fun fold_rev2 f l1 l2 b = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
111 |
case (l1,l2) of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
112 |
([],[]) => b |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
113 |
| (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
|
114 |
| _ => error "fold_rev2"; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
115 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
116 |
(* Vectors. Conventionally indexed 1..n. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
117 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
118 |
fun vector_0 n = (n,Intfunc.undefined):vector; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
119 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
120 |
fun dim (v:vector) = fst v; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
121 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
122 |
fun vector_const c n = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
123 |
if c =/ rat_0 then vector_0 n |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
124 |
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
|
125 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
126 |
val vector_1 = vector_const rat_1; |
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_cmul c (v:vector) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
129 |
let val n = dim v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
130 |
in if c =/ rat_0 then vector_0 n |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
131 |
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
|
132 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
133 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
134 |
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
|
135 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
136 |
fun vector_add (v1:vector) (v2:vector) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
137 |
let val m = dim v1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
138 |
val n = dim v2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
139 |
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
|
140 |
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
|
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 |
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
|
144 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
145 |
fun vector_dot (v1:vector) (v2:vector) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
146 |
let val m = dim v1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
147 |
val n = dim v2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
148 |
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
|
149 |
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
|
150 |
(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
|
151 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
152 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
153 |
fun vector_of_list l = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
154 |
let val n = length l |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
155 |
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
|
156 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
157 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
158 |
(* Matrices; again rows and columns indexed from 1. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
159 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
160 |
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
|
161 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
162 |
fun dimensions (m:matrix) = fst m; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
163 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
164 |
fun matrix_const c (mn as (m,n)) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
165 |
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
|
166 |
else if c =/ rat_0 then matrix_0 mn |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
167 |
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
|
168 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
169 |
val matrix_1 = matrix_const rat_1; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
170 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
171 |
fun matrix_cmul c (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
172 |
let val (i,j) = dimensions m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
176 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
177 |
fun matrix_neg (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
178 |
(dimensions m, Intpairfunc.mapf Rat.neg (snd m)) :matrix; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
179 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
180 |
fun matrix_add (m1:matrix) (m2:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
181 |
let val d1 = dimensions m1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
182 |
val d2 = dimensions m2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
183 |
in if d1 <> d2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
184 |
then error "matrix_add: incompatible dimensions" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
185 |
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
|
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 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
|
189 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
190 |
fun row k (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
191 |
let val (i,j) = dimensions m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
192 |
in (j, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
193 |
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
|
194 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
195 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
196 |
fun column k (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
197 |
let val (i,j) = dimensions m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
198 |
in (i, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
199 |
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
|
200 |
: vector |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
201 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
202 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
203 |
fun transp (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
204 |
let val (i,j) = dimensions m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
205 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
206 |
((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
|
207 |
end; |
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 diagonal (v:vector) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
210 |
let val n = dim v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
211 |
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
|
212 |
end; |
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 matrix_of_list l = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
215 |
let val m = length l |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
216 |
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
|
217 |
let val n = length (hd l) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
218 |
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
|
219 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
220 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
221 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
222 |
(* Monomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
223 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
224 |
fun monomial_eval assig (m:monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
225 |
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
|
226 |
m rat_1; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
227 |
val monomial_1 = (Ctermfunc.undefined:monomial); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
228 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
229 |
fun monomial_var x = Ctermfunc.onefunc (x, 1) :monomial; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
230 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
231 |
val (monomial_mul:monomial->monomial->monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
232 |
Ctermfunc.combine (curry op +) (K false); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
233 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
234 |
fun monomial_pow (m:monomial) k = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
235 |
if k = 0 then monomial_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
236 |
else Ctermfunc.mapf (fn x => k * x) m; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
237 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
238 |
fun monomial_divides (m1:monomial) (m2:monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
239 |
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
|
240 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
241 |
fun monomial_div (m1:monomial) (m2:monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
242 |
let val m = Ctermfunc.combine (curry op +) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
243 |
(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
|
244 |
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
|
245 |
else error "monomial_div: non-divisible" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
246 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
247 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
248 |
fun monomial_degree x (m:monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
249 |
Ctermfunc.tryapplyd m x 0;; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
250 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
251 |
fun monomial_lcm (m1:monomial) (m2:monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
252 |
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
|
253 |
(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
|
254 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
255 |
fun monomial_multidegree (m:monomial) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
256 |
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
|
257 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
258 |
fun monomial_variables m = Ctermfunc.dom m;; |
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 |
(* Polynomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
261 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
262 |
fun eval assig (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
263 |
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
|
264 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
265 |
val poly_0 = (Monomialfunc.undefined:poly); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
266 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
267 |
fun poly_isconst (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
268 |
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
|
269 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
270 |
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
|
271 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
272 |
fun poly_const c = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
273 |
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
|
274 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
275 |
fun poly_cmul c (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
276 |
if c =/ rat_0 then poly_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
277 |
else Monomialfunc.mapf (fn x => c */ x) p; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
278 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
279 |
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
|
280 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
281 |
fun poly_add (p1:poly) (p2:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
282 |
(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
|
283 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
284 |
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
|
285 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
286 |
fun poly_cmmul (c,m) (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
287 |
if c =/ rat_0 then poly_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
288 |
else if Ctermfunc.is_undefined m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
289 |
then Monomialfunc.mapf (fn d => c */ d) p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
290 |
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
|
291 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
292 |
fun poly_mul (p1:poly) (p2:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
293 |
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
|
294 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
295 |
fun poly_div (p1:poly) (p2:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
296 |
if not(poly_isconst p2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
297 |
then error "poly_div: non-constant" else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
298 |
let val c = eval Ctermfunc.undefined p2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
299 |
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
|
300 |
else poly_cmul (Rat.inv c) p1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
301 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
302 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
303 |
fun poly_square p = poly_mul p p; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
304 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
305 |
fun poly_pow p k = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
306 |
if k = 0 then poly_const rat_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
307 |
else if k = 1 then p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
308 |
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
|
309 |
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
|
310 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
311 |
fun poly_exp p1 p2 = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
312 |
if not(poly_isconst p2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
313 |
then error "poly_exp: not a constant" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
314 |
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
|
315 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
316 |
fun degree x (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
317 |
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
|
318 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
319 |
fun multidegree (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
320 |
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
|
321 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
322 |
fun poly_variables (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
323 |
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
|
324 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
325 |
(* Order monomials for human presentation. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
326 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
327 |
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
|
328 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
329 |
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
|
330 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
331 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
332 |
fun ord (l1,l2) = case (l1,l2) of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
333 |
(_,[]) => LESS |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
334 |
| ([],_) => GREATER |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
335 |
| (h1::t1,h2::t2) => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
336 |
(case humanorder_varpow (h1, h2) of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
337 |
LESS => LESS |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
338 |
| EQUAL => ord (t1,t2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
339 |
| GREATER => GREATER) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
340 |
in fun humanorder_monomial m1 m2 = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
341 |
ord (sort humanorder_varpow (Ctermfunc.graph m1), |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
342 |
sort humanorder_varpow (Ctermfunc.graph m2)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
343 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
344 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
345 |
fun fold1 f l = case l of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
346 |
[] => error "fold1" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
347 |
| [x] => x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
348 |
| (h::t) => f h (fold1 f t); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
349 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
350 |
(* Conversions to strings. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
351 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
352 |
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
|
353 |
let val n_raw = dim v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
354 |
in if n_raw = 0 then "[]" else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
355 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
356 |
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
|
357 |
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
|
358 |
in "[" ^ fold1 (fn s => fn t => s ^ ", " ^ t) xs ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
359 |
(if n_raw > max_size then ", ...]" else "]") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
360 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
361 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
362 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
363 |
fun string_of_matrix max_size (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
364 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
365 |
val (i_raw,j_raw) = dimensions m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
366 |
val i = min max_size i_raw |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
367 |
val j = min max_size j_raw |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
368 |
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
|
369 |
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
|
370 |
(if j > max_size then "\n ...]" else "]") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
371 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
372 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
373 |
fun string_of_term t = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
374 |
case t of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
375 |
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
|
376 |
| Abs x => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
377 |
let val (xn, b) = Term.dest_abs x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
378 |
in "(\\"^xn^"."^(string_of_term b)^")" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
379 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
380 |
| Const(s,_) => s |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
381 |
| Free (s,_) => s |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
382 |
| Var((s,_),_) => s |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
383 |
| _ => error "string_of_term"; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
384 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
385 |
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
|
386 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
387 |
fun string_of_varpow x k = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
388 |
if k = 1 then string_of_cterm x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
389 |
else string_of_cterm x^"^"^string_of_int k; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
390 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
391 |
fun string_of_monomial m = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
392 |
if Ctermfunc.is_undefined m then "1" else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
393 |
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
|
394 |
(sort humanorder_varpow (Ctermfunc.graph m)) [] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
395 |
in fold1 (fn s => fn t => s^"*"^t) vps |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
396 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
397 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
398 |
fun string_of_cmonomial (c,m) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
399 |
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
|
400 |
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
|
401 |
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
|
402 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
403 |
fun string_of_poly (p:poly) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
404 |
if Monomialfunc.is_undefined p then "<<0>>" else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
405 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
406 |
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
|
407 |
val s = fold (fn (m,c) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
408 |
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
|
409 |
else a ^ " + " ^ string_of_cmonomial(c,m)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
410 |
cms "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
411 |
val s1 = String.substring (s, 0, 3) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
412 |
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
|
413 |
in "<<" ^(if s1 = " + " then s2 else "-"^s2)^">>" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
414 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
415 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
416 |
(* Conversion from HOL term. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
417 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
418 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
419 |
val neg_tm = @{cterm "uminus :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
420 |
val add_tm = @{cterm "op + :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
421 |
val sub_tm = @{cterm "op - :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
422 |
val mul_tm = @{cterm "op * :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
423 |
val inv_tm = @{cterm "inverse :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
424 |
val div_tm = @{cterm "op / :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
425 |
val pow_tm = @{cterm "op ^ :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
426 |
val zero_tm = @{cterm "0:: real"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
427 |
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
|
428 |
fun is_comb t = case t of _$_ => true | _ => false |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
429 |
fun poly_of_term tm = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
430 |
if tm aconvc zero_tm then poly_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
431 |
else if RealArith.is_ratconst tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
432 |
then poly_const(RealArith.dest_ratconst tm) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
433 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
434 |
(let val (lop,r) = Thm.dest_comb tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
435 |
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
|
436 |
else if lop aconvc inv_tm then |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
437 |
let val p = poly_of_term r |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
438 |
in if poly_isconst p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
439 |
then poly_const(Rat.inv (eval Ctermfunc.undefined p)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
440 |
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
|
441 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
442 |
else (let val (opr,l) = Thm.dest_comb lop |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
443 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
444 |
if opr aconvc pow_tm andalso is_numeral r |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
445 |
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
|
446 |
else if opr aconvc add_tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
447 |
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
|
448 |
else if opr aconvc sub_tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
449 |
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
|
450 |
else if opr aconvc mul_tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
451 |
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
|
452 |
else if opr aconvc div_tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
453 |
then let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
454 |
val p = poly_of_term l |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
455 |
val q = poly_of_term r |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
456 |
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
|
457 |
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
|
458 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
459 |
else poly_var tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
460 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
461 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
462 |
handle CTERM ("dest_comb",_) => poly_var tm) |
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 |
handle CTERM ("dest_comb",_) => poly_var tm) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
465 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
466 |
val poly_of_term = fn tm => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
467 |
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
|
468 |
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
|
469 |
end; |
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 of vector (just a list of space-separated numbers). *) |
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_vector (v:vector) = |
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 n = dim v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
476 |
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
|
477 |
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
|
478 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
479 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
480 |
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
|
481 |
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
|
482 |
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
|
483 |
((a,(b,c)),(a',(b',c'))); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
484 |
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
|
485 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
486 |
(* String for block diagonal matrix numbered k. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
487 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
488 |
fun sdpa_of_blockdiagonal k m = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
489 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
490 |
val pfx = string_of_int k ^" " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
491 |
val ents = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
492 |
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
|
493 |
val entss = sort (increasing fst triple_int_ord ) ents |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
494 |
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
|
495 |
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
|
496 |
" " ^ decimalize 20 c ^ "\n" ^ a) entss "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
497 |
end; |
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 |
(* 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
|
500 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
501 |
fun sdpa_of_matrix k (m:matrix) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
502 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
503 |
val pfx = string_of_int k ^ " 1 " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
504 |
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
|
505 |
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
|
506 |
in fold_rev (fn ((i,j),c) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
507 |
pfx ^ string_of_int i ^ " " ^ string_of_int j ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
508 |
" " ^ decimalize 20 c ^ "\n" ^ a) mss "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
509 |
end;; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
510 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
511 |
(* ------------------------------------------------------------------------- *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
512 |
(* String in SDPA sparse format for standard SDP problem: *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
513 |
(* *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
514 |
(* 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
|
515 |
(* Minimize obj_1 * v_1 + ... obj_m * v_m *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
516 |
(* ------------------------------------------------------------------------- *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
517 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
518 |
fun sdpa_of_problem obj mats = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
519 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
520 |
val m = length mats - 1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
521 |
val (n,_) = dimensions (hd mats) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
522 |
in |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
523 |
string_of_int m ^ "\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
524 |
"1\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
525 |
string_of_int n ^ "\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
526 |
sdpa_of_vector obj ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
527 |
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
|
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 index_char str chr pos = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
531 |
if pos >= String.size str then ~1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
532 |
else if String.sub(str,pos) = chr then pos |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
533 |
else index_char str chr (pos + 1); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
534 |
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
|
535 |
fun rat_of_string s = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
536 |
let val n = index_char s #"/" 0 in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
537 |
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
|
538 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
539 |
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
|
540 |
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
|
541 |
in rat_of_quotient(numer, den) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
542 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
543 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
544 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
545 |
fun isspace x = x = " " ; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
546 |
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
|
547 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
548 |
(* More parser basics. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
549 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
550 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
551 |
open Scan |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
552 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
553 |
val word = this_string |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
554 |
fun token s = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
555 |
repeat ($$ " ") |-- word s --| repeat ($$ " ") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
556 |
val numeral = one isnum |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
557 |
val decimalint = bulk numeral >> (rat_of_string o implode) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
558 |
val decimalfrac = bulk numeral |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
559 |
>> (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
|
560 |
val decimalsig = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
561 |
decimalint -- option (Scan.$$ "." |-- decimalfrac) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
562 |
>> (fn (h,NONE) => h | (h,SOME x) => h +/ x) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
563 |
fun signed prs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
564 |
$$ "-" |-- prs >> Rat.neg |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
565 |
|| $$ "+" |-- prs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
566 |
|| prs; |
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 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
|
569 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
570 |
val exponent = ($$ "e" || $$ "E") |-- signed decimalint; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
571 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
572 |
val decimal = signed decimalsig -- (emptyin rat_0|| exponent) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
573 |
>> (fn (h, x) => h */ pow10 (int_of_rat x)); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
574 |
end; |
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 |
fun mkparser p s = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
577 |
let val (x,rst) = p (explode s) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
578 |
in if null rst then x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
579 |
else error "mkparser: unparsed input" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
580 |
end;; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
581 |
val parse_decimal = mkparser decimal; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
582 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
583 |
fun fix err prs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
584 |
prs || (fn x=> error err); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
585 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
586 |
fun listof prs sep err = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
587 |
prs -- Scan.bulk (sep |-- fix err prs) >> uncurry cons; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
588 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
589 |
(* Parse back a vector. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
590 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
591 |
val vector = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
592 |
token "{" |-- listof decimal (token ",") "decimal" --| token "}" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
593 |
>> vector_of_list |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
594 |
val parse_vector = mkparser vector |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
595 |
fun skipupto dscr prs inp = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
596 |
(dscr |-- prs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
597 |
|| Scan.one (K true) |-- skipupto dscr prs) inp |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
598 |
fun ignore inp = ((),[]) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
599 |
fun sdpaoutput inp = skipupto (word "xVec" -- token "=") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
600 |
(vector --| ignore) inp |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
601 |
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
|
602 |
val parse_sdpaoutput = mkparser sdpaoutput |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
603 |
val parse_csdpoutput = mkparser csdpoutput |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
604 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
605 |
(* Run prover on a problem in linear form. *) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
606 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
607 |
fun run_problem prover obj mats = |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
608 |
parse_csdpoutput (prover (sdpa_of_problem obj mats)) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
609 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
610 |
(* |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
611 |
UNUSED |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
612 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
613 |
(* 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
|
614 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
615 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
616 |
val prs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
617 |
skipupto (word "phase.value" -- token "=") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
618 |
(Scan.option (Scan.$$ "p") -- Scan.option (Scan.$$ "d") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
619 |
-- (word "OPT" || word "FEAS")) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
620 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
621 |
fun sdpa_run_succeeded s = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
622 |
(prs (explode s); true) handle _ => false |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
623 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
624 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
625 |
(* 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
|
626 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
627 |
val sdpa_default_parameters = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
628 |
"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
|
629 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
630 |
(* 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
|
631 |
(* 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
|
632 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
633 |
val sdpa_alt_parameters = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
634 |
"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
|
635 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
636 |
val sdpa_params = sdpa_alt_parameters;; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
637 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
638 |
(* 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
|
639 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
640 |
val csdp_default_parameters = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
641 |
"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
|
642 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
643 |
val csdp_params = csdp_default_parameters;; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
644 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
645 |
fun tmp_file pre suf = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
646 |
let val i = string_of_int (round (random())) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
647 |
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
|
648 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
649 |
if File.exists name then tmp_file pre suf |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
650 |
else name |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
651 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
652 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
653 |
(* 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
|
654 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
655 |
fun run_sdpa dbg obj mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
656 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
657 |
val input_file = tmp_file "sos" ".dat-s" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
658 |
val output_file = tmp_file "sos" ".out" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
659 |
val params_file = tmp_file "param" ".sdpa" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
660 |
val current_dir = File.pwd() |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
661 |
val _ = File.write input_file |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
662 |
(sdpa_of_problem "" obj mats) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
663 |
val _ = File.write params_file sdpa_params |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
664 |
val _ = File.cd (Path.variable "ISABELLE_TMP") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
665 |
val _ = File.system_command ("sdpa "^ (Path.implode input_file) ^ " " ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
666 |
(Path.implode output_file) ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
667 |
(if dbg then "" else "> /dev/null")) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
668 |
val opr = File.read output_file |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
669 |
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
|
670 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
671 |
let val res = parse_sdpaoutput opr |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
672 |
in ((if dbg then () |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
673 |
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
|
674 |
res) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
675 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
676 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
677 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
678 |
fun sdpa obj mats = run_sdpa (!debugging) obj mats; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
679 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
680 |
(* The same thing with CSDP. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
681 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
682 |
fun run_csdp dbg obj mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
683 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
684 |
val input_file = tmp_file "sos" ".dat-s" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
685 |
val output_file = tmp_file "sos" ".out" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
686 |
val params_file = tmp_file "param" ".csdp" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
687 |
val current_dir = File.pwd() |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
688 |
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
|
689 |
val _ = File.write params_file csdp_params |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
690 |
val _ = File.cd (Path.variable "ISABELLE_TMP") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
691 |
val rv = system ("csdp "^(Path.implode input_file) ^ " " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
692 |
^ (Path.implode output_file) ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
693 |
(if dbg then "" else "> /dev/null")) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
694 |
val opr = File.read output_file |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
695 |
val res = parse_csdpoutput opr |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
696 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
697 |
((if dbg then () |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
698 |
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
|
699 |
(rv,res)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
700 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
701 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
702 |
fun csdp obj mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
703 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
704 |
val (rv,res) = run_csdp (!debugging) obj mats |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
705 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
706 |
((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
|
707 |
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
|
708 |
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
|
709 |
else ()); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
710 |
res) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
711 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
712 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
713 |
*) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
714 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
715 |
(* 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
|
716 |
(* 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
|
717 |
(* 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
|
718 |
(* are extreme numbers in the original problem. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
719 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
720 |
(* Version for (int*int) keys *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
721 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
722 |
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
|
723 |
fun common_denominator fld amat acc = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
724 |
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
|
725 |
fun maximal_element fld amat acc = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
726 |
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
|
727 |
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
|
728 |
in Real.fromLargeInt a / Real.fromLargeInt b end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
729 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
730 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
731 |
fun pi_scale_then solver (obj:vector) mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
732 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
733 |
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
|
734 |
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
|
735 |
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
|
736 |
val obj' = vector_cmul cd2 obj |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
737 |
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
|
738 |
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
|
739 |
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
|
740 |
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
|
741 |
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
|
742 |
val obj'' = vector_cmul scal2 obj' |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
743 |
in solver obj'' mats'' |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
744 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
745 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
746 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
747 |
(* 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
|
748 |
(* 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
|
749 |
(* 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
|
750 |
(* are extreme numbers in the original problem. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
751 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
752 |
(* Version for (int*int*int) keys *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
753 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
754 |
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
|
755 |
fun common_denominator fld amat acc = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
756 |
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
|
757 |
fun maximal_element fld amat acc = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
758 |
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
|
759 |
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
|
760 |
in Real.fromLargeInt a / Real.fromLargeInt b end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
761 |
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
|
762 |
in |
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 |
fun tri_scale_then solver (obj:vector) mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
765 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
766 |
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
|
767 |
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
|
768 |
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
|
769 |
val obj' = vector_cmul cd2 obj |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
770 |
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
|
771 |
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
|
772 |
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
|
773 |
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
|
774 |
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
|
775 |
val obj'' = vector_cmul scal2 obj' |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
776 |
in solver obj'' mats'' |
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 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
779 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
780 |
(* Round a vector to "nice" rationals. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
781 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
782 |
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
|
783 |
fun nice_vector n ((d,v) : vector) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
784 |
(d, Intfunc.fold (fn (i,c) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
785 |
let val y = nice_rational n c |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
786 |
in if c =/ rat_0 then a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
787 |
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
|
788 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
789 |
(* |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
790 |
UNUSED |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
791 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
792 |
(* 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
|
793 |
(* 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
|
794 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
795 |
fun linear_program_basic a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
796 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
797 |
val (m,n) = dimensions a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
798 |
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
|
799 |
val obj = vector_const rat_1 m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
800 |
val (rv,res) = run_csdp false obj mats |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
801 |
in if rv = 1 orelse rv = 2 then false |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
802 |
else if rv = 0 then true |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
803 |
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
|
804 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
805 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
806 |
(* 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
|
807 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
808 |
fun linear_program a b = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
809 |
let val (m,n) = dimensions a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
810 |
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
|
811 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
812 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
813 |
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
|
814 |
val obj = vector_const rat_1 m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
815 |
val (rv,res) = run_csdp false obj mats |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
816 |
in if rv = 1 orelse rv = 2 then false |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
817 |
else if rv = 0 then true |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
818 |
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
|
819 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
820 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
821 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
822 |
(* 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
|
823 |
(* computational geometry, express as linear inequalities and call CSDP. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
824 |
(* 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
|
825 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
826 |
fun in_convex_hull pts pt = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
827 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
828 |
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
|
829 |
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
|
830 |
val n = length pts + 1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
831 |
val v = 2 * (length pt + 1) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
832 |
val m = v + n - 1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
833 |
val mat = ((m,n), |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
834 |
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
|
835 |
(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
|
836 |
(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
|
837 |
Intpairfunc.undefined)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
838 |
in linear_program_basic mat |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
839 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
840 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
841 |
(* 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
|
842 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
843 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
844 |
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
|
845 |
fun augment m ms = funpow 3 augment1 (m::ms) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
846 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
847 |
fun minimal_convex_hull mons = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
848 |
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
|
849 |
in funpow (length mons') augment1 mons' |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
850 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
851 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
852 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
853 |
*) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
854 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
855 |
fun dest_ord f x = is_equal (f x); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
856 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
857 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
858 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
859 |
(* Stuff for "equations" ((int*int*int)->num functions). *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
860 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
861 |
fun tri_equation_cmul c eq = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
862 |
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
|
863 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
864 |
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
|
865 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
866 |
fun tri_equation_eval assig eq = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
867 |
let fun value v = Inttriplefunc.apply assig v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
868 |
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
|
869 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
870 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
871 |
(* Eliminate among linear equations: return unconstrained variables and *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
872 |
(* 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
|
873 |
(* "one" that's used for a constant term. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
874 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
875 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
876 |
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
|
877 |
[] => error "extract_first" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
878 |
| h::t => if p h then (h,t) else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
879 |
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
|
880 |
fun eliminate vars dun eqs = case vars of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
881 |
[] => if forall Inttriplefunc.is_undefined eqs then dun |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
882 |
else raise Unsolvable |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
883 |
| v::vs => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
884 |
((let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
885 |
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
|
886 |
val a = Inttriplefunc.apply eq v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
887 |
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
|
888 |
fun elim e = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
889 |
let val b = Inttriplefunc.tryapplyd e v rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
890 |
in if b =/ rat_0 then e else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
891 |
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
|
892 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
893 |
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
|
894 |
end) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
895 |
handle ERROR _ => eliminate vs dun eqs) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
896 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
897 |
fun tri_eliminate_equations one vars eqs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
898 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
899 |
val assig = eliminate vars Inttriplefunc.undefined eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
900 |
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
|
901 |
in (distinct (dest_ord triple_int_ord) vs, assig) |
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 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
904 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
905 |
(* Eliminate all variables, in an essentially arbitrary order. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
906 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
907 |
fun tri_eliminate_all_equations one = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
908 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
909 |
fun choose_variable eq = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
910 |
let val (v,_) = Inttriplefunc.choose eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
911 |
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
|
912 |
let val eq' = Inttriplefunc.undefine v eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
913 |
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
|
914 |
else fst (Inttriplefunc.choose eq') |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
915 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
916 |
else v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
917 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
918 |
fun eliminate dun eqs = case eqs of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
919 |
[] => dun |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
920 |
| eq::oeqs => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
921 |
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
|
922 |
let val v = choose_variable eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
923 |
val a = Inttriplefunc.apply eq v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
924 |
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
|
925 |
(Inttriplefunc.undefine v eq) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
926 |
fun elim e = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
927 |
let val b = Inttriplefunc.tryapplyd e v rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
928 |
in if b =/ rat_0 then e |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
929 |
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
|
930 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
931 |
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
|
932 |
(map elim oeqs) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
933 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
934 |
in fn eqs => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
935 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
936 |
val assig = eliminate Inttriplefunc.undefined eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
937 |
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
|
938 |
in (distinct (dest_ord triple_int_ord) vs,assig) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
939 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
940 |
end; |
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 |
(* Solve equations by assigning arbitrary numbers. *) |
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_solve_equations one eqs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
945 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
946 |
val (vars,assigs) = tri_eliminate_all_equations one eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
947 |
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
|
948 |
(Inttriplefunc.onefunc(one, Rat.rat_of_int ~1)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
949 |
val ass = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
950 |
Inttriplefunc.combine (curry op +/) (K false) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
951 |
(Inttriplefunc.mapf (tri_equation_eval vfn) assigs) vfn |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
952 |
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
|
953 |
then Inttriplefunc.undefine one ass else raise Sanity |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
954 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
955 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
956 |
(* 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
|
957 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
958 |
fun tri_epoly_pmul p q acc = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
959 |
Monomialfunc.fold (fn (m1, c) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
960 |
Monomialfunc.fold (fn (m2,e) => fn b => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
961 |
let val m = monomial_mul m1 m2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
962 |
val es = Monomialfunc.tryapplyd b m Inttriplefunc.undefined |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
963 |
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
|
964 |
end) q a) p acc ; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
965 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
966 |
(* Usual operations on equation-parametrized poly. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
967 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
968 |
fun tri_epoly_cmul c l = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
969 |
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
|
970 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
971 |
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
|
972 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
973 |
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
|
974 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
975 |
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
|
976 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
977 |
(* Stuff for "equations" ((int*int)->num functions). *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
978 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
979 |
fun pi_equation_cmul c eq = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
980 |
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
|
981 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
982 |
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
|
983 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
984 |
fun pi_equation_eval assig eq = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
985 |
let fun value v = Inttriplefunc.apply assig v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
986 |
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
|
987 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
988 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
989 |
(* Eliminate among linear equations: return unconstrained variables and *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
990 |
(* 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
|
991 |
(* "one" that's used for a constant term. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
992 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
993 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
994 |
fun extract_first p l = case l of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
995 |
[] => error "extract_first" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
996 |
| h::t => if p h then (h,t) else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
997 |
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
|
998 |
fun eliminate vars dun eqs = case vars of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
999 |
[] => if forall Inttriplefunc.is_undefined eqs then dun |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1000 |
else raise Unsolvable |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1001 |
| v::vs => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1002 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1003 |
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
|
1004 |
val a = Inttriplefunc.apply eq v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1005 |
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
|
1006 |
fun elim e = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1007 |
let val b = Inttriplefunc.tryapplyd e v rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1008 |
in if b =/ rat_0 then e else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1009 |
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
|
1010 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1011 |
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
|
1012 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1013 |
handle ERROR _ => eliminate vs dun eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1014 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1015 |
fun pi_eliminate_equations one vars eqs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1016 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1017 |
val assig = eliminate vars Inttriplefunc.undefined eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1018 |
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
|
1019 |
in (distinct (dest_ord triple_int_ord) vs, assig) |
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 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1022 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1023 |
(* Eliminate all variables, in an essentially arbitrary order. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1024 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1025 |
fun pi_eliminate_all_equations one = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1026 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1027 |
fun choose_variable eq = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1028 |
let val (v,_) = Inttriplefunc.choose eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1029 |
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
|
1030 |
let val eq' = Inttriplefunc.undefine v eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1031 |
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
|
1032 |
else fst (Inttriplefunc.choose eq') |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1033 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1034 |
else v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1035 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1036 |
fun eliminate dun eqs = case eqs of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1037 |
[] => dun |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1038 |
| eq::oeqs => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1039 |
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
|
1040 |
let val v = choose_variable eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1041 |
val a = Inttriplefunc.apply eq v |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1042 |
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
|
1043 |
(Inttriplefunc.undefine v eq) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1044 |
fun elim e = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1045 |
let val b = Inttriplefunc.tryapplyd e v rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1046 |
in if b =/ rat_0 then e |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1047 |
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
|
1048 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1049 |
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
|
1050 |
(map elim oeqs) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1051 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1052 |
in fn eqs => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1053 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1054 |
val assig = eliminate Inttriplefunc.undefined eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1055 |
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
|
1056 |
in (distinct (dest_ord triple_int_ord) vs,assig) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1057 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1058 |
end; |
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 |
(* Solve equations by assigning arbitrary numbers. *) |
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_solve_equations one eqs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1063 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1064 |
val (vars,assigs) = pi_eliminate_all_equations one eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1065 |
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
|
1066 |
(Inttriplefunc.onefunc(one, Rat.rat_of_int ~1)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1067 |
val ass = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1068 |
Inttriplefunc.combine (curry op +/) (K false) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1069 |
(Inttriplefunc.mapf (pi_equation_eval vfn) assigs) vfn |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1070 |
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
|
1071 |
then Inttriplefunc.undefine one ass else raise Sanity |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1072 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1073 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1074 |
(* 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
|
1075 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1076 |
fun pi_epoly_pmul p q acc = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1077 |
Monomialfunc.fold (fn (m1, c) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1078 |
Monomialfunc.fold (fn (m2,e) => fn b => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1079 |
let val m = monomial_mul m1 m2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1080 |
val es = Monomialfunc.tryapplyd b m Inttriplefunc.undefined |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1081 |
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
|
1082 |
end) q a) p acc ; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1083 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1084 |
(* Usual operations on equation-parametrized poly. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1085 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1086 |
fun pi_epoly_cmul c l = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1087 |
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
|
1088 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1089 |
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
|
1090 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1091 |
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
|
1092 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1093 |
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
|
1094 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1095 |
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
|
1096 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1097 |
(* 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
|
1098 |
(* 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
|
1099 |
(* 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
|
1100 |
(* vol 45, pp. 363--374, 1978. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1101 |
(* *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1102 |
(* 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
|
1103 |
(* 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
|
1104 |
(* quadratic form that will tend to display constants. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1105 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1106 |
(* |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1107 |
UNUSED |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1108 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1109 |
fun newton_polytope pol = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1110 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1111 |
val vars = poly_variables pol |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1112 |
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
|
1113 |
(Monomialfunc.dom pol) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1114 |
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
|
1115 |
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
|
1116 |
val mons' = minimal_convex_hull mons |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1117 |
val all' = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1118 |
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
|
1119 |
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
|
1120 |
vars m monomial_1) (rev all') |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1121 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1122 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1123 |
*) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1124 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1125 |
(* 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
|
1126 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1127 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1128 |
fun diagonalize n i m = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1129 |
if Intpairfunc.is_undefined (snd m) then [] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1130 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1131 |
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
|
1132 |
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
|
1133 |
else if a11 =/ rat_0 then |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1134 |
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
|
1135 |
else error "diagonalize: not PSD ___ " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1136 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1137 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1138 |
val v = row i m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1139 |
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
|
1140 |
let val y = c // a11 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1141 |
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
|
1142 |
end) (snd v) Intfunc.undefined) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1143 |
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
|
1144 |
val m' = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1145 |
((n,n), |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1146 |
iter (i+1,n) (fn j => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1147 |
iter (i+1,n) (fn k => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1148 |
(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
|
1149 |
Intpairfunc.undefined) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1150 |
in (a11,v')::diagonalize n (i + 1) m' |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1151 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1152 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1153 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1154 |
fun diag m = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1155 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1156 |
val nn = dimensions m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1157 |
val n = fst nn |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1158 |
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
|
1159 |
else diagonalize n 1 m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1160 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1161 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1162 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1163 |
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
|
1164 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1165 |
(* Adjust a diagonalization to collect rationals at the start. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1166 |
(* FIXME : Potentially polymorphic keys, but here only: integers!! *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1167 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1168 |
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
|
1169 |
fun mapa f (d,v) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1170 |
(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
|
1171 |
fun adj (c,l) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1172 |
let val a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1173 |
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
|
1174 |
(snd l) rat_1 // |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1175 |
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
|
1176 |
(snd l) rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1177 |
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
|
1178 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1179 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1180 |
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
|
1181 |
let val d' = map adj d |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1182 |
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
|
1183 |
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
|
1184 |
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
|
1185 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1186 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1187 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1188 |
(* Enumeration of monomials with given multidegree bound. *) |
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 |
fun enumerate_monomials d vars = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1191 |
if d < 0 then [] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1192 |
else if d = 0 then [Ctermfunc.undefined] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1193 |
else if null vars then [monomial_1] else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1194 |
let val alts = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1195 |
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
|
1196 |
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
|
1197 |
in fold1 (curry op @) alts |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1198 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1199 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1200 |
(* Enumerate products of distinct input polys with degree <= d. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1201 |
(* We ignore any constant input polynomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1202 |
(* 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
|
1203 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1204 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1205 |
open RealArith |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1206 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1207 |
fun enumerate_products d pols = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1208 |
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
|
1209 |
else if d < 0 then [] else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1210 |
case pols of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1211 |
[] => [(poly_const rat_1,Rational_lt rat_1)] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1212 |
| (p,b)::ps => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1213 |
let val e = multidegree p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1214 |
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
|
1215 |
enumerate_products d ps @ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1216 |
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
|
1217 |
(enumerate_products (d - e) ps) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1218 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1219 |
end; |
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 |
(* 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
|
1222 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1223 |
fun epoly_of_poly p = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1224 |
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
|
1225 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1226 |
(* String for block diagonal matrix numbered k. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1227 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1228 |
fun sdpa_of_blockdiagonal k m = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1229 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1230 |
val pfx = string_of_int k ^" " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1231 |
val ents = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1232 |
Inttriplefunc.fold |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1233 |
(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
|
1234 |
m [] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1235 |
val entss = sort (increasing fst triple_int_ord) ents |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1236 |
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
|
1237 |
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
|
1238 |
" " ^ decimalize 20 c ^ "\n" ^ a) entss "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1239 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1240 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1241 |
(* 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
|
1242 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1243 |
fun sdpa_of_blockproblem nblocks blocksizes obj mats = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1244 |
let val m = length mats - 1 |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1245 |
in |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1246 |
string_of_int m ^ "\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1247 |
string_of_int nblocks ^ "\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1248 |
(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
|
1249 |
"\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1250 |
sdpa_of_vector obj ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1251 |
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
|
1252 |
(1 upto length mats) mats "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1253 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1254 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1255 |
(* Run prover on a problem in block diagonal form. *) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1256 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1257 |
fun run_blockproblem prover nblocks blocksizes obj mats= |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1258 |
parse_csdpoutput (prover (sdpa_of_blockproblem nblocks blocksizes obj mats)) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1259 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1260 |
(* |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1261 |
UNUSED |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1262 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1263 |
(* 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
|
1264 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1265 |
fun run_csdp dbg nblocks blocksizes obj mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1266 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1267 |
val input_file = tmp_file "sos" ".dat-s" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1268 |
val output_file = tmp_file "sos" ".out" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1269 |
val params_file = tmp_file "param" ".csdp" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1270 |
val _ = File.write input_file |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1271 |
(sdpa_of_blockproblem "" nblocks blocksizes obj mats) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1272 |
val _ = File.write params_file csdp_params |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1273 |
val current_dir = File.pwd() |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1274 |
val _ = File.cd (Path.variable "ISABELLE_TMP") |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1275 |
val rv = system ("csdp "^(Path.implode input_file) ^ " " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1276 |
^ (Path.implode output_file) ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1277 |
(if dbg then "" else "> /dev/null")) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1278 |
val opr = File.read output_file |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1279 |
val res = parse_csdpoutput opr |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1280 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1281 |
((if dbg then () |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1282 |
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
|
1283 |
(rv,res)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1284 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1285 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1286 |
fun csdp nblocks blocksizes obj mats = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1287 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1288 |
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
|
1289 |
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
|
1290 |
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
|
1291 |
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
|
1292 |
else ()); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1293 |
res) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1294 |
end; |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1295 |
*) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1296 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1297 |
(* 3D versions of matrix operations to consider blocks separately. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1298 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1299 |
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
|
1300 |
fun bmatrix_cmul c bm = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1301 |
if c =/ rat_0 then Inttriplefunc.undefined |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1302 |
else Inttriplefunc.mapf (fn x => c */ x) bm; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1303 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1304 |
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
|
1305 |
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
|
1306 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1307 |
(* Smash a block matrix into components. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1308 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1309 |
fun blocks blocksizes bm = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1310 |
map (fn (bs,b0) => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1311 |
let val m = Inttriplefunc.fold |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1312 |
(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
|
1313 |
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
|
1314 |
in (((bs,bs),m):matrix) end) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1315 |
(blocksizes ~~ (1 upto length blocksizes));; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1316 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1317 |
(* FIXME : Get rid of this !!!*) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1318 |
local |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1319 |
fun tryfind_with msg f [] = error msg |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1320 |
| tryfind_with msg f (x::xs) = (f x handle ERROR s => tryfind_with s f xs); |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1321 |
in |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1322 |
fun tryfind f = tryfind_with "tryfind" f |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1323 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1324 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1325 |
(* |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1326 |
fun tryfind f [] = error "tryfind" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1327 |
| tryfind f (x::xs) = (f x handle ERROR _ => tryfind f xs); |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1328 |
*) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1329 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1330 |
(* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1331 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1332 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1333 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1334 |
open RealArith |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1335 |
in |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1336 |
fun real_positivnullstellensatz_general prover linf d eqs leqs pol = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1337 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1338 |
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
|
1339 |
(pol::eqs @ map fst leqs) [] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1340 |
val monoid = if linf then |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1341 |
(poly_const rat_1,Rational_lt rat_1):: |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1342 |
(filter (fn (p,c) => multidegree p <= d) leqs) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1343 |
else enumerate_products d leqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1344 |
val nblocks = length monoid |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1345 |
fun mk_idmultiplier k p = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1346 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1347 |
val e = d - multidegree p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1348 |
val mons = enumerate_monomials e vars |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1349 |
val nons = mons ~~ (1 upto length mons) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1350 |
in (mons, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1351 |
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
|
1352 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1353 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1354 |
fun mk_sqmultiplier k (p,c) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1355 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1356 |
val e = (d - multidegree p) div 2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1357 |
val mons = enumerate_monomials e vars |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1358 |
val nons = mons ~~ (1 upto length mons) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1359 |
in (mons, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1360 |
fold_rev (fn (m1,n1) => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1361 |
fold_rev (fn (m2,n2) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1362 |
let val m = monomial_mul m1 m2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1363 |
in if n1 > n2 then a else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1364 |
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
|
1365 |
val e = Monomialfunc.tryapplyd a m Inttriplefunc.undefined |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1366 |
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
|
1367 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1368 |
end) nons) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1369 |
nons Monomialfunc.undefined) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1370 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1371 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1372 |
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
|
1373 |
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
|
1374 |
val blocksizes = map length sqmonlist |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1375 |
val bigsum = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1376 |
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
|
1377 |
(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
|
1378 |
(epoly_of_poly(poly_neg pol))) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1379 |
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
|
1380 |
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
|
1381 |
val qvars = (0,0,0)::pvs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1382 |
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
|
1383 |
fun mk_matrix v = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1384 |
Inttriplefunc.fold (fn ((b,i,j), ass) => fn m => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1385 |
if b < 0 then m else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1386 |
let val c = Inttriplefunc.tryapplyd ass v rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1387 |
in if c = rat_0 then m else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1388 |
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
|
1389 |
end) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1390 |
allassig Inttriplefunc.undefined |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1391 |
val diagents = Inttriplefunc.fold |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1392 |
(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
|
1393 |
allassig Inttriplefunc.undefined |
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 |
val mats = map mk_matrix qvars |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1396 |
val obj = (length pvs, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1397 |
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
|
1398 |
Intfunc.undefined) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1399 |
val raw_vec = if null pvs then vector_0 0 |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1400 |
else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1401 |
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
|
1402 |
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
|
1403 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1404 |
fun find_rounding d = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1405 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1406 |
val _ = if !debugging |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1407 |
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
|
1408 |
else () |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1409 |
val vec = nice_vector d raw_vec |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1410 |
val blockmat = iter (1,dim vec) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1411 |
(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
|
1412 |
(bmatrix_neg (nth mats 0)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1413 |
val allmats = blocks blocksizes blockmat |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1414 |
in (vec,map diag allmats) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1415 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1416 |
val (vec,ratdias) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1417 |
if null pvs then find_rounding rat_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1418 |
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
|
1419 |
map pow2 (5 upto 66)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1420 |
val newassigs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1421 |
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
|
1422 |
(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
|
1423 |
val finalassigs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1424 |
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
|
1425 |
fun poly_of_epoly p = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1426 |
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
|
1427 |
p Monomialfunc.undefined |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1428 |
fun mk_sos mons = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1429 |
let fun mk_sq (c,m) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1430 |
(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
|
1431 |
(1 upto length mons) Monomialfunc.undefined) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1432 |
in map mk_sq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1433 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1434 |
val sqs = map2 mk_sos sqmonlist ratdias |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1435 |
val cfs = map poly_of_epoly ids |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1436 |
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
|
1437 |
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
|
1438 |
val sanity = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1439 |
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
|
1440 |
(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
|
1441 |
(poly_neg pol)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1442 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1443 |
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
|
1444 |
(cfs,map (fn (a,b) => (snd a,b)) msq) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1445 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1446 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1447 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1448 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1449 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1450 |
(* Iterative deepening. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1451 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1452 |
fun deepen f n = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1453 |
(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
|
1454 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1455 |
(* The ordering so we can create canonical HOL polynomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1456 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1457 |
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
|
1458 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1459 |
fun monomial_order (m1,m2) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1460 |
if Ctermfunc.is_undefined m2 then LESS |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1461 |
else if Ctermfunc.is_undefined m1 then GREATER |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1462 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1463 |
let val mon1 = dest_monomial m1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1464 |
val mon2 = dest_monomial m2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1465 |
val deg1 = fold (curry op + o snd) mon1 0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1466 |
val deg2 = fold (curry op + o snd) mon2 0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1467 |
in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1468 |
else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1469 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1470 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1471 |
fun dest_poly p = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1472 |
map (fn (m,c) => (c,dest_monomial m)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1473 |
(sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p)); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1474 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1475 |
(* Map back polynomials and their composites to HOL. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1476 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1477 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1478 |
open Thm Numeral RealArith |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1479 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1480 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1481 |
fun cterm_of_varpow x k = if k = 1 then x else capply (capply @{cterm "op ^ :: real => _"} x) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1482 |
(mk_cnumber @{ctyp nat} k) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1483 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1484 |
fun cterm_of_monomial m = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1485 |
if Ctermfunc.is_undefined m then @{cterm "1::real"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1486 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1487 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1488 |
val m' = dest_monomial m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1489 |
val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1490 |
in fold1 (fn s => fn t => capply (capply @{cterm "op * :: real => _"} s) t) vps |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1491 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1492 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1493 |
fun cterm_of_cmonomial (m,c) = if Ctermfunc.is_undefined m then cterm_of_rat c |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1494 |
else if c = Rat.one then cterm_of_monomial m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1495 |
else capply (capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1496 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1497 |
fun cterm_of_poly p = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1498 |
if Monomialfunc.is_undefined p then @{cterm "0::real"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1499 |
else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1500 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1501 |
val cms = map cterm_of_cmonomial |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1502 |
(sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1503 |
in fold1 (fn t1 => fn t2 => capply(capply @{cterm "op + :: real => _"} t1) t2) cms |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1504 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1505 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1506 |
fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square(cterm_of_poly p)); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1507 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1508 |
fun cterm_of_sos (pr,sqs) = if null sqs then pr |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1509 |
else Product(pr,fold1 (fn a => fn b => Sum(a,b)) (map cterm_of_sqterm sqs)); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1510 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1511 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1512 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1513 |
(* Interface to HOL. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1514 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1515 |
open Thm Conv RealArith |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1516 |
val concl = dest_arg o cprop_of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1517 |
fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1518 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1519 |
(* FIXME: Replace tryfind by get_first !! *) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1520 |
fun real_nonlinear_prover prover ctxt = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1521 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1522 |
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1523 |
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1524 |
simple_cterm_ord |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1525 |
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1526 |
real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1527 |
fun mainf translator (eqs,les,lts) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1528 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1529 |
val eq0 = map (poly_of_term o dest_arg1 o concl) eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1530 |
val le0 = map (poly_of_term o dest_arg o concl) les |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1531 |
val lt0 = map (poly_of_term o dest_arg o concl) lts |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1532 |
val eqp0 = map (fn (t,i) => (t,Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1))) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1533 |
val lep0 = map (fn (t,i) => (t,Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1))) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1534 |
val ltp0 = map (fn (t,i) => (t,Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1))) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1535 |
val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1536 |
val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1537 |
val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1538 |
fun trivial_axiom (p,ax) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1539 |
case ax of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1540 |
Axiom_eq n => if eval Ctermfunc.undefined p <>/ Rat.zero then nth eqs n |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1541 |
else error "trivial_axiom: Not a trivial axiom" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1542 |
| Axiom_le n => if eval Ctermfunc.undefined p </ Rat.zero then nth les n |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1543 |
else error "trivial_axiom: Not a trivial axiom" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1544 |
| Axiom_lt n => if eval Ctermfunc.undefined p <=/ Rat.zero then nth lts n |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1545 |
else error "trivial_axiom: Not a trivial axiom" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1546 |
| _ => error "trivial_axiom: Not a trivial axiom" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1547 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1548 |
((let val th = tryfind trivial_axiom (keq @ klep @ kltp) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1549 |
in fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th end) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1550 |
handle ERROR _ => ( |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1551 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1552 |
val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1553 |
val leq = lep @ ltp |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1554 |
fun tryall d = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1555 |
let val e = multidegree pol |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1556 |
val k = if e = 0 then 0 else d div e |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1557 |
val eq' = map fst eq |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1558 |
in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1559 |
(poly_neg(poly_pow pol i)))) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1560 |
(0 upto k) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1561 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1562 |
val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1563 |
val proofs_ideal = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1564 |
map2 (fn q => fn (p,ax) => Eqmul(cterm_of_poly q,ax)) cert_ideal eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1565 |
val proofs_cone = map cterm_of_sos cert_cone |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1566 |
val proof_ne = if null ltp then Rational_lt Rat.one else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1567 |
let val p = fold1 (fn s => fn t => Product(s,t)) (map snd ltp) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1568 |
in funpow i (fn q => Product(p,q)) (Rational_lt Rat.one) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1569 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1570 |
val proof = fold1 (fn s => fn t => Sum(s,t)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1571 |
(proof_ne :: proofs_ideal @ proofs_cone) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1572 |
in writeln "Translating proof certificate to HOL"; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1573 |
translator (eqs,les,lts) proof |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1574 |
end)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1575 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1576 |
in mainf end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1577 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1578 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1579 |
fun C f x y = f y x; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1580 |
(* FIXME : This is very bad!!!*) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1581 |
fun subst_conv eqs t = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1582 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1583 |
val t' = fold (Thm.cabs o Thm.lhs_of) eqs t |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1584 |
in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t')) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1585 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1586 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1587 |
(* A wrapper that tries to substitute away variables first. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1588 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1589 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1590 |
open Thm Conv RealArith |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1591 |
fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1592 |
val concl = dest_arg o cprop_of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1593 |
val shuffle1 = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1594 |
fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) }) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1595 |
val shuffle2 = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1596 |
fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps)}) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1597 |
fun substitutable_monomial fvs tm = case term_of tm of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1598 |
Free(_,@{typ real}) => if not (member (op aconvc) fvs tm) then (Rat.one,tm) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1599 |
else error "substitutable_monomial" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1600 |
| @{term "op * :: real => _"}$c$(t as Free _ ) => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1601 |
if is_ratconst (dest_arg1 tm) andalso not (member (op aconvc) fvs (dest_arg tm)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1602 |
then (dest_ratconst (dest_arg1 tm),dest_arg tm) else error "substitutable_monomial" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1603 |
| @{term "op + :: real => _"}$s$t => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1604 |
(substitutable_monomial (add_cterm_frees (dest_arg tm) fvs) (dest_arg1 tm) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1605 |
handle ERROR _ => substitutable_monomial (add_cterm_frees (dest_arg1 tm) fvs) (dest_arg tm)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1606 |
| _ => error "substitutable_monomial" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1607 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1608 |
fun isolate_variable v th = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1609 |
let val w = dest_arg1 (cprop_of th) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1610 |
in if v aconvc w then th |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1611 |
else case term_of w of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1612 |
@{term "op + :: real => _"}$s$t => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1613 |
if dest_arg1 w aconvc v then shuffle2 th |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1614 |
else isolate_variable v (shuffle1 th) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1615 |
| _ => error "isolate variable : This should not happen?" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1616 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1617 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1618 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1619 |
fun real_nonlinear_subst_prover prover ctxt = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1620 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1621 |
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1622 |
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1623 |
simple_cterm_ord |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1624 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1625 |
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1626 |
real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1627 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1628 |
fun make_substitution th = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1629 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1630 |
val (c,v) = substitutable_monomial [] (dest_arg1(concl th)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1631 |
val th1 = Drule.arg_cong_rule (capply @{cterm "op * :: real => _"} (cterm_of_rat (Rat.inv c))) (mk_meta_eq th) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1632 |
val th2 = fconv_rule (binop_conv real_poly_mul_conv) th1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1633 |
in fconv_rule (arg_conv real_poly_conv) (isolate_variable v th2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1634 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1635 |
fun oprconv cv ct = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1636 |
let val g = Thm.dest_fun2 ct |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1637 |
in if g aconvc @{cterm "op <= :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1638 |
orelse g aconvc @{cterm "op < :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1639 |
then arg_conv cv ct else arg1_conv cv ct |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1640 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1641 |
fun mainf translator = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1642 |
let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1643 |
fun substfirst(eqs,les,lts) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1644 |
((let |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1645 |
val eth = tryfind make_substitution eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1646 |
val modify = fconv_rule (arg_conv (oprconv(subst_conv [eth] then_conv real_poly_conv))) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1647 |
in substfirst |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1648 |
(filter_out (fn t => (Thm.dest_arg1 o Thm.dest_arg o cprop_of) t |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1649 |
aconvc @{cterm "0::real"}) (map modify eqs), |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1650 |
map modify les,map modify lts) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1651 |
end) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1652 |
handle ERROR _ => real_nonlinear_prover prover ctxt translator (rev eqs, rev les, rev lts)) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1653 |
in substfirst |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1654 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1655 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1656 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1657 |
in mainf |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1658 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1659 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1660 |
(* Overall function. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1661 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1662 |
fun real_sos prover ctxt t = gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) t; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1663 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
1664 |
|
31131 | 1665 |
(* A tactic *) |
1666 |
fun strip_all ct = |
|
1667 |
case term_of ct of |
|
1668 |
Const("all",_) $ Abs (xn,xT,p) => |
|
1669 |
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct |
|
1670 |
in apfst (cons v) (strip_all t') |
|
1671 |
end |
|
1672 |
| _ => ([],ct) |
|
1673 |
||
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1674 |
fun core_sos_conv prover ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos prover ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI}) |
31512 | 1675 |
|
1676 |
val known_sos_constants = |
|
1677 |
[@{term "op ==>"}, @{term "Trueprop"}, |
|
1678 |
@{term "op -->"}, @{term "op &"}, @{term "op |"}, |
|
1679 |
@{term "Not"}, @{term "op = :: bool => _"}, |
|
1680 |
@{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, |
|
1681 |
@{term "op = :: real => _"}, @{term "op < :: real => _"}, |
|
1682 |
@{term "op <= :: real => _"}, |
|
1683 |
@{term "op + :: real => _"}, @{term "op - :: real => _"}, |
|
1684 |
@{term "op * :: real => _"}, @{term "uminus :: real => _"}, |
|
1685 |
@{term "op / :: real => _"}, @{term "inverse :: real => _"}, |
|
1686 |
@{term "op ^ :: real => _"}, @{term "abs :: real => _"}, |
|
1687 |
@{term "min :: real => _"}, @{term "max :: real => _"}, |
|
1688 |
@{term "0::real"}, @{term "1::real"}, @{term "number_of :: int => real"}, |
|
1689 |
@{term "number_of :: int => nat"}, |
|
1690 |
@{term "Int.Bit0"}, @{term "Int.Bit1"}, |
|
1691 |
@{term "Int.Pls"}, @{term "Int.Min"}]; |
|
1692 |
||
1693 |
fun check_sos kcts ct = |
|
1694 |
let |
|
1695 |
val t = term_of ct |
|
1696 |
val _ = if not (null (Term.add_tfrees t []) |
|
1697 |
andalso null (Term.add_tvars t [])) |
|
1698 |
then error "SOS: not sos. Additional type varables" else () |
|
1699 |
val fs = Term.add_frees t [] |
|
1700 |
val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs |
|
1701 |
then error "SOS: not sos. Variables with type not real" else () |
|
1702 |
val vs = Term.add_vars t [] |
|
1703 |
val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs |
|
1704 |
then error "SOS: not sos. Variables with type not real" else () |
|
1705 |
val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t []) |
|
1706 |
val _ = if null ukcs then () |
|
1707 |
else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs)) |
|
1708 |
in () end |
|
1709 |
||
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1710 |
fun core_sos_tac prover ctxt = CSUBGOAL (fn (ct, i) => |
31512 | 1711 |
let val _ = check_sos known_sos_constants ct |
1712 |
val (avs, p) = strip_all ct |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1713 |
val th = standard (fold_rev forall_intr avs (real_sos prover ctxt (Thm.dest_arg p))) |
31131 | 1714 |
in rtac th i end); |
1715 |
||
1716 |
fun default_SOME f NONE v = SOME v |
|
1717 |
| default_SOME f (SOME v) _ = SOME v; |
|
1718 |
||
1719 |
fun lift_SOME f NONE a = f a |
|
1720 |
| lift_SOME f (SOME a) _ = SOME a; |
|
1721 |
||
1722 |
||
1723 |
local |
|
1724 |
val is_numeral = can (HOLogic.dest_number o term_of) |
|
1725 |
in |
|
1726 |
fun get_denom b ct = case term_of ct of |
|
1727 |
@{term "op / :: real => _"} $ _ $ _ => |
|
1728 |
if is_numeral (Thm.dest_arg ct) then get_denom b (Thm.dest_arg1 ct) |
|
1729 |
else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b) |
|
1730 |
| @{term "op < :: real => _"} $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct) |
|
1731 |
| @{term "op <= :: real => _"} $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct) |
|
1732 |
| _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct) |
|
1733 |
| _ => NONE |
|
1734 |
end; |
|
1735 |
||
1736 |
fun elim_one_denom_tac ctxt = |
|
1737 |
CSUBGOAL (fn (P,i) => |
|
1738 |
case get_denom false P of |
|
1739 |
NONE => no_tac |
|
1740 |
| SOME (d,ord) => |
|
1741 |
let |
|
32150 | 1742 |
val ss = simpset_of ctxt addsimps @{thms field_simps} |
31131 | 1743 |
addsimps [@{thm nonzero_power_divide}, @{thm power_divide}] |
1744 |
val th = instantiate' [] [SOME d, SOME (Thm.dest_arg P)] |
|
1745 |
(if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto} |
|
1746 |
else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast}) |
|
1747 |
in (rtac th i THEN Simplifier.asm_full_simp_tac ss i) end); |
|
1748 |
||
1749 |
fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i); |
|
1750 |
||
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
1751 |
fun sos_tac prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac prover ctxt |
31131 | 1752 |
|
1753 |
||
31512 | 1754 |
end; |