Home
last modified time | relevance | path

Searched refs:func_decl (Results 1 – 25 of 1205) sorted by relevance

12345678910>>...49

/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.h36 typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
37 typedef obj_map<func_decl, expr*> const2bv_t;
38 typedef obj_map<func_decl, func_decl*> uf2bvuf_t;
89 virtual void mk_const(func_decl * f, expr_ref & result);
90 virtual void mk_rm_const(func_decl * f, expr_ref & result);
94 void mk_pinf(func_decl * f, expr_ref & result);
95 void mk_ninf(func_decl * f, expr_ref & result);
96 void mk_nan(func_decl * f, expr_ref & result);
97 void mk_nzero(func_decl *f, expr_ref & result);
98 void mk_pzero(func_decl *f, expr_ref & result);
[all …]
H A Dbv2fpa_converter.h35 obj_map<func_decl, expr*> m_const2bv;
36 obj_map<func_decl, expr*> m_rm_const2bv;
37 obj_map<func_decl, func_decl*> m_uf2bvuf;
38 obj_map<func_decl, std::pair<app*, app*> > m_min_max_specials;
53 … void convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
54 …void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen…
56 … void convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
58 func_interp * convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
63 func_decl * new_float_fd;
65 func_decl * bv_fd;
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/
H A Ddl_rule_set.h30 typedef obj_hashtable<func_decl> item_set;
48 void remove_m_data_entry(func_decl * key);
54 item_set & ensure_key(func_decl * pred);
55 void insert(func_decl * depending, func_decl * master);
66 void remove(func_decl * itm);
95 typedef func_decl T;
169 obj_map<func_decl,func_decl*> m_orig2pred;
170 obj_map<func_decl,func_decl*> m_pred2orig;
192 void inherit_predicate(rule_set const& other, func_decl* orig, func_decl* pred);
193 func_decl* get_orig(func_decl* pred) const;
[all …]
H A Ddl_context.h113 virtual bool is_empty_relation(func_decl* pred) const = 0;
121 virtual bool has_facts(func_decl * pred) const = 0;
123 virtual void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) = 0;
288 void register_variable(func_decl* var);
307 void register_predicate(func_decl * pred, bool named);
331 func_decl * res = nullptr; in try_get_predicate_decl()
384 bool has_facts(func_decl * pred) const;
408 unsigned get_num_levels(func_decl* pred);
413 expr_ref get_reachable(func_decl *pred);
420 expr_ref get_cover_delta(int level, func_decl* pred);
[all …]
/dports/math/z3/z3-z3-4.8.13/src/muz/base/
H A Ddl_rule_set.h30 typedef obj_hashtable<func_decl> item_set;
48 void remove_m_data_entry(func_decl * key);
54 item_set & ensure_key(func_decl * pred);
55 void insert(func_decl * depending, func_decl * master);
66 void remove(func_decl * itm);
95 typedef func_decl T;
169 obj_map<func_decl,func_decl*> m_orig2pred;
170 obj_map<func_decl,func_decl*> m_pred2orig;
192 void inherit_predicate(rule_set const& other, func_decl* orig, func_decl* pred);
193 func_decl* get_orig(func_decl* pred) const;
[all …]
H A Ddl_context.h113 virtual bool is_empty_relation(func_decl* pred) const = 0;
121 virtual bool has_facts(func_decl * pred) const = 0;
123 virtual void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) = 0;
288 void register_variable(func_decl* var);
307 void register_predicate(func_decl * pred, bool named);
331 func_decl * res = nullptr; in try_get_predicate_decl()
384 bool has_facts(func_decl * pred) const;
408 unsigned get_num_levels(func_decl* pred);
413 expr_ref get_reachable(func_decl *pred);
420 expr_ref get_cover_delta(int level, func_decl* pred);
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A Dfpa2bv_converter.h36 typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
37 typedef obj_map<func_decl, expr*> const2bv_t;
38 typedef obj_map<func_decl, func_decl*> uf2bvuf_t;
89 virtual void mk_const(func_decl * f, expr_ref & result);
90 virtual void mk_rm_const(func_decl * f, expr_ref & result);
94 void mk_pinf(func_decl * f, expr_ref & result);
95 void mk_ninf(func_decl * f, expr_ref & result);
96 void mk_nan(func_decl * f, expr_ref & result);
97 void mk_nzero(func_decl *f, expr_ref & result);
98 void mk_pzero(func_decl *f, expr_ref & result);
[all …]
H A Dbv2fpa_converter.h35 obj_map<func_decl, expr*> m_const2bv; in expr_counter_proc()
36 obj_map<func_decl, expr*> m_rm_const2bv; in expr_counter_proc()
37 obj_map<func_decl, func_decl*> m_uf2bvuf; in expr_counter_proc()
38 obj_map<func_decl, std::pair<app*, app*> > m_min_max_specials; in expr_counter_proc()
53 … void convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen); in expr_counter_proc()
54 …void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen… in expr_counter_proc()
56 … void convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen); in expr_counter_proc()
58 func_interp * convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f); in expr_counter_proc()
63 func_decl * new_float_fd; in expr_counter_proc()
65 func_decl * bv_fd; in expr_counter_proc()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/model/
H A Dmodel_core.h29 typedef obj_map<func_decl, i_expr> decl2expr;
30 typedef obj_map<func_decl, func_interp*> decl2finterp;
36 ptr_vector<func_decl> m_const_decls;
37 ptr_vector<func_decl> m_func_decls;
51 bool eval(func_decl * f, expr_ref & r) const;
52 bool is_true_decl(func_decl *f) const { in is_true_decl()
56 bool is_false_decl(func_decl *f) const { in is_false_decl()
70 void register_decl(func_decl * d, expr * v);
71 void register_decl(func_decl * f, func_interp * fi);
72 void unregister_decl(func_decl * d);
[all …]
H A Dmodel_macro_solver.h40 void set_else_interp(func_decl* f, expr* f_else);
126 typedef obj_map<func_decl, quantifier_set*> q_f;
130 typedef obj_map<func_decl, expr_set*> f2defs;
138 void insert_q_f(quantifier* q, func_decl* f);
140 void insert_f2def(func_decl* f, expr* def);
143 quantifier_set* get_q_f_def(func_decl* f, expr* def);
184 typedef obj_map<func_decl, expr*> f2def;
207 void greedy(func_decl* f, unsigned depth);
216 obj_hashtable<func_decl> m_acyclic;
240 void process(func_decl* f);
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/model/
H A Dmodel_core.h29 typedef obj_map<func_decl, i_expr> decl2expr;
30 typedef obj_map<func_decl, func_interp*> decl2finterp;
36 ptr_vector<func_decl> m_const_decls;
37 ptr_vector<func_decl> m_func_decls;
51 bool eval(func_decl * f, expr_ref & r) const;
52 bool is_true_decl(func_decl *f) const {
56 bool is_false_decl(func_decl *f) const {
70 void register_decl(func_decl * d, expr * v);
71 void register_decl(func_decl * f, func_interp * fi);
72 void unregister_decl(func_decl * d);
[all …]
H A Dmodel_macro_solver.h40 void set_else_interp(func_decl* f, expr* f_else);
126 typedef obj_map<func_decl, quantifier_set*> q_f;
130 typedef obj_map<func_decl, expr_set*> f2defs;
138 void insert_q_f(quantifier* q, func_decl* f);
140 void insert_f2def(func_decl* f, expr* def);
143 quantifier_set* get_q_f_def(func_decl* f, expr* def);
184 typedef obj_map<func_decl, expr*> f2def;
207 void greedy(func_decl* f, unsigned depth);
216 obj_hashtable<func_decl> m_acyclic;
240 void process(func_decl* f);
[all …]
/dports/math/z3/z3-z3-4.8.13/src/ast/
H A Dbv_decl_plugin.h122 inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) { in get_div0_decl()
141 func_decl * m_bit0;
142 func_decl * m_bit1;
143 func_decl * m_carry;
144 func_decl * m_xor3;
149 ptr_vector<func_decl> m_bv_neg;
150 ptr_vector<func_decl> m_bv_add;
181 ptr_vector<func_decl> m_bv_or;
205 ptr_vector<func_decl> m_mkbv;
211 func_decl * mk_binary(ptr_vector<func_decl> & decls, decl_kind k,
[all …]
H A Darray_decl_plugin.h79 func_decl * mk_map(func_decl* f, unsigned arity, sort* const* domain);
81 func_decl * mk_default(unsigned arity, sort* const* domain);
83 func_decl * mk_select(unsigned arity, sort * const * domain);
85 func_decl * mk_store(unsigned arity, sort * const * domain);
99 func_decl * mk_as_array(func_decl * f);
166 …bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && … in is_as_array()
167 func_decl * get_as_array_func_decl(expr * n) const;
168 func_decl * get_as_array_func_decl(func_decl* f) const;
169 func_decl * get_map_func_decl(func_decl* f) const;
262 func_decl * mk_array_ext(sort* domain, unsigned i);
[all …]
H A Dspecial_relations_decl_plugin.h49 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
75 func_decl* mk_rel_decl(func_decl* f, decl_kind k) { in mk_rel_decl()
86 bool is_special_relation(func_decl* f) const { return f->get_family_id() == fid(); } in is_special_relation()
88 sr_property get_property(func_decl* f) const;
90 …func_decl* get_relation(func_decl* f) const { SASSERT(is_special_relation(f)); return to_func_decl… in get_relation()
92 func_decl* mk_to_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TO); } in mk_to_decl()
93 func_decl* mk_po_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PO); } in mk_po_decl()
94 func_decl* mk_plo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PLO); } in mk_plo_decl()
95 func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); } in mk_lo_decl()
96 func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); } in mk_tc_decl()
H A Darith_decl_plugin.h95 func_decl * m_r_le_decl;
96 func_decl * m_r_ge_decl;
97 func_decl * m_r_lt_decl;
98 func_decl * m_r_gt_decl;
106 func_decl * m_i_le_decl;
107 func_decl * m_i_ge_decl;
108 func_decl * m_i_lt_decl;
109 func_decl * m_i_gt_decl;
128 func_decl * m_sin_decl;
129 func_decl * m_cos_decl;
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/
H A Dbv_decl_plugin.h122 inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) { in get_div0_decl()
141 func_decl * m_bit0;
142 func_decl * m_bit1;
143 func_decl * m_carry;
144 func_decl * m_xor3;
149 ptr_vector<func_decl> m_bv_neg;
150 ptr_vector<func_decl> m_bv_add;
181 ptr_vector<func_decl> m_bv_or;
205 ptr_vector<func_decl> m_mkbv;
211 func_decl * mk_binary(ptr_vector<func_decl> & decls, decl_kind k,
[all …]
H A Darray_decl_plugin.h79 func_decl * mk_map(func_decl* f, unsigned arity, sort* const* domain);
81 func_decl * mk_default(unsigned arity, sort* const* domain);
83 func_decl * mk_select(unsigned arity, sort * const * domain);
85 func_decl * mk_store(unsigned arity, sort * const * domain);
99 func_decl * mk_as_array(func_decl * f);
166 …bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && … in is_as_array()
167 func_decl * get_as_array_func_decl(expr * n) const;
168 func_decl * get_as_array_func_decl(func_decl* f) const;
169 func_decl * get_map_func_decl(func_decl* f) const;
261 func_decl * mk_array_ext(sort* domain, unsigned i);
[all …]
H A Darith_decl_plugin.h95 func_decl * m_r_le_decl;
96 func_decl * m_r_ge_decl;
97 func_decl * m_r_lt_decl;
98 func_decl * m_r_gt_decl;
106 func_decl * m_i_le_decl;
107 func_decl * m_i_ge_decl;
108 func_decl * m_i_lt_decl;
109 func_decl * m_i_gt_decl;
128 func_decl * m_sin_decl;
129 func_decl * m_cos_decl;
[all …]
H A Dspecial_relations_decl_plugin.h49 func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
75 func_decl* mk_rel_decl(func_decl* f, decl_kind k) { in mk_rel_decl()
86 bool is_special_relation(func_decl* f) const { return f->get_family_id() == fid(); } in is_special_relation()
88 sr_property get_property(func_decl* f) const;
91 func_decl* mk_to_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TO); } in mk_to_decl()
92 func_decl* mk_po_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PO); } in mk_po_decl()
93 func_decl* mk_plo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PLO); } in mk_plo_decl()
94 func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); } in mk_lo_decl()
95 func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); } in mk_tc_decl()
/dports/math/z3/z3-z3-4.8.13/src/muz/rel/
H A Drel_context.h32 typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
64 relation_base & get_relation(func_decl * pred) override;
65 relation_base * try_get_relation(func_decl * pred) const override;
66 bool is_empty_relation(func_decl* pred) const override;
67 expr_ref try_get_formula(func_decl * pred) const override;
73 lbool query(unsigned num_rels, func_decl * const* rels) override;
78 void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) override;
107 void add_fact(func_decl* pred, relation_fact const& fact) override;
108 void add_fact(func_decl* pred, table_fact const& fact) override;
112 bool has_facts(func_decl * pred) const override;
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/rel/
H A Drel_context.h32 typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
64 relation_base & get_relation(func_decl * pred) override;
65 relation_base * try_get_relation(func_decl * pred) const override;
66 bool is_empty_relation(func_decl* pred) const override;
67 expr_ref try_get_formula(func_decl * pred) const override;
73 lbool query(unsigned num_rels, func_decl * const* rels) override;
78 void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) override;
107 void add_fact(func_decl* pred, relation_fact const& fact) override;
108 void add_fact(func_decl* pred, table_fact const& fact) override;
112 bool has_facts(func_decl * pred) const override;
[all …]
/dports/math/z3/z3-z3-4.8.13/src/muz/spacer/
H A Dspacer_sym_mux.h40 typedef obj_map<func_decl, sym_mux_entry*> decl2entry_map;
41 typedef obj_map<func_decl, std::pair<sym_mux_entry*, unsigned> > mux2entry_map;
47 func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const;
55 void register_decl(func_decl *fdecl);
56 bool find_idx(func_decl * sym, unsigned & idx) const;
57 bool has_index(func_decl * sym, unsigned idx) const in has_index()
60 bool is_muxed(func_decl *fdecl) const {return m_muxes.contains(fdecl);} in is_muxed()
66 func_decl * find_by_decl(func_decl* fdecl, unsigned idx) const;
79 func_decl * shift_decl(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const;
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/
H A Dspacer_sym_mux.h40 typedef obj_map<func_decl, sym_mux_entry*> decl2entry_map;
41 typedef obj_map<func_decl, std::pair<sym_mux_entry*, unsigned> > mux2entry_map;
47 func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const;
55 void register_decl(func_decl *fdecl);
56 bool find_idx(func_decl * sym, unsigned & idx) const;
57 bool has_index(func_decl * sym, unsigned idx) const in has_index()
60 bool is_muxed(func_decl *fdecl) const {return m_muxes.contains(fdecl);} in is_muxed()
66 func_decl * find_by_decl(func_decl* fdecl, unsigned idx) const;
79 func_decl * shift_decl(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const;
/dports/math/z3/z3-z3-4.8.13/src/ast/macros/
H A Dmacro_manager.h41 obj_map<func_decl, quantifier *> m_decl2macro; // func-decl -> quantifier
42 obj_map<func_decl, proof *> m_decl2macro_pr; // func-decl -> quantifier_proof
43 obj_map<func_decl, expr_dependency *> m_decl2macro_dep; // func-decl -> unsat core dependency
48 obj_hashtable<func_decl> m_forbidden_set;
70 bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = nullptr);
78 bool is_forbidden(func_decl * d) const { return m_forbidden_set.contains(d); } in is_forbidden()
79 obj_hashtable<func_decl> const & get_forbidden_set() const { return m_forbidden_set; } in get_forbidden_set()
81 bool contains(func_decl* d) const { return m_decls.contains(d); } in contains()
84 func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); } in get_macro_func_decl()
85 func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
[all …]

12345678910>>...49