4 Setup SMT solvers. |
4 Setup SMT solvers. |
5 *) |
5 *) |
6 |
6 |
7 signature SMT_SETUP_SOLVERS = |
7 signature SMT_SETUP_SOLVERS = |
8 sig |
8 sig |
9 val z3_non_commercial: unit -> bool |
9 datatype z3_non_commercial = |
|
10 Z3_Non_Commercial_Unknown | |
|
11 Z3_Non_Commercial_Accepted | |
|
12 Z3_Non_Commercial_Declined |
|
13 val z3_non_commercial: unit -> z3_non_commercial |
10 val setup: theory -> theory |
14 val setup: theory -> theory |
11 end |
15 end |
12 |
16 |
13 structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS = |
17 structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS = |
14 struct |
18 struct |
94 reconstruct = NONE } |
98 reconstruct = NONE } |
95 |
99 |
96 |
100 |
97 (* Z3 *) |
101 (* Z3 *) |
98 |
102 |
|
103 datatype z3_non_commercial = |
|
104 Z3_Non_Commercial_Unknown | |
|
105 Z3_Non_Commercial_Accepted | |
|
106 Z3_Non_Commercial_Declined |
|
107 |
|
108 |
99 local |
109 local |
100 val flagN = "Z3_NON_COMMERCIAL" |
110 val flagN = "Z3_NON_COMMERCIAL" |
|
111 |
|
112 val accepted = member (op =) ["yes", "Yes", "YES"] |
|
113 val declined = member (op =) ["no", "No", "NO"] |
101 in |
114 in |
102 |
115 |
103 fun z3_non_commercial () = (getenv flagN = "yes") |
116 fun z3_non_commercial () = |
|
117 if accepted (getenv flagN) then Z3_Non_Commercial_Accepted |
|
118 else if declined (getenv flagN) then Z3_Non_Commercial_Declined |
|
119 else Z3_Non_Commercial_Unknown |
104 |
120 |
105 fun if_z3_non_commercial f = |
121 fun if_z3_non_commercial f = |
106 if z3_non_commercial () then f () |
122 (case z3_non_commercial () of |
107 else |
123 Z3_Non_Commercial_Accepted => f () |
108 error ("The SMT solver Z3 is not enabled. To enable it, set " ^ |
124 | Z3_Non_Commercial_Declined => |
109 "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^ |
125 error ("The SMT solver Z3 may only be used for non-commercial " ^ |
110 ".") |
126 "applications.") |
|
127 | Z3_Non_Commercial_Unknown => |
|
128 error ("The SMT solver Z3 is not activated. To activate it, set " ^ |
|
129 "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^ |
|
130 ".")) |
111 |
131 |
112 end |
132 end |
113 |
133 |
114 |
134 |
115 local |
135 local |