1 (* Title: Library/Sum_Of_Squares |
1 (* Title: Library/Sum_Of_Squares |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 |
3 |
4 In order to use the method sos, call it with (sos remote_csdp) to use the remote solver |
4 In order to use the method sos, call it with (sos remote_csdp) to use the remote solver |
5 or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path, |
5 or install CSDP (https://projects.coin-or.org/Csdp/), set the Isabelle environment |
6 and call it with (sos csdp). By default, sos calls remote_csdp. This can take of the order |
6 variable CSDP_EXE and call it with (sos csdp). By default, sos calls remote_csdp. |
7 of a minute for one sos call, because sos calls CSDP repeatedly. |
7 This can take of the order of a minute for one sos call, because sos calls CSDP repeatedly. |
8 If you install CSDP locally, sos calls typically takes only a few seconds. |
8 If you install CSDP locally, sos calls typically takes only a few seconds. |
9 |
9 |
10 *) |
10 *) |
11 |
11 |
12 header {* A decision method for universal multivariate real arithmetic with addition, |
12 header {* A decision method for universal multivariate real arithmetic with addition, |
13 multiplication and ordering using semidefinite programming*} |
13 multiplication and ordering using semidefinite programming*} |
14 |
14 |
15 theory Sum_Of_Squares |
15 theory Sum_Of_Squares |
16 imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *) |
16 imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *) |
17 uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML" |
17 uses |
18 begin |
18 ("positivstellensatz.ML") |
|
19 ("Sum_Of_Squares/sum_of_squares.ML") |
|
20 ("Sum_Of_Squares/sos_wrapper.ML") |
|
21 begin |
19 |
22 |
20 (* setup sos tactic *) |
23 (* setup sos tactic *) |
|
24 |
|
25 use "positivstellensatz.ML" |
|
26 use "Sum_Of_Squares/sum_of_squares.ML" |
|
27 use "Sum_Of_Squares/sos_wrapper.ML" |
|
28 |
21 setup SosWrapper.setup |
29 setup SosWrapper.setup |
22 |
30 |
23 text{* Tests -- commented since they work only when csdp is installed or take too long with remote csdps *} |
31 text{* Tests -- commented since they work only when csdp is installed or take too long with remote csdps *} |
24 |
32 |
25 (* |
33 (* |