| /dports/math/z3/z3-z3-4.8.13/src/muz/transforms/ |
| H A D | dl_mk_quantifier_instantiation.cpp | 47 …void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_… in extract_quantifiers()
67 … void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, expr_ref_vector & conjs) { in instantiate_quantifier()
88 …uantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs) { in instantiate_quantifier()
95 …:match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs) { in match()
153 void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs) { in yield_binding()
198 …void mk_quantifier_instantiation::instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref… in instantiate_rule()
265 expr_ref_vector conjs(m); in operator ()() local
|
| H A D | dl_mk_coalesce.cpp | 64 expr_ref_vector revsub(m), conjs(m); in extract_conjs() local
116 expr_ref_vector conjs1(m), conjs(m); in merge_rules() local
|
| H A D | dl_mk_array_blast.cpp | 118 expr_ref_vector conjs(m), trail(m); in ackermanize() local
244 expr_ref_vector conjs(m), new_conjs(m); in blast() local
|
| H A D | dl_mk_slice.cpp | 466 expr_ref_vector conjs = get_tail_conjs(r); in solve_vars() local
629 expr_ref_vector conjs(m); in get_tail_conjs() local
791 expr_ref_vector conjs = get_tail_conjs(r); in update_rule() local
|
| /dports/lang/gcc11/gcc-11.2.0/gcc/testsuite/ada/acats/tests/c3/ |
| H A D | c393010.a | 51 ----------------------------------------------------------------- C393010_0
71 begin
72 -- Check that a call on an abstract operation is a dispatching operation
90 type Passenger_Ticket(Service : Service_Classes) is
100 function Issue( Service : Service_Classes;
157 return Issue( Coach, 0, "non" );
202 begin
203 Num := Num +1;
265 function Travel_Agent_2 return Next_Leg is
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | qe_bool_plugin.cpp | 82 bool solve(conj_enum& conjs,expr* fml) override { in solve()
94 bool solve_units(conj_enum& conjs, expr* _fml) { in solve_units()
|
| H A D | qe_bv_plugin.cpp | 72 bool solve(conj_enum& conjs, expr* fml) override { return false; } in solve()
|
| H A D | qe_lite.cpp | 548 void flatten_definitions(expr_ref_vector& conjs) { in flatten_definitions()
591 void flatten_constructor(app* c, app* r, expr_ref_vector& conjs) { in flatten_constructor()
617 bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) { in is_unconstrained()
627 bool remove_unconstrained(expr_ref_vector& conjs) { in remove_unconstrained()
651 bool reduce_var_set(expr_ref_vector& conjs) { in reduce_var_set()
786 bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e1, expr* e2) { in solve_select()
825 bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e) { in solve_select()
838 bool solve_neq_select(expr_ref_vector& conjs, unsigned i, expr* e) { in solve_neq_select()
2347 expr_ref_vector disjs(m), conjs(m); in operator ()() local
|
| /dports/math/z3/z3-z3-4.8.13/src/model/ |
| H A D | model2expr.cpp | 66 expr_ref_vector conjs(m); in mk_entry_cond() local
82 expr_ref_vector conjs(m); in model2expr() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | qe_bool_plugin.cpp | 82 bool solve(conj_enum& conjs,expr* fml) override { in solve()
94 bool solve_units(conj_enum& conjs, expr* _fml) { in solve_units()
|
| H A D | qe_bv_plugin.cpp | 72 bool solve(conj_enum& conjs, expr* fml) override { return false; } in solve()
|
| H A D | qe_lite.cpp | 548 void flatten_definitions(expr_ref_vector& conjs) { in flatten_definitions()
591 void flatten_constructor(app* c, app* r, expr_ref_vector& conjs) { in flatten_constructor()
617 bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) { in is_unconstrained()
627 bool remove_unconstrained(expr_ref_vector& conjs) { in remove_unconstrained()
651 bool reduce_var_set(expr_ref_vector& conjs) { in reduce_var_set()
786 bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e1, expr* e2) { in solve_select()
825 bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e) { in solve_select()
838 bool solve_neq_select(expr_ref_vector& conjs, unsigned i, expr* e) { in solve_neq_select()
2347 expr_ref_vector disjs(m), conjs(m); in operator ()() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/model/ |
| H A D | model2expr.cpp | 66 expr_ref_vector conjs(m); in mk_entry_cond() local
82 expr_ref_vector conjs(m); in model2expr() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/transforms/ |
| H A D | dl_mk_coalesce.cpp | 64 expr_ref_vector revsub(m), conjs(m); in extract_conjs() local
116 expr_ref_vector conjs1(m), conjs(m); in merge_rules() local
|
| H A D | dl_mk_slice.cpp | 466 expr_ref_vector conjs = get_tail_conjs(r); in solve_vars() local
629 expr_ref_vector conjs(m); in get_tail_conjs() local
791 expr_ref_vector conjs = get_tail_conjs(r); in update_rule() local
|
| /dports/math/z3/z3-z3-4.8.13/src/test/ |
| H A D | doc.cpp | 166 expr_ref_vector conjs(m); in mk_conj() local
182 expr_ref_vector conjs(m); in to_formula() local
206 expr_ref_vector conjs(m); in to_formula() local
|
| /dports/net/wireshark-lite/wireshark-3.6.1/epan/dissectors/ |
| H A D | packet-dcerpc-frsrpc.h | 118 int frsrpc_dissect_struct_CommPktChunk(tvbuff_t *tvb _U_, int offset _U_, packet_info *pinfo _U_, p…
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/ |
| H A D | horn_subsume_model_converter.cpp | 45 expr_ref_vector conjs(m), subst(m); in mk_horn() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/ |
| H A D | horn_subsume_model_converter.cpp | 45 expr_ref_vector conjs(m), subst(m); in mk_horn() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | factor_rewriter.cpp | 130 expr_ref_vector conjs(m()); in mk_is_negative() local
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | factor_rewriter.cpp | 130 expr_ref_vector conjs(m()); in mk_is_negative() local
|
| /dports/www/firefox-legacy/firefox-52.8.0esr/toolkit/content/ |
| H A D | aboutTelemetry.css | 118 font-size: medium;
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_manager.cpp | 70 expr_ref_vector conjs(m); in fixup_clauses() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/dataflow/ |
| H A D | dataflow.h | 100 func_decl* head_sym = r->get_head()->get_decl();
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_manager.cpp | 70 expr_ref_vector conjs(m); in fixup_clauses() local
|