/dports/math/z3/z3-z3-4.8.13/src/ast/proofs/ |
H A D | proof_utils.cpp | 127 m_hyps.insert(m.get_fact(p)); in compute_marks() 297 if (m.is_false(m.get_fact(res))) { in reduce_units() 394 hyps->insert(m.get_fact(p)); in add_hypotheses() 516 expr* fact = m.get_fact(p); in elim() 605 SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i))); in elim() 627 expr* clause = m.get_fact(tmp); in elim() 770 expr* cls = m.get_fact(p); in check() 781 expr* fact = m.get_fact(p); in check() 897 args.push_back(m.get_fact(pr)); in permute_unit_resolution() 952 if (m.get_fact(p0) == m.get_fact(p)) { in push() [all …]
|
H A D | proof_utils.h | 80 m.get_fact(to_app(arg)) == fact) { in matches_fact() 196 if (!m.is_true(m.get_fact(arg))) in operator() 209 SASSERT(m.get_fact(newp) == args.back()); in operator()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/proofs/ |
H A D | proof_utils.cpp | 127 m_hyps.insert(m.get_fact(p)); in compute_marks() 297 if (m.is_false(m.get_fact(res))) { in reduce_units() 394 hyps->insert(m.get_fact(p)); in add_hypotheses() 516 expr* fact = m.get_fact(p); in elim() 605 SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i))); in elim() 627 expr* clause = m.get_fact(tmp); in elim() 770 expr* cls = m.get_fact(p); in check() 781 expr* fact = m.get_fact(p); in check() 897 args.push_back(m.get_fact(pr)); in permute_unit_resolution() 952 if (m.get_fact(p0) == m.get_fact(p)) { in push() [all …]
|
H A D | proof_utils.h | 80 m.get_fact(to_app(arg)) == fact) { in matches_fact() 196 if (!m.is_true(m.get_fact(arg))) in operator() 209 SASSERT(m.get_fact(newp) == args.back()); in operator()
|
/dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
H A D | spacer_proof_utils.cpp | 301 lit0 = m.get_fact(parents.get(0)); in mk_fk_from_ab() 376 app *fact = to_app(m.get_fact(p)); in reduce() 425 SASSERT(m.get_fact(res) == m.get_fact(p)); in reduce() 534 m_hyp_mark.mark(m.get_fact(p)); in compute_hypsets() 608 SASSERT(m.is_false(m.get_fact(pf))); in reduce_core() 710 SASSERT(m.is_false(m.get_fact(premise))); in mk_lemma_core() 729 hyp_fact = m.get_fact(hyp); in mk_lemma_core() 750 if (m.is_false(m.get_fact(args[i]))) { in mk_unit_resolution_core() 758 app *fact0 = to_app(m.get_fact(arg0)); in mk_unit_resolution_core() 828 if (m.is_false(m.get_fact(args[i]))) { in mk_proof_core() [all …]
|
H A D | spacer_farkas_learner.cpp | 254 expr* fact = m.get_fact(arg); in get_lemmas() 257 tout << "Add: " << mk_pp(m.get_fact(arg), m) << "\n"; in get_lemmas() 271 if (bs.contains(m.get_fact(p))) { in get_lemmas() 280 hyps->insert(m.get_fact(p)); in get_lemmas() 286 if (!is_pure_expr(Bsymbs, m.get_fact(p), m)) { in get_lemmas() 296 expr* fml = m.get_fact(p); in get_lemmas() 333 tout << mk_pp(m.get_fact(p), m) << "\n"; in get_lemmas() 349 lits.push_back(to_app(m.get_fact(prem))); in get_lemmas() 356 expr* fact = m.get_fact(p); in get_lemmas() 413 bs.contains(m.get_fact(p))) { in get_asserted() [all …]
|
H A D | spacer_unsat_core_plugin.cpp | 74 expr* fact = m.get_fact(pf); in add_lowest_split_to_core() 143 … tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; in compute_partial_core() 174 … coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); in compute_partial_core() 186 expr* conclusion = m.get_fact(step); in compute_partial_core() 258 … tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; in compute_partial_core() 274 (std::make_pair(abs(coefficient), to_app(m.get_fact(premise)))); in compute_partial_core() 561 spacer::is_literal(m, m.get_fact(current)))) in advance_to_lowest_partial_cut() 629 m_node_to_formula[node_other] = m.get_fact(i); in add_edge() 630 m_node_to_formula[node_i] = m.get_fact(i); in add_edge() 659 m_node_to_formula[node_j] = m.get_fact(j); in add_edge() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
H A D | spacer_proof_utils.cpp | 301 lit0 = m.get_fact(parents.get(0)); in mk_fk_from_ab() 376 app *fact = to_app(m.get_fact(p)); in reduce() 425 SASSERT(m.get_fact(res) == m.get_fact(p)); in reduce() 534 m_hyp_mark.mark(m.get_fact(p)); in compute_hypsets() 608 SASSERT(m.is_false(m.get_fact(pf))); in reduce_core() 710 SASSERT(m.is_false(m.get_fact(premise))); in mk_lemma_core() 729 hyp_fact = m.get_fact(hyp); in mk_lemma_core() 750 if (m.is_false(m.get_fact(args[i]))) { in mk_unit_resolution_core() 758 app *fact0 = to_app(m.get_fact(arg0)); in mk_unit_resolution_core() 828 if (m.is_false(m.get_fact(args[i]))) { in mk_proof_core() [all …]
|
H A D | spacer_farkas_learner.cpp | 254 expr* fact = m.get_fact(arg); in get_lemmas() 257 tout << "Add: " << mk_pp(m.get_fact(arg), m) << "\n"; in get_lemmas() 271 if (bs.contains(m.get_fact(p))) { in get_lemmas() 280 hyps->insert(m.get_fact(p)); in get_lemmas() 286 if (!is_pure_expr(Bsymbs, m.get_fact(p), m)) { in get_lemmas() 296 expr* fml = m.get_fact(p); in get_lemmas() 333 tout << mk_pp(m.get_fact(p), m) << "\n"; in get_lemmas() 349 lits.push_back(to_app(m.get_fact(prem))); in get_lemmas() 356 expr* fact = m.get_fact(p); in get_lemmas() 413 bs.contains(m.get_fact(p))) { in get_asserted() [all …]
|
H A D | spacer_unsat_core_plugin.cpp | 74 expr* fact = m.get_fact(pf); in add_lowest_split_to_core() 143 … tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; in compute_partial_core() 174 … coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); in compute_partial_core() 186 expr* conclusion = m.get_fact(step); in compute_partial_core() 258 … tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; in compute_partial_core() 274 (std::make_pair(abs(coefficient), to_app(m.get_fact(premise)))); in compute_partial_core() 561 spacer::is_literal(m, m.get_fact(current)))) in advance_to_lowest_partial_cut() 629 m_node_to_formula[node_other] = m.get_fact(i); in add_edge() 630 m_node_to_formula[node_i] = m.get_fact(i); in add_edge() 659 m_node_to_formula[node_j] = m.get_fact(j); in add_edge() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/ast/ |
H A D | ast.cpp | 2737 …CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2)… in mk_modus_ponens() 2740 SASSERT(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))); in mk_modus_ponens() 2741 CTRACE("mk_modus_ponens", to_app(get_fact(p2))->get_arg(0) != get_fact(p1), in mk_modus_ponens() 2799 …mk_app(to_app(get_fact(p))->get_decl(), to_app(get_fact(p))->get_arg(1), to_app(get_fact(p))->get_… in mk_symmetry() 2820 ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) && in mk_transitivity() 2821 (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))); in mk_transitivity() 2827 SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)); in mk_transitivity() 2834 if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl(); in mk_transitivity() 2906 SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p))); in mk_quant_intro() 2914 SASSERT(is_oeq(get_fact(p)) || is_lambda(get_fact(p))); in mk_oeq_quant_intro() [all …]
|
H A D | expr_substitution.cpp | 69 SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(0) == c); in insert() 70 SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(1) == def); in insert()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
H A D | ast.cpp | 2815 …CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2)… in mk_modus_ponens() 2818 SASSERT(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))); in mk_modus_ponens() 2819 CTRACE("mk_modus_ponens", to_app(get_fact(p2))->get_arg(0) != get_fact(p1), in mk_modus_ponens() 2877 …mk_app(to_app(get_fact(p))->get_decl(), to_app(get_fact(p))->get_arg(1), to_app(get_fact(p))->get_… in mk_symmetry() 2898 ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) && in mk_transitivity() 2899 (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))); in mk_transitivity() 2905 SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)); in mk_transitivity() 2912 if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl(); in mk_transitivity() 2984 SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p))); in mk_quant_intro() 2992 SASSERT(is_oeq(get_fact(p)) || is_lambda(get_fact(p))); in mk_oeq_quant_intro() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
H A D | hnf.cpp | 226 SASSERT(!premise || fml == m.get_fact(premise)); in mk_horn() 248 SASSERT(!premise || (fml1 == fml && fml == m.get_fact(premise))); in mk_horn() 315 if (m.is_iff(m.get_fact(p))) { in mk_quant_intro() 318 if (m.is_oeq(m.get_fact(p))) { in mk_quant_intro() 466 expr* fact = m.get_fact(p1); in mk_congruence() 469 fact = m.get_fact(p1); in mk_congruence() 483 if (m.get_fact(premise) == m.get_fact(result)) { in mk_modus_ponens() 491 app* f = to_app(m.get_fact(p1)); in mk_transitivity() 497 app* f = to_app(m.get_fact(p2)); in mk_transitivity()
|
H A D | dl_boogie_proof.cpp | 108 if (m.get_fact(premises1[k].get()) == lit) { in mk_input_resolution() 160 steps[j].m_fact = m.get_fact(p); in pp_proof() 219 quantifier* q = to_quantifier(m.get_fact(premises[0].get())); in get_subst()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
H A D | hnf.cpp | 227 SASSERT(!premise || fml == m.get_fact(premise)); in mk_horn() 249 SASSERT(!premise || (fml1 == fml && fml == m.get_fact(premise))); in mk_horn() 316 if (m.is_iff(m.get_fact(p))) { in mk_quant_intro() 319 if (m.is_oeq(m.get_fact(p))) { in mk_quant_intro() 467 expr* fact = m.get_fact(p1); in mk_congruence() 470 fact = m.get_fact(p1); in mk_congruence() 484 if (m.get_fact(premise) == m.get_fact(result)) { in mk_modus_ponens() 492 app* f = to_app(m.get_fact(p1)); in mk_transitivity() 498 app* f = to_app(m.get_fact(p2)); in mk_transitivity()
|
H A D | dl_boogie_proof.cpp | 108 if (m.get_fact(premises1[k].get()) == lit) { in mk_input_resolution() 160 steps[j].m_fact = m.get_fact(p); in pp_proof() 219 quantifier* q = to_quantifier(m.get_fact(premises[0].get())); in get_subst()
|
/dports/math/z3/z3-z3-4.8.13/src/muz/rel/ |
H A D | dl_base.cpp | 257 k.get_fact(row); in reset() 266 k.get_fact(row); in contains_fact() 283 k.get_fact(row); in fetch_fact() 333 k.get_fact(row); in clone() 429 void table_base::row_interface::get_fact(table_fact & result) const { in get_fact() function in datalog::table_base::row_interface 440 get_fact(fact); in display() 454 r.get_fact(fact); in to_formula()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/rel/ |
H A D | dl_base.cpp | 257 k.get_fact(row); in reset() 266 k.get_fact(row); in contains_fact() 283 k.get_fact(row); in fetch_fact() 333 k.get_fact(row); in clone() 429 void table_base::row_interface::get_fact(table_fact & result) const { in get_fact() function in datalog::table_base::row_interface 440 get_fact(fact); in display() 454 r.get_fact(fact); in to_formula()
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_justification.cpp | 100 for (proof* p : prs) tout << mk_ll_pp(m.get_fact(p), m);); in mk_proof() 165 proof * pr2 = m.mk_rewrite(m.get_fact(pr1), lit); in mk_proof() 206 app* fact1 = to_app(m.get_fact(pr1)); in mk_proof() 207 app* fact2 = to_app(m.get_fact(pr2)); in mk_proof() 211 fact1 = to_app(m.get_fact(pr1)); in mk_proof() 221 fact1 = to_app(m.get_fact(pr1)); in mk_proof() 232 mk_pp(m.get_fact(pr), m) << "\n";); in mk_proof()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_justification.cpp | 100 for (proof* p : prs) tout << mk_ll_pp(m.get_fact(p), m);); in mk_proof() 165 proof * pr2 = m.mk_rewrite(m.get_fact(pr1), lit); in mk_proof() 206 app* fact1 = to_app(m.get_fact(pr1)); in mk_proof() 207 app* fact2 = to_app(m.get_fact(pr2)); in mk_proof() 211 fact1 = to_app(m.get_fact(pr1)); in mk_proof() 221 fact1 = to_app(m.get_fact(pr1)); in mk_proof() 232 mk_pp(m.get_fact(pr), m) << "\n";); in mk_proof()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/macros/ |
H A D | macro_manager.cpp | 146 SASSERT(m.get_fact(pr) == q); in insert() 373 SASSERT(!old_pr || m.get_fact(old_pr) == old_n); in expand_macros() 384 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros() 393 SASSERT(!new_pr || m.get_fact(new_pr) == r); 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_manager.cpp | 146 SASSERT(m.get_fact(pr) == q); in insert() 363 SASSERT(!old_pr || m.get_fact(old_pr) == old_n); in expand_macros() 374 SASSERT(!new_pr || m.get_fact(new_pr) == r); in expand_macros() 383 SASSERT(!new_pr || m.get_fact(new_pr) == r); 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/muz/transforms/ |
H A D | dl_mk_coi_filter.cpp | 51 bool reachable = engine.get_fact(decl_i).is_reachable(); in bottom_up() 129 if (engine.get_fact(pred).is_reachable()) { in top_down()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/transforms/ |
H A D | dl_mk_coi_filter.cpp | 51 bool reachable = engine.get_fact(decl_i).is_reachable(); in bottom_up() 129 if (engine.get_fact(pred).is_reachable()) { in top_down()
|