/dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
H A D | propagate_values_tactic.cpp | 75 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 D | der_tactic.cpp | 40 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 D | simplify_tactic.cpp | 51 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 D | nnf_tactic.cpp | 70 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 D | distribute_forall_tactic.cpp | 115 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 D | propagate_values_tactic.cpp | 75 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 D | der_tactic.cpp | 40 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 D | simplify_tactic.cpp | 51 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 D | nnf_tactic.cpp | 70 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 D | distribute_forall_tactic.cpp | 115 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 D | edit.c | 310 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 D | macro_finder.cpp | 81 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 D | macro_manager.cpp | 360 …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 D | macro_finder.cpp | 81 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 D | macro_manager.cpp | 350 …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 D | arith_bounds_tactic.cpp | 96 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 D | eq2bv_tactic.cpp | 206 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 D | arith_bounds_tactic.cpp | 96 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 D | eq2bv_tactic.cpp | 206 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 D | qe_tactic.cpp | 53 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 D | qe_tactic.cpp | 53 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 D | bvarray2uf_tactic.cpp | 73 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 D | dt2bv_tactic.cpp | 134 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 D | bvarray2uf_tactic.cpp | 73 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 D | dt2bv_tactic.cpp | 134 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));
|