1(* 2 Copyright (C) 2012 Microsoft Corporation 3 Author: CM Wintersteiger (cwinter) 2012-12-17 4*) 5 6open Z3 7open Z3.Symbol 8open Z3.Sort 9open Z3.Expr 10open Z3.Boolean 11open Z3.FuncDecl 12open Z3.Goal 13open Z3.Tactic 14open Z3.Tactic.ApplyResult 15open Z3.Probe 16open Z3.Solver 17open Z3.Arithmetic 18open Z3.Arithmetic.Integer 19open Z3.Arithmetic.Real 20open Z3.BitVector 21 22 23exception TestFailedException of string 24 25(** 26 Model Converter test 27*) 28let model_converter_test ( ctx : context ) = 29 Printf.printf "ModelConverterTest\n"; 30 let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in 31 let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in 32 let g4 = (mk_goal ctx true false false ) in 33 (Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ; 34 (Goal.add g4 [ (mk_eq ctx 35 yr 36 (Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ; 37 (Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ; 38 ( 39 let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in 40 if ((get_num_subgoals ar) == 1 && 41 ((is_decided_sat (get_subgoal ar 0)) || 42 (is_decided_unsat (get_subgoal ar 0)))) then 43 raise (TestFailedException "") 44 else 45 Printf.printf "Test passed.\n" 46 ); 47 ( 48 let ar = (Tactic.apply (and_then ctx (mk_tactic ctx ("simplify")) (mk_tactic ctx "solve-eqs") []) g4 None) in 49 if ((get_num_subgoals ar) == 1 && 50 ((is_decided_sat (get_subgoal ar 0)) || 51 (is_decided_unsat (get_subgoal ar 0)))) then 52 raise (TestFailedException "") 53 else 54 Printf.printf "Test passed.\n" 55 ; 56 let solver = (mk_solver ctx None) in 57 let f e = (Solver.add solver [ e ]) in 58 ignore (List.map f (get_formulas (get_subgoal ar 0))) ; 59 let q = (check solver []) in 60 if q != SATISFIABLE then 61 raise (TestFailedException "") 62 else 63 let m = (get_model solver) in 64 match m with 65 | None -> raise (TestFailedException "") 66 | Some (m) -> 67 Printf.printf "Solver says: %s\n" (string_of_status q) ; 68 Printf.printf "Model: \n%s\n" (Model.to_string m) 69 ) 70 71(** 72 Some basic tests. 73*) 74let basic_tests ( ctx : context ) = 75 Printf.printf "BasicTests\n" ; 76 let fname = (mk_string ctx "f") in 77 let x = (mk_string ctx "x") in 78 let y = (mk_string ctx "y") in 79 let bs = (Boolean.mk_sort ctx) in 80 let domain = [ bs; bs ] in 81 let f = (FuncDecl.mk_func_decl ctx fname domain bs) in 82 let fapp = (mk_app ctx f 83 [ (Expr.mk_const ctx x bs); (Expr.mk_const ctx y bs) ]) in 84 let fargs2 = [ (mk_fresh_const ctx "cp" bs) ] in 85 let domain2 = [ bs ] in 86 let fapp2 = (mk_app ctx (mk_fresh_func_decl ctx "fp" domain2 bs) fargs2) in 87 let trivial_eq = (mk_eq ctx fapp fapp) in 88 let nontrivial_eq = (mk_eq ctx fapp fapp2) in 89 let g = (mk_goal ctx true false false) in 90 (Goal.add g [ trivial_eq ]) ; 91 (Goal.add g [ nontrivial_eq ]) ; 92 Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ; 93 ( 94 let solver = (mk_solver ctx None) in 95 (List.iter (fun a -> (Solver.add solver [ a ])) (get_formulas g)) ; 96 if (check solver []) != SATISFIABLE then 97 raise (TestFailedException "") 98 else 99 Printf.printf "Test passed.\n" 100 ); 101 ( 102 let ar = (Tactic.apply (mk_tactic ctx "simplify") g None) in 103 if ((get_num_subgoals ar) == 1 && 104 ((is_decided_sat (get_subgoal ar 0)) || 105 (is_decided_unsat (get_subgoal ar 0)))) then 106 raise (TestFailedException "") 107 else 108 Printf.printf "Test passed.\n" 109 ); 110 ( 111 let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in 112 if ((get_num_subgoals ar) == 1 && 113 (not (is_decided_sat (get_subgoal ar 0)))) then 114 raise (TestFailedException "") 115 else 116 Printf.printf "Test passed.\n" 117 ); 118 (Goal.add g [ (mk_eq ctx 119 (mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32)) 120 (mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] ) 121 ; 122 ( 123 let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in 124 if ((get_num_subgoals ar) == 1 && 125 (not (is_decided_unsat (get_subgoal ar 0)))) then 126 raise (TestFailedException "") 127 else 128 Printf.printf "Test passed.\n" 129 ); 130 ( 131 let g2 = (mk_goal ctx true true false) in 132 let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in 133 if ((get_num_subgoals ar) == 1 && 134 (not (is_decided_sat (get_subgoal ar 0)))) then 135 raise (TestFailedException "") 136 else 137 Printf.printf "Test passed.\n" 138 ); 139 ( 140 let g2 = (mk_goal ctx true true false) in 141 (Goal.add g2 [ (Boolean.mk_false ctx) ]) ; 142 let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in 143 if ((get_num_subgoals ar) == 1 && 144 (not (is_decided_unsat (get_subgoal ar 0)))) then 145 raise (TestFailedException "") 146 else 147 Printf.printf "Test passed.\n" 148 ); 149 ( 150 let g3 = (mk_goal ctx true true false) in 151 let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in 152 let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in 153 (Goal.add g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ; 154 (Goal.add g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ; 155 let constr = (mk_eq ctx xc yc) in 156 (Goal.add g3 [ constr ] ) ; 157 let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in 158 if ((get_num_subgoals ar) == 1 && 159 (not (is_decided_unsat (get_subgoal ar 0)))) then 160 raise (TestFailedException "") 161 else 162 Printf.printf "Test passed.\n" 163 ) ; 164 model_converter_test ctx ; 165 (* Real num/den test. *) 166 let rn = Real.mk_numeral_nd ctx 42 43 in 167 let inum = (get_numerator rn) in 168 let iden = get_denominator rn in 169 Printf.printf "Numerator: %s Denominator: %s\n" (Real.numeral_to_string inum) (Real.numeral_to_string iden) ; 170 if ((Real.numeral_to_string inum) <> "42" || (Real.numeral_to_string iden) <> "43") then 171 raise (TestFailedException "") 172 else 173 Printf.printf "Test passed.\n" 174 ; 175 if ((to_decimal_string rn 3) <> "0.976?") then 176 raise (TestFailedException "") 177 else 178 Printf.printf "Test passed.\n" 179 ; 180 if (to_decimal_string (Real.mk_numeral_s ctx "-1231231232/234234333") 5 <> "-5.25640?") then 181 raise (TestFailedException "") 182 else if (to_decimal_string (Real.mk_numeral_s ctx "-123123234234234234231232/234234333") 5 <> "-525641278361333.28170?") then 183 raise (TestFailedException "") 184 else if (to_decimal_string (Real.mk_numeral_s ctx "-234234333") 5 <> "-234234333") then 185 raise (TestFailedException "") 186 else if (to_decimal_string (Real.mk_numeral_s ctx "234234333/2") 5 <> "117117166.5") then 187 raise (TestFailedException "") 188 ; 189 (* Error handling test. *) 190 try ( 191 let i = Integer.mk_numeral_s ctx "1/2" in 192 Printf.printf "%s\n" (Expr.to_string i) ; 193 raise (TestFailedException "check") 194 ) 195 with Z3.Error(_) -> ( 196 Printf.printf "Exception caught, OK.\n" 197 ) 198 199(** 200 A basic example of how to use quantifiers. 201**) 202let quantifier_example1 ( ctx : context ) = 203 Printf.printf "QuantifierExample\n" ; 204 let is = (Integer.mk_sort ctx) in 205 let types = [ is; is; is ] in 206 let names = [ (Symbol.mk_string ctx "x_0"); 207 (Symbol.mk_string ctx "x_1"); 208 (Symbol.mk_string ctx "x_2") ] in 209 let vars = [ (Quantifier.mk_bound ctx 2 (List.nth types 0)); 210 (Quantifier.mk_bound ctx 2 (List.nth types 1)); 211 (Quantifier.mk_bound ctx 2 (List.nth types 2)) ] in 212 let xs = [ (Integer.mk_const ctx (List.nth names 0)); 213 (Integer.mk_const ctx (List.nth names 1)); 214 (Integer.mk_const ctx (List.nth names 2)) ] in 215 216 let body_vars = (Boolean.mk_and ctx 217 [ (mk_eq ctx 218 (Arithmetic.mk_add ctx [ (List.nth vars 0) ; (Integer.mk_numeral_i ctx 1)]) 219 (Integer.mk_numeral_i ctx 2)) ; 220 (mk_eq ctx 221 (Arithmetic.mk_add ctx [ (List.nth vars 1); (Integer.mk_numeral_i ctx 2)]) 222 (Arithmetic.mk_add ctx [ (List.nth vars 2); (Integer.mk_numeral_i ctx 3)])) ]) in 223 let body_const = (Boolean.mk_and ctx 224 [ (mk_eq ctx 225 (Arithmetic.mk_add ctx [ (List.nth xs 0); (Integer.mk_numeral_i ctx 1)]) 226 (Integer.mk_numeral_i ctx 2)) ; 227 (mk_eq ctx 228 (Arithmetic.mk_add ctx [ (List.nth xs 1); (Integer.mk_numeral_i ctx 2)]) 229 (Arithmetic.mk_add ctx [ (List.nth xs 2); (Integer.mk_numeral_i ctx 3)])) ]) in 230 231 let x = (Quantifier.mk_forall ctx types names body_vars (Some 1) [] [] (Some (Symbol.mk_string ctx "Q1")) (Some (Symbol.mk_string ctx "skid1"))) in 232 Printf.printf "Quantifier X: %s\n" (Quantifier.to_string x) ; 233 let y = (Quantifier.mk_forall_const ctx xs body_const (Some 1) [] [] (Some (Symbol.mk_string ctx "Q2")) (Some (Symbol.mk_string ctx "skid2"))) in 234 Printf.printf "Quantifier Y: %s\n" (Quantifier.to_string y) ; 235 if (is_true (Quantifier.expr_of_quantifier x)) then 236 raise (TestFailedException "") (* unreachable *) 237 else if (is_false (Quantifier.expr_of_quantifier x)) then 238 raise (TestFailedException "") (* unreachable *) 239 else if (is_const (Quantifier.expr_of_quantifier x)) then 240 raise (TestFailedException "") (* unreachable *) 241 242 243open Z3.FloatingPoint 244 245(** 246 A basic example of floating point arithmetic 247**) 248let fpa_example ( ctx : context ) = 249 Printf.printf "FPAExample\n" ; 250 (* let str = ref "" in *) 251 (* (read_line ()) ; *) 252 let double_sort = (FloatingPoint.mk_sort_double ctx) in 253 let rm_sort = (FloatingPoint.RoundingMode.mk_sort ctx) in 254 255 (** Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode). *) 256 let s_rm = (mk_string ctx "rm") in 257 let rm = (mk_const ctx s_rm rm_sort) in 258 let s_x = (mk_string ctx "x") in 259 let s_y = (mk_string ctx "y") in 260 let x = (mk_const ctx s_x double_sort) in 261 let y = (mk_const ctx s_y double_sort)in 262 let n = (FloatingPoint.mk_numeral_f ctx 42.0 double_sort) in 263 let s_x_plus_y = (mk_string ctx "x_plus_y") in 264 let x_plus_y = (mk_const ctx s_x_plus_y double_sort) in 265 let c1 = (mk_eq ctx x_plus_y (mk_add ctx rm x y)) in 266 let args = [ c1 ; (mk_eq ctx x_plus_y n) ] in 267 let c2 = (Boolean.mk_and ctx args) in 268 let args2 = [ c2 ; (Boolean.mk_not ctx (Boolean.mk_eq ctx rm (RoundingMode.mk_rtz ctx))) ] in 269 let c3 = (Boolean.mk_and ctx args2) in 270 let and_args = [ (Boolean.mk_not ctx (mk_is_zero ctx y)) ; 271 (Boolean.mk_not ctx (mk_is_nan ctx y)) ; 272 (Boolean.mk_not ctx (mk_is_infinite ctx y)) ] in 273 let args3 = [ c3 ; (Boolean.mk_and ctx and_args) ] in 274 let c4 = (Boolean.mk_and ctx args3) in 275 (Printf.printf "c4: %s\n" (Expr.to_string c4)) ; 276 ( 277 let solver = (mk_solver ctx None) in 278 (Solver.add solver [ c4 ]) ; 279 if (check solver []) != SATISFIABLE then 280 raise (TestFailedException "") 281 else 282 Printf.printf "Test passed.\n" 283 ); 284 285 (* Show that the following are equal: *) 286 (* (fp #b0 #b10000000001 #xc000000000000) *) 287 (* ((_ to_fp 11 53) #x401c000000000000)) *) 288 (* ((_ to_fp 11 53) RTZ 1.75 2))) *) 289 (* ((_ to_fp 11 53) RTZ 7.0))) *) 290 let c1 = (mk_fp ctx (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) 291 (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11)) 292 (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))) in 293 let c2 = (mk_to_fp_bv ctx 294 (mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64)) 295 (mk_sort ctx 11 53)) in 296 let c3 = (mk_to_fp_int_real ctx 297 (RoundingMode.mk_rtz ctx) 298 (mk_numeral_string ctx "2" (Integer.mk_sort ctx)) 299 (mk_numeral_string ctx "1.75" (Real.mk_sort ctx)) 300 (FloatingPoint.mk_sort ctx 11 53)) in 301 let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx) 302 (mk_numeral_string ctx "7.0" (Real.mk_sort ctx)) 303 (FloatingPoint.mk_sort ctx 11 53)) in 304 let args3 = [ (mk_eq ctx c1 c2) ; 305 (mk_eq ctx c1 c3) ; 306 (mk_eq ctx c1 c4) ] in 307 let c5 = (Boolean.mk_and ctx args3) in 308 (Printf.printf "c5: %s\n" (Expr.to_string c5)) ; 309 ( 310 let solver = (mk_solver ctx None) in 311 (Solver.add solver [ c5 ]) ; 312 if (check solver []) != SATISFIABLE then 313 raise (TestFailedException "") 314 else 315 Printf.printf "Test passed.\n" 316 ) 317 318let _ = 319 try ( 320 if not (Log.open_ "z3.log") then 321 raise (TestFailedException "Log couldn't be opened.") 322 else 323 ( 324 Printf.printf "Running Z3 version %s\n" Version.to_string ; 325 Printf.printf "Z3 full version string: %s\n" Version.full_version ; 326 let cfg = [("model", "true"); ("proof", "false")] in 327 let ctx = (mk_context cfg) in 328 let is = (Symbol.mk_int ctx 42) in 329 let ss = (Symbol.mk_string ctx "mySymbol") in 330 let bs = (Boolean.mk_sort ctx) in 331 let ints = (Integer.mk_sort ctx) in 332 let rs = (Real.mk_sort ctx) in 333 let v = (Arithmetic.Integer.mk_numeral_i ctx 8000000000) in 334 Printf.printf "int symbol: %s\n" (Symbol.to_string is); 335 Printf.printf "string symbol: %s\n" (Symbol.to_string ss); 336 Printf.printf "bool sort: %s\n" (Sort.to_string bs); 337 Printf.printf "int sort: %s\n" (Sort.to_string ints); 338 Printf.printf "real sort: %s\n" (Sort.to_string rs); 339 Printf.printf "integer: %s\n" (Expr.to_string v); 340 basic_tests ctx ; 341 quantifier_example1 ctx ; 342 fpa_example ctx ; 343 Printf.printf "Disposing...\n"; 344 Gc.full_major () 345 ); 346 Printf.printf "Exiting.\n" ; 347 exit 0 348 ) with Error(msg) -> ( 349 Printf.printf "Z3 EXCEPTION: %s\n" msg ; 350 exit 1 351 ) 352;; 353