Project

General

Profile

« Previous | Next » 

Revision 4300981b

Added by Pierre-Loïc Garoche over 3 years ago

Zustre: timeout and slicing

View differences:

src/tools/zustre/zustre_verifier.ml
55 55
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
56 56
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
57 57
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
58
        "-timeout", Arg.Set_int timeout, "Set timeout in ms (default 10000 = 10 s)";
58 59
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
60
        "-debug", Arg.Set debug, "Debug mode";
59 61
      ]
60 62
                
61 63
    let activate () = (
......
77 79
       * let solver =Z3.Solver.mk_solver !ctx None in
78 80
       * let help = Z3.Solver.get_help solver in
79 81
       * Format.eprintf "Z3 help : %s@." help; *)
80
      
82

  
81 83
      let module P = Z3.Params in
82 84
      let module S = Z3.Symbol in
83 85
      let mks = S.mk_string !ctx in
84
      let params = P.mk_params !ctx in
86
      
87
      (* Fixpoint Engine parameters *)
88
      
89
      let fp_params = P.mk_params !ctx in
85 90

  
86 91
      (* (\* self.fp.set (engine='spacer') *\) *)
87
      P.add_symbol params (mks "engine") (mks "spacer");
88
      (* P.add_symbol params (mks "engine") (mks "pdr");  *)
92
      P.add_symbol fp_params (mks "engine") (mks "spacer");
93
      (* P.add_symbol fp_params (mks "engine") (mks "pdr");  *)
89 94
      
90 95
       (* #z3.set_option(rational_to_decimal=True) *)
91 96
       (* #self.fp.set('precision',30) *)
92 97
      if !param_stat then 
93 98
        (* self.fp.set('print_statistics',True) *)
94
        P.add_bool params (mks "print_statistics") true;
99
        P.add_bool fp_params (mks "print_statistics") true;
95 100

  
96 101
      (* Dont know where to find this parameter *)
97 102
      (* if !param_spacer_verbose then
......
100 105

  
101 106
      (* The option is not recogined*)
102 107
      (* self.fp.set('use_heavy_mev',True) *)
103
      (* P.add_bool params (mks "use_heavy_mev") true; *)
108
      (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
104 109
      
105 110
      (* self.fp.set('pdr.flexible_trace',True) *)
106
      P.add_bool params (mks "pdr.flexible_trace") true;
111
      P.add_bool fp_params (mks "pdr.flexible_trace") true;
107 112

  
108 113
      (* self.fp.set('reset_obligation_queue',False) *)
109
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
114
      P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
110 115

  
111 116
      (* self.fp.set('spacer.elim_aux',False) *)
112
      P.add_bool params (mks "spacer.elim_aux") false;
117
      P.add_bool fp_params (mks "spacer.elim_aux") false;
113 118

  
114 119
      (* if self.args.eldarica:
115 120
        *     self.fp.set('print_fixedpoint_extensions', False) *)
116 121
      if !param_eldarica then
117
        P.add_bool params (mks "print_fixedpoint_extensions") false;
122
        P.add_bool fp_params (mks "print_fixedpoint_extensions") false;
118 123
      
119 124
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
120 125
      if !param_utvpi then
121
        P.add_bool params (mks "pdr.utvpi") false;
126
        P.add_bool fp_params (mks "pdr.utvpi") false;
122 127

  
123 128
      (* if self.args.tosmt:
124 129
       *        self.log.info("Setting low level printing")
125 130
       *        self.fp.set ('print.low_level_smt2',True) *)
126 131
      if !param_tosmt then
127
        P.add_bool params (mks "print.low_level_smt2") true;
132
        P.add_bool fp_params (mks "print.low_level_smt2") true;
128 133

  
129 134
      (* if not self.args.pp:
130 135
       *        self.log.info("No pre-processing")
......
132 137
       *        self.fp.set ('xform.inline_linear',False)
133 138
       *        self.fp.set ('xform.inline_eager',False) *\) *)
134 139
      if !param_pp then (
135
        P.add_bool params (mks "xform.slice") false;
136
        P.add_bool params (mks "xform.inline_linear") false;
137
        P.add_bool params (mks "xform.inline_eager") false
140
        P.add_bool fp_params (mks "xform.slice") false;
141
        P.add_bool fp_params (mks "xform.inline_linear") false;
142
        P.add_bool fp_params (mks "xform.inline_eager") false
138 143
      );
139
      Z3.Fixedpoint.set_parameters !fp params
140
              
144

  
145

  
146
      (* Ploc's options. Do not seem to have any effect yet *)
147
      P.add_bool fp_params (mks "print_answer") true;
148
      P.add_bool fp_params (mks "print_certificate") true;
149
      P.add_bool fp_params (mks "xform.slice") false;
150

  
151
      (* Adding a timeout *)
152
      P.add_int fp_params (mks "timeout") !timeout;
153

  
154
      Z3.Fixedpoint.set_parameters !fp fp_params
141 155
      
142 156
    let run basename prog machines =
143 157
      let machines = Machine_code_common.arrow_machine::machines in

Also available in: Unified diff