Home
last modified time | relevance | path

Searched refs:new_pr (Results 1 – 25 of 97) sorted by relevance

1234

/dports/math/z3/z3-z3-4.8.13/src/tactic/core/
H A Dpropagate_values_tactic.cpp75 void push_result(expr * new_curr, proof * new_pr) { in push_result() argument
78 new_pr = m.mk_modus_ponens(pr, new_pr); in push_result()
91 m_goal->update(m_idx, new_curr, new_pr, new_d); in push_result()
98 m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d); in push_result()
104 if (inverted && new_pr) new_pr = m.mk_symmetry(new_pr); in push_result()
105 m_subst->insert(lhs, value, new_pr, new_d); in push_result()
112 proof_ref new_pr(m); in process_current() local
115 m_r(curr, new_curr, new_pr); in process_current()
120 new_pr = m.mk_reflexivity(curr); in process_current()
127 push_result(new_curr, new_pr); in process_current()
[all …]
H A Dder_tactic.cpp40 proof_ref new_pr(m()); in operator ()() local
46 m_r(curr, new_curr, new_pr); in operator ()()
49 new_pr = m().mk_modus_ponens(pr, new_pr); in operator ()()
51 g.update(idx, new_curr, new_pr, g.dep(idx)); in operator ()()
H A Dsimplify_tactic.cpp51 proof_ref new_pr(m()); in operator ()() local
57 m_r(curr, new_curr, new_pr); in operator ()()
61 new_pr = m().mk_modus_ponens(pr, new_pr); in operator ()()
63 g.update(idx, new_curr, new_pr, g.dep(idx)); in operator ()()
H A Dnnf_tactic.cpp70 proof_ref new_pr(m); in operator ()() local
75 local_nnf(curr, defs, def_prs, new_curr, new_pr); in operator ()()
78 new_pr = m.mk_modus_ponens(pr, new_pr); in operator ()()
80 g->update(i, new_curr, new_pr, g->dep(i)); in operator ()()
H A Ddistribute_forall_tactic.cpp115 proof_ref new_pr(m); in operator ()() local
121 r(curr, new_curr, new_pr); in operator ()()
124 new_pr = m.mk_modus_ponens(pr, new_pr); in operator ()()
126 g->update(idx, new_curr, new_pr, g->dep(idx)); in operator ()()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/
H A Dpropagate_values_tactic.cpp75 void push_result(expr * new_curr, proof * new_pr) { in push_result() argument
78 new_pr = m.mk_modus_ponens(pr, new_pr); in push_result()
91 m_goal->update(m_idx, new_curr, new_pr, new_d); in push_result()
98 m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d); in push_result()
104 if (inverted && new_pr) new_pr = m.mk_symmetry(new_pr); in push_result()
105 m_subst->insert(lhs, value, new_pr, new_d); in push_result()
112 proof_ref new_pr(m); in process_current() local
115 m_r(curr, new_curr, new_pr); in process_current()
120 new_pr = m.mk_reflexivity(curr); in process_current()
127 push_result(new_curr, new_pr); in process_current()
[all …]
H A Dder_tactic.cpp40 proof_ref new_pr(m()); in operator ()() local
46 m_r(curr, new_curr, new_pr); in operator ()()
49 new_pr = m().mk_modus_ponens(pr, new_pr); in operator ()()
51 g.update(idx, new_curr, new_pr, g.dep(idx)); in operator ()()
H A Dsimplify_tactic.cpp51 proof_ref new_pr(m()); in operator ()() local
57 m_r(curr, new_curr, new_pr); in operator ()()
61 new_pr = m().mk_modus_ponens(pr, new_pr); in operator ()()
63 g.update(idx, new_curr, new_pr, g.dep(idx)); in operator ()()
H A Dnnf_tactic.cpp70 proof_ref new_pr(m); in operator ()() local
75 local_nnf(curr, defs, def_prs, new_curr, new_pr); in operator ()()
78 new_pr = m.mk_modus_ponens(pr, new_pr); in operator ()()
80 g->update(i, new_curr, new_pr, g->dep(i)); in operator ()()
H A Ddistribute_forall_tactic.cpp115 proof_ref new_pr(m); in operator ()() local
121 r(curr, new_curr, new_pr); in operator ()()
124 new_pr = m.mk_modus_ponens(pr, new_pr); in operator ()()
126 g->update(idx, new_curr, new_pr, g->dep(idx)); in operator ()()
/dports/databases/gnats4/gnats-4.1.0/gnats/
H A Dedit.c310 unsetField (new_pr, field); in processPRChanges()
336 unsetField (new_pr, field); in processPRChanges()
421 if (! isPrLocked (new_pr->database, field_value (new_pr, NUMBER (database)))) in rewrite_pr()
499 new_path = gen_pr_path (new_pr); in rewrite_pr()
514 buildIndexEntry (new_pr); in rewrite_pr()
579 read_pr (new_pr, fp, 0); in replace_pr()
610 free_pr (new_pr); in replace_pr()
995 PR *pr, *new_pr; in edit_field() local
1070 new_pr = allocPR (database); in edit_field()
1074 fillInPR (new_pr, err); in edit_field()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/ast/macros/
H A Dmacro_finder.cpp81 proof * new_pr = nullptr; in is_arith_macro() local
84 new_pr = m.mk_modus_ponens(pr, rw); in is_arith_macro()
112 proof * mp = m.mk_modus_ponens(new_pr, rw); in is_arith_macro()
154 proof * new_pr = nullptr; in is_arith_macro() local
157 new_pr = m.mk_modus_ponens(pr, rw); in is_arith_macro()
160 return m_macro_manager.insert(f, new_q, new_pr); in is_arith_macro()
183 proof * mp = m.mk_modus_ponens(new_pr, rw); in is_arith_macro()
287 proof_ref new_pr(m); in expand_macros() local
307 new_prs.push_back(new_pr); in expand_macros()
355 proof_ref new_pr(m); in expand_macros() local
[all …]
H A Dmacro_manager.cpp360 …s(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_r… in expand_macros() argument
376 new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr); in expand_macros()
381 old_pr = new_pr; in expand_macros()
384 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros()
392 new_pr = m.mk_modus_ponens(new_pr, rw_pr); in expand_macros()
393 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros()
398 new_pr = pr; in expand_macros()
402 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/macros/
H A Dmacro_finder.cpp81 proof * new_pr = nullptr; in is_arith_macro() local
84 new_pr = m.mk_modus_ponens(pr, rw); in is_arith_macro()
112 proof * mp = m.mk_modus_ponens(new_pr, rw); in is_arith_macro()
154 proof * new_pr = nullptr; in is_arith_macro() local
157 new_pr = m.mk_modus_ponens(pr, rw); in is_arith_macro()
160 return m_macro_manager.insert(f, new_q, new_pr); in is_arith_macro()
183 proof * mp = m.mk_modus_ponens(new_pr, rw); in is_arith_macro()
287 proof_ref new_pr(m); in expand_macros() local
307 new_prs.push_back(new_pr); in expand_macros()
355 proof_ref new_pr(m); in expand_macros() local
[all …]
H A Dmacro_manager.cpp350 …s(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_r… in expand_macros() argument
366 new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr); in expand_macros()
371 old_pr = new_pr; in expand_macros()
374 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros()
382 new_pr = m.mk_modus_ponens(new_pr, rw_pr); in expand_macros()
383 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros()
388 new_pr = pr; in expand_macros()
392 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros()
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/
H A Darith_bounds_tactic.cpp96 proof_ref new_pr(m); in bounds_arith_subsumption() local
100 mk_proof(new_pr, s, i, inf.idx); in bounds_arith_subsumption()
101 s->update(inf.idx, m.mk_true(), new_pr); in bounds_arith_subsumption()
108 mk_proof(new_pr, s, inf.idx, i); in bounds_arith_subsumption()
109 s->update(i, m.mk_true(), new_pr); in bounds_arith_subsumption()
120 mk_proof(new_pr, s, i, inf.idx); in bounds_arith_subsumption()
121 s->update(inf.idx, m.mk_true(), new_pr); in bounds_arith_subsumption()
128 mk_proof(new_pr, s, inf.idx, i); in bounds_arith_subsumption()
H A Deq2bv_tactic.cpp206 proof_ref new_pr(m); in operator ()() local
210 new_pr = m.mk_rewrite(g->form(i), m.mk_true()); in operator ()()
211 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
221 g->update(i, m.mk_true(), new_pr, nullptr); in operator ()()
228 new_pr = m.mk_rewrite(g->form(i), new_curr); in operator ()()
229 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
231 g->update(i, new_curr, new_pr); in operator ()()
234 m_rw(g->form(i), new_curr, new_pr); in operator ()()
239 if (!new_pr) new_pr = m.mk_rewrite(g->form(i), new_curr); in operator ()()
240 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/
H A Darith_bounds_tactic.cpp96 proof_ref new_pr(m); in bounds_arith_subsumption() local
100 mk_proof(new_pr, s, i, inf.idx); in bounds_arith_subsumption()
101 s->update(inf.idx, m.mk_true(), new_pr); in bounds_arith_subsumption()
108 mk_proof(new_pr, s, inf.idx, i); in bounds_arith_subsumption()
109 s->update(i, m.mk_true(), new_pr); in bounds_arith_subsumption()
120 mk_proof(new_pr, s, i, inf.idx); in bounds_arith_subsumption()
121 s->update(inf.idx, m.mk_true(), new_pr); in bounds_arith_subsumption()
128 mk_proof(new_pr, s, inf.idx, i); in bounds_arith_subsumption()
H A Deq2bv_tactic.cpp206 proof_ref new_pr(m); in operator ()() local
210 new_pr = m.mk_rewrite(g->form(i), m.mk_true()); in operator ()()
211 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
221 g->update(i, m.mk_true(), new_pr, nullptr); in operator ()()
228 new_pr = m.mk_rewrite(g->form(i), new_curr); in operator ()()
229 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
231 g->update(i, new_curr, new_pr); in operator ()()
234 m_rw(g->form(i), new_curr, new_pr); in operator ()()
239 if (!new_pr) new_pr = m.mk_rewrite(g->form(i), new_curr); in operator ()()
240 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/qe/
H A Dqe_tactic.cpp53 proof_ref new_pr(m); in operator ()() local
66 new_pr = nullptr; in operator ()()
68 new_pr = m.mk_rewrite(f, new_f); in operator ()()
69 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
71 g->update(i, new_f, new_pr, g->dep(i)); in operator ()()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/
H A Dqe_tactic.cpp53 proof_ref new_pr(m); in operator ()() local
66 new_pr = nullptr; in operator ()()
68 new_pr = m.mk_rewrite(f, new_f); in operator ()()
69 new_pr = m.mk_modus_ponens(g->pr(i), new_pr); in operator ()()
71 g->update(i, new_f, new_pr, g->dep(i)); in operator ()()
/dports/math/z3/z3-z3-4.8.13/src/tactic/bv/
H A Dbvarray2uf_tactic.cpp73 proof_ref new_pr(m_manager); in operator ()() local
79 m_rw(curr, new_curr, new_pr); in operator ()()
82 new_pr = m_manager.mk_modus_ponens(pr, new_pr); in operator ()()
84 g->update(idx, new_curr, new_pr, g->dep(idx)); in operator ()()
H A Ddt2bv_tactic.cpp134 proof_ref new_pr(m); in operator ()() local
136 rw(g->form(idx), new_curr, new_pr); in operator ()()
139 new_pr = m.mk_modus_ponens(pr, new_pr); in operator ()()
141 g->update(idx, new_curr, new_pr, g->dep(idx)); in operator ()()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/
H A Dbvarray2uf_tactic.cpp73 proof_ref new_pr(m_manager);
79 m_rw(curr, new_curr, new_pr);
82 new_pr = m_manager.mk_modus_ponens(pr, new_pr);
84 g->update(idx, new_curr, new_pr, g->dep(idx));
H A Ddt2bv_tactic.cpp134 proof_ref new_pr(m);
136 rw(g->form(idx), new_curr, new_pr);
139 new_pr = m.mk_modus_ponens(pr, new_pr);
141 g->update(idx, new_curr, new_pr, g->dep(idx));

1234