| /dports/devel/csmith/csmith-2.3.0/src/ |
| H A D | Fact.cpp | 138 if (new_fact->is_related(*facts[i])) { in find_related_fact()
166 if (f->is_related(*new_fact)) { in merge_fact()
167 if (!f->imply(*new_fact)) { in merge_fact()
168 Fact* copy_fact = new_fact->clone(); in merge_fact()
181 facts.push_back(new_fact); in merge_fact()
193 if (new_fact->equal(*facts[i])) { in renew_fact()
196 facts[i] = new_fact; in renew_fact()
202 facts.push_back(new_fact); in renew_fact()
254 const Fact* new_fact = facts2[i]; in combine_facts() local
257 if (old_fact->is_related(*new_fact)) { in combine_facts()
[all …]
|
| H A D | Fact.h | 117 const Fact* find_related_fact(const FactVec& facts, const Fact* new_fact);
118 const Fact* find_related_fact(const vector<Fact*>& facts, const Fact* new_fact);
121 bool merge_fact(FactVec& facts, const Fact* new_fact);
133 bool renew_fact(FactVec& facts, const Fact* new_fact);
|
| H A D | FactMgr.cpp | 172 FactPointTo* new_fact = f->mark_dead_var(var); in update_facts_for_oos_vars() local
173 if (new_fact) { in update_facts_for_oos_vars()
174 facts[j] = new_fact; in update_facts_for_oos_vars()
208 FactPointTo* new_fact = f->mark_func_end(stm); in remove_function_local_facts() local
209 if (new_fact) { in remove_function_local_facts()
210 inputs[i] = new_fact; in remove_function_local_facts()
|
| /dports/devel/p5-Data-Remember/Data-Remember-0.140490/lib/Data/Remember/ |
| H A D | Class.pm | 194 my @new_fact
196 $brain->remember($clean_que, \@new_fact);
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_subtheory_algebraic.cpp | 524 Node new_fact = nm->mkNode(kind::EQUAL, new_left, new_right); in solve() local
525 bool changed = subst.addSubstitution(fact, new_fact, reason); in solve()
559 Node new_fact = nm->mkNode(kind::EQUAL, zero, new_left); in solve() local
560 bool changed = subst.addSubstitution(fact, new_fact, reason); in solve()
571 Node new_fact = nm->mkNode(kind::EQUAL, zero, new_right); in solve() local
572 bool changed = subst.addSubstitution(fact, new_fact, reason); in solve()
581 Node new_fact = nm->mkNode(kind::EQUAL, left[0], left[1]); in solve() local
582 bool changed = subst.addSubstitution(fact, new_fact, reason); in solve()
|
| /dports/lang/ghc/ghc-8.10.7/compiler/cmm/Hoopl/ |
| H A D | Dataflow.hs | 334 updateFact fact_join dep_blocks (todo, fbase) lbl new_fact
338 let !z = mapInsert lbl new_fact fbase in (changed, z)
340 case fact_join (OldFact old_fact) (NewFact new_fact) of
|
| /dports/irc/py-limnoria/Limnoria-master-2019-09-08/plugins/MoobotFactoids/ |
| H A D | plugin.py | 414 new_fact = r(fact)
415 self.db.updateFactoid(channel, key, new_fact, id)
430 new_fact = format(_('%s, or %s'), fact, new_text)
431 self.db.updateFactoid(channel, key, new_fact, id)
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/proofs/ |
| H A D | proof_utils.cpp | 282 expr_ref new_fact(m); in mk_unit_resolution_core() local
283 new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.data()); in mk_unit_resolution_core()
286 proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.data(), new_fact); in mk_unit_resolution_core()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/proofs/ |
| H A D | proof_utils.cpp | 282 expr_ref new_fact(m); in mk_unit_resolution_core() local
283 new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.c_ptr()); in mk_unit_resolution_core()
286 proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), new_fact); in mk_unit_resolution_core()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | ast.cpp | 3079 …f * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact) { in mk_unit_resolution() argument
3083 tout << mk_pp(new_fact, *this) << "\n";); in mk_unit_resolution()
3087 args.push_back(new_fact); in mk_unit_resolution()
3092 SASSERT(is_false(new_fact)); in mk_unit_resolution()
3098 … CTRACE("unit_bug", !(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))), in mk_unit_resolution()
3101 tout << mk_pp(new_fact, *this) << "\n";); in mk_unit_resolution()
3117 …CTRACE("unit_bug", new_fact != lit, tout << mk_pp(f1, *this) << "\n" << mk_ll_pp(new_fact, *this) … in mk_unit_resolution()
3118 SASSERT(new_fact == lit); in mk_unit_resolution()
3123 SASSERT(num_matches != cls_sz || is_false(new_fact)); in mk_unit_resolution()
|
| H A D | ast.h | 2319 proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | ast.cpp | 3157 …f * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact) { in mk_unit_resolution() argument
3161 tout << mk_pp(new_fact, *this) << "\n";); in mk_unit_resolution()
3165 args.push_back(new_fact); in mk_unit_resolution()
3170 SASSERT(is_false(new_fact)); in mk_unit_resolution()
3176 … CTRACE("unit_bug", !(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))), in mk_unit_resolution()
3179 tout << mk_pp(new_fact, *this) << "\n";); in mk_unit_resolution()
3195 …CTRACE("unit_bug", new_fact != lit, tout << mk_pp(f1, *this) << "\n" << mk_ll_pp(new_fact, *this) … in mk_unit_resolution()
3196 SASSERT(new_fact == lit); in mk_unit_resolution()
3201 SASSERT(num_matches != cls_sz || is_false(new_fact)); in mk_unit_resolution()
|
| H A D | ast.h | 2379 proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact);
|