1

(* Example of a use of Z3 Fixedpoint that doesn't work

2

The file is selfcontained and shall be compiled as follow:

3


4

in File _tags, add the simple line

5

<**/*>: package(z3)

6


7

Then compile as

8

ocamlbuild useocamlfind zustre_test.native

9


10

We obtain the following output:

11

$ ./zustre_test.native

12

Registered rules:

13

Rule: (forall ((x Int) (y Int)) (=> (= x y) (f x y)))

14

Rule: INIT_STATE

15

Rule: (forall ((x Int) (y Int)) (=> (and (f x y) INIT_STATE) (MAIN x y)))

16

Rule: (forall ((x Int) (y Int)) (=> (and (not (= x y)) (MAIN x y)) ERR))

17


18

Fatal error: exception Z3.Error("Uninterpreted 'y' in <null>:

19

f(#0,#1) :

20

(= (:var 1) y),

21

(= (:var 0) x),

22

(= x y).

23

")

24


25

*)

26


27


28


29

let rec fprintf_list ~sep:sep f fmt = function

30

 [] > ()

31

 [e] > f fmt e

32

 x::r > Format.fprintf fmt "%a%(%)%a" f x sep (fprintf_list ~sep f) r

33


34

(* Global references to declare Z3 context and Fixedpoint engine *)

35


36

let ctx = ref (Z3.mk_context [])

37

let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)

38


39

(* Shortcuts to basic sorts *)

40


41

let bool_sort = Z3.Boolean.mk_sort !ctx

42

let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx

43

let real_sort = Z3.Arithmetic.Real.mk_sort !ctx

44


45


46

let _ =

47


48


49

(* Setting up the fixed point engine *)

50

fp := Z3.Fixedpoint.mk_fixedpoint !ctx;

51

let module P = Z3.Params in

52

let module S = Z3.Symbol in

53

let mks = S.mk_string !ctx in

54

let params = P.mk_params !ctx in

55

P.add_symbol params (mks "engine") (mks "spacer");

56

Z3.Fixedpoint.set_parameters !fp params;

57


58

(* Three rules

59

R1: (x = y) => f(x,y)

60

R2: INIT and f(x,y) => MAIN(x,y)

61

R3: x!=y and MAIN(x,y) => ERR(x,y)

62

INIT is assumed as the beginning

63


64

Querying ERR shall be unsat since the only valid MAIN(x,y) are x=y and

65

therefore ERR is unsat.

66

*)

67


68

(* Simple rule : forall x, y, (x=y => f(x,y)) *)

69

let x = Z3.FuncDecl.mk_func_decl_s !ctx "x" [] int_sort in

70

let y = Z3.FuncDecl.mk_func_decl_s !ctx "y" [] int_sort in

71

let x_expr = Z3.Expr.mk_const_f !ctx x in

72

let y_expr = Z3.Expr.mk_const_f !ctx y in

73


74

let decl_f = Z3.FuncDecl.mk_func_decl_s !ctx "f" [int_sort; int_sort] bool_sort in

75

Z3.Fixedpoint.register_relation !fp decl_f; (* since f appears in the rhs of a rule *)

76

let f_x_y_expr = Z3.Expr.mk_app !ctx decl_f [x_expr; y_expr] in

77

let x_eq_y_expr = Z3.Boolean.mk_eq !ctx x_expr y_expr in

78


79

let expr_f_lhs = (* x = y *)

80

x_eq_y_expr

81

in

82

let expr_f_rhs = f_x_y_expr in

83

let expr_f = Z3.Boolean.mk_implies !ctx expr_f_lhs expr_f_rhs in

84

(* Adding forall as prefix *)

85

let expr_forall_f = Z3.Quantifier.mk_forall_const

86

!ctx (* context *)

87

(* [int_sort; int_sort] (\* sort list*\) *)

88

(* [Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (\* symbol list *\) *)

89

(* [x_expr; y_expr] Second try with expr list "const" *)

90

[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]

91

expr_f (* expression *)

92

None (* quantifier weight, None means 1 *)

93

[] (* pattern list ? *)

94

[] (* ? *)

95

None (* ? *)

96

None (* ? *)

97

in

98

let expr_forall_f = Z3.Quantifier.expr_of_quantifier expr_forall_f in

99

Z3.Fixedpoint.add_rule !fp expr_forall_f None;

100


101


102

(* INIT RULE *)

103

let decl_init = Z3.FuncDecl.mk_func_decl_s !ctx "INIT_STATE" [] bool_sort in

104

Z3.Fixedpoint.register_relation !fp decl_init;

105

let init_expr = Z3.Expr.mk_app !ctx decl_init [] in

106

Z3.Fixedpoint.add_rule !fp init_expr None;

107


108

(* MAIN is defined by two rules : INIT and induction *)

109

let decl_main = Z3.FuncDecl.mk_func_decl_s !ctx "MAIN" [int_sort; int_sort] bool_sort in

110

Z3.Fixedpoint.register_relation !fp decl_main;

111

let main_x_y_expr = Z3.Expr.mk_app !ctx decl_main [x_expr; y_expr] in

112


113

(* Rule 1: forall x, y, INIT_STATE and f(x,y) => MAIN(x,y) : at the beginning x=y *)

114

let expr_main1_lhs = (* INIT_STATE and f(x, y) *)

115

Z3.Boolean.mk_and !ctx [f_x_y_expr; init_expr] in

116

let expr_main1_rhs = main_x_y_expr in

117

let expr_main1 = Z3.Boolean.mk_implies !ctx expr_main1_lhs expr_main1_rhs in

118

(* Adding forall as prefix *)

119

let expr_forall_main1 = Z3.Quantifier.mk_forall_const

120

!ctx (* context *)

121

(*

122

[int_sort; int_sort] (* sort list*)

123

[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)

124

*)

125

(* [x_expr; y_expr] Second try with expr list "const" *)

126

[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]

127

expr_main1 (* expression *)

128

None (* quantifier weight, None means 1 *)

129

[] (* pattern list ? *)

130

[] (* ? *)

131

None (* ? *)

132

None (* ? *)

133

in

134

let expr_forall_main1 = Z3.Quantifier.expr_of_quantifier expr_forall_main1 in

135

Z3.Fixedpoint.add_rule !fp expr_forall_main1 None;

136


137

(* Rule 2: forall x,y, MAIN(x,y) => MAIN(x+1, y+1) *)

138

let expr_main2_lhs = main_x_y_expr in

139

let plus_one x = Z3.Arithmetic.mk_add !ctx

140

[

141

x;

142

(* Z3.Arithmetic.Integer.mk_const_s !ctx "1" *)

143

Z3.Expr.mk_numeral_int !ctx 1 int_sort

144

] in

145

let main_x_y_plus_one_expr = Z3.Expr.mk_app !ctx decl_main [plus_one x_expr; plus_one y_expr] in

146

let expr_main2_rhs = main_x_y_plus_one_expr in

147

let expr_main2 = Z3.Boolean.mk_implies !ctx expr_main2_lhs expr_main2_rhs in

148

(* Adding forall as prefix *)

149

let expr_forall_main2 = Z3.Quantifier.mk_forall_const

150

!ctx (* context *)

151

(*

152

[int_sort; int_sort] (* sort list*)

153

[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)

154

*)

155

(* [x_expr; y_expr] Second try with expr list "const" *)

156

[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]

157

expr_main2 (* expression *)

158

None (* quantifier weight, None means 1 *)

159

[] (* pattern list ? *)

160

[] (* ? *)

161

None (* ? *)

162

None (* ? *)

163

in

164

let expr_forall_main2 = Z3.Quantifier.expr_of_quantifier expr_forall_main2 in

165

Z3.Fixedpoint.add_rule !fp expr_forall_main2 None;

166


167


168


169

(* TODO: not implemented yet since the error is visible without it *)

170


171

(* Query: is it possible to have MAIN(x,y) and x!=y ? *)

172

(* This is performed as follow:

173

rule (forall x, y, MAIN(x,y) and x!=y => ERR)

174

*)

175

let decl_err = Z3.FuncDecl.mk_func_decl_s !ctx "ERR" [] bool_sort in

176

Z3.Fixedpoint.register_relation !fp decl_err;

177

let err_expr = Z3.Expr.mk_app !ctx decl_err [] in

178

let x_diff_y_expr = Z3.Boolean.mk_not !ctx x_eq_y_expr in

179

let expr_err_lhs =

180

Z3.Boolean.mk_and !ctx [x_diff_y_expr; main_x_y_expr] in

181

let expr_err_rhs = err_expr in

182

let expr_err = Z3.Boolean.mk_implies !ctx expr_err_lhs expr_err_rhs in

183

(* Adding forall as prefix *)

184

let expr_forall_err = Z3.Quantifier.mk_forall_const

185

!ctx (* context *)

186

(* [int_sort; int_sort] (* sort list*)

187

[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)

188

*)

189

(* [x_expr; y_expr] Second try with expr list "const" *)

190

[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]

191

expr_err (* expression *)

192

None (* quantifier weight, None means 1 *)

193

[] (* pattern list ? *)

194

[] (* ? *)

195

None (* ? *)

196

None (* ? *)

197

in

198

let expr_forall_err = Z3.Quantifier.expr_of_quantifier expr_forall_err in

199

Z3.Fixedpoint.add_rule !fp expr_forall_err None;

200


201

(* Printing the rules for sanity check *)

202


203

let rules_expr = Z3.Fixedpoint.get_rules !fp in

204

Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."

205

(fprintf_list ~sep:"@ "

206

(fun fmt e >

207

(* let e2 = Z3.Quantifier.get_body eq in *)

208

(* let fd = Z3.Expr.get_func_decl e in *)

209

Format.fprintf fmt "Rule: %s@ "

210

(Z3.Expr.to_string e);

211

)) rules_expr;

212


213


214

let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in

215


216

Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)

217


218


219


220


221

