Project

General

Profile

« Previous | Next » 

Revision 8eeec77e

Added by Pierre-Loïc Garoche almost 4 years ago

Filtering out ERR and MAIN from the forall quantification

View differences:

src/tools/zustre/zustre_common.ml
122 122
  
123 123

  
124 124
(* Quantifiying universally all occuring variables *)
125
let add_rule vars expr =
125
let add_rule ?(dont_touch=[]) vars expr =
126 126
  (* let fds = Z3.Expr.get_args expr in *)
127 127
  (* Format.eprintf "Expr %s: args: [%a]@." *)
128 128
  (*   (Z3.Expr.to_string expr) *)
......
143 143
    let nb_args = Z3.Expr.get_num_args e in
144 144
    if nb_args <= 0 then (
145 145
      let fdecl = Z3.Expr.get_func_decl e in
146
      let params = Z3.FuncDecl.get_parameters fdecl in
146
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
147 147
      Format.eprintf "Extracting info about %s: [@?" (Z3.Expr.to_string e);
148 148
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
149 149
      match dkind with Z3enums.OP_UNINTERPRETED -> (
150
	Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | OP_UNINTERPRETED -> "uninter");
151
	let open Z3.FuncDecl.Parameter in
152
	List.iter (fun p ->
153
	  match p with
154
            P_Int i -> Format.eprintf "int %i" i
155
	  | P_Dbl f -> Format.eprintf "dbl %f" f
156
	  | P_Sym s -> Format.eprintf "symb" 
157
	  | P_Srt s -> Format.eprintf "sort" 
158
	  | P_Ast _ ->Format.eprintf "ast" 
159
	  | P_Fdl f -> Format.eprintf "fundecl" 
160
	  | P_Rat s -> Format.eprintf "rat %s" s 
150
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
151
	(* let open Z3.FuncDecl.Parameter in *)
152
	(* List.iter (fun p -> *)
153
	(*   match p with *)
154
        (*     P_Int i -> Format.eprintf "int %i" i *)
155
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
156
	(*   | P_Sym s -> Format.eprintf "symb"  *)
157
	(*   | P_Srt s -> Format.eprintf "sort"  *)
158
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
159
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
160
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
161 161
	     
162
	) params;
163
	Format.eprintf "]@.";
162
	(* ) params; *)
163
	(* Format.eprintf "]@."; *)
164 164
	FDSet.singleton fdecl
165 165
      )
166 166
      | _ -> FDSet.empty
......
170 170
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
171 171
	FDSet.empty (Z3.Expr.get_args e)
172 172
  in
173
  let vars = FDSet.elements (get_expr_vars expr) in
173
  let vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
174 174
  let sorts = List.map Z3.FuncDecl.get_range vars in
175 175
  let symbols = List.map Z3.FuncDecl.get_name vars in
176 176
  

Also available in: Unified diff