| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | bv_elim.cpp | 24 expr_ref_buffer no_pats(m); in reduce_quantifier() local
96 no_pats.push_back(subst(new_no_patterns[j], sub_size, sub)); in reduce_quantifier()
108 no_pats.size(), no_pats.data()); in reduce_quantifier()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | bv_elim.cpp | 24 expr_ref_buffer no_pats(m); in reduce_quantifier() local
96 no_pats.push_back(subst(new_no_patterns[j], sub_size, sub)); in reduce_quantifier()
108 no_pats.size(), no_pats.c_ptr()); in reduce_quantifier()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/substitution/ |
| H A D | substitution.cpp | 196 expr_ref_vector pats(m_manager), no_pats(m_manager); in apply() local
203 no_pats.push_back(std::move(er)); in apply()
206 … er = m_manager.update_quantifier(q, pats.size(), pats.data(), no_pats.size(), no_pats.data(), er); in apply()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/substitution/ |
| H A D | substitution.cpp | 196 expr_ref_vector pats(m_manager), no_pats(m_manager); in apply() local
203 no_pats.push_back(std::move(er)); in apply()
206 …er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er… in apply()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | ast_translation.cpp | 281 expr ** no_pats = pats + num_pats; in process() local
291 num_no_pats, no_pats); in process()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | ast_translation.cpp | 281 expr ** no_pats = pats + num_pats; in process() local
291 num_no_pats, no_pats); in process()
|
| /dports/math/z3/z3-z3-4.8.13/examples/dotnet/ |
| H A D | Program.cs | 614 Expr[] no_pats = new Expr[] { f_y }; in QuantifierExample2()
618 … q1 = ctx.MkForall(bound, body, 1, null, no_pats, ctx.MkSymbol("q"), ctx.MkSymbol("sk")); in QuantifierExample2()
630 Expr[] no_pats = new Expr[] { f_y }; in QuantifierExample2()
637 no_pats, in QuantifierExample2()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/dotnet/ |
| H A D | Program.cs | 614 Expr[] no_pats = new Expr[] { f_y }; in QuantifierExample2()
618 … q1 = ctx.MkForall(bound, body, 1, null, no_pats, ctx.MkSymbol("q"), ctx.MkSymbol("sk")); in QuantifierExample2()
630 Expr[] no_pats = new Expr[] { f_y }; in QuantifierExample2()
637 no_pats, in QuantifierExample2()
|
| /dports/math/z3/z3-z3-4.8.13/examples/java/ |
| H A D | JavaExample.java | 654 Expr[] no_pats = new Expr[] { f_y }; in quantifierExample2() local
658 q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"), in quantifierExample2()
673 Expr[] no_pats = new Expr[] { f_y }; in quantifierExample2() local
680 no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk")); in quantifierExample2()
|
| H A D | JavaGenericExample.java | 606 Expr[] no_pats = new Expr[] { f_y }; in quantifierExample2() local
610 q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"), in quantifierExample2()
625 Expr[] no_pats = new Expr[] { f_y }; in quantifierExample2() local
632 no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk")); in quantifierExample2()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/java/ |
| H A D | JavaExample.java | 654 Expr[] no_pats = new Expr[] { f_y }; in quantifierExample2() local
658 q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"), in quantifierExample2()
673 Expr[] no_pats = new Expr[] { f_y }; in quantifierExample2() local
680 no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk")); in quantifierExample2()
|
| H A D | JavaGenericExample.java | 606 Expr[] no_pats = new Expr[] { f_y };
610 q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"),
625 Expr[] no_pats = new Expr[] { f_y };
632 no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk"));
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/bmc/ |
| H A D | dl_bmc_engine.cpp | 692 expr * const * no_pats = &new_body; in reduce_quantifier() local
693 result = n.m.update_quantifier(old_q, 0, nullptr, 1, no_pats, new_body); in reduce_quantifier()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/bmc/ |
| H A D | dl_bmc_engine.cpp | 692 expr * const * no_pats = &new_body;
693 result = n.m.update_quantifier(old_q, 0, nullptr, 1, no_pats, new_body);
|