extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
authorboehmes
Wed May 23 16:03:38 2012 +0200 (2012-05-23)
changeset 479658ba6438557bc
parent 47964 b74655182ed6
child 47969 ce4345b06408
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/z3_interface.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed May 23 15:40:10 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed May 23 16:03:38 2012 +0200
     1.3 @@ -67,8 +67,12 @@
     1.4      if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
     1.5      else NONE
     1.6  
     1.7 +  fun mk_nary _ cu [] = cu
     1.8 +    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
     1.9 +
    1.10    val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
    1.11 -  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
    1.12 +  val add = Thm.cterm_of @{theory} @{const plus (real)}
    1.13 +  val real0 = Numeral.mk_cnumber @{ctyp real} 0
    1.14    val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
    1.15    val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    1.16    val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
    1.17 @@ -76,8 +80,8 @@
    1.18    val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    1.19  
    1.20    fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.21 -    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) [ct, cu] =
    1.22 -        SOME (mk_add ct cu)
    1.23 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts =
    1.24 +        SOME (mk_nary add real0 cts)
    1.25      | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] =
    1.26          SOME (mk_sub ct cu)
    1.27      | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] =
     2.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed May 23 15:40:10 2012 +0200
     2.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed May 23 16:03:38 2012 +0200
     2.3 @@ -184,7 +184,8 @@
     2.4    end
     2.5  
     2.6  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
     2.7 -val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
     2.8 +val add = Thm.cterm_of @{theory} @{const plus (int)}
     2.9 +val int0 = Numeral.mk_cnumber @{ctyp int} 0
    2.10  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
    2.11  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
    2.12  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
    2.13 @@ -211,7 +212,7 @@
    2.14    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
    2.15    | _ =>
    2.16      (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
    2.17 -      (Sym ("+", _), SOME @{typ int}, [ct, cu]) => SOME (mk_add ct cu)
    2.18 +      (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
    2.19      | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
    2.20      | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
    2.21      | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu)