Home
last modified time | relevance | path

Searched refs:get_fact (Results 1 – 25 of 99) sorted by relevance

1234

/dports/math/z3/z3-z3-4.8.13/src/ast/proofs/
H A Dproof_utils.cpp127 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 Dproof_utils.h80 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 Dproof_utils.cpp127 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 Dproof_utils.h80 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 Dspacer_proof_utils.cpp301 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 Dspacer_farkas_learner.cpp254 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 Dspacer_unsat_core_plugin.cpp74 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 Dspacer_proof_utils.cpp301 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 Dspacer_farkas_learner.cpp254 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 Dspacer_unsat_core_plugin.cpp74 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 Dast.cpp2737 …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 Dexpr_substitution.cpp69 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 Dast.cpp2815 …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 Dhnf.cpp226 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 Ddl_boogie_proof.cpp108 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 Dhnf.cpp227 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 Ddl_boogie_proof.cpp108 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 Ddl_base.cpp257 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 Ddl_base.cpp257 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 Dsmt_justification.cpp100 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 Dsmt_justification.cpp100 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 Dmacro_manager.cpp146 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 Dmacro_manager.cpp146 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 Ddl_mk_coi_filter.cpp51 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 Ddl_mk_coi_filter.cpp51 bool reachable = engine.get_fact(decl_i).is_reachable(); in bottom_up()
129 if (engine.get_fact(pred).is_reachable()) { in top_down()

1234