| /dports/math/z3/z3-z3-4.8.13/src/sat/ |
| H A D | sat_ddfw.cpp | 243 clause const& c = get_clause(cls_idx); in flip()
266 clause const& c = get_clause(cls_idx); in flip()
322 clause const& c = get_clause(i); in init_clause_data()
465 clause const& c = get_clause(cf_idx); in select_max_same_sign()
504 for (literal lit : get_clause(cf_idx)) { in shift_weights()
517 out << get_clause(i) << " "; in display()
537 for (literal lit : get_clause(cl)) { in invariant()
570 for (literal lit : get_clause(i)) { in invariant()
577 for (literal lit : get_clause(cl)) { in invariant()
|
| H A D | sat_clause.h | 145 clause * get_clause(clause_offset cls_off) const;
180 clause * get_clause() const { SASSERT(!is_binary()); return m_cls; } in get_clause() function
181 bool was_removed() const { return !is_binary() && get_clause()->was_removed(); } in was_removed()
182 bool is_learned() const { return !is_binary() && get_clause()->is_learned(); } in is_learned()
|
| H A D | sat_clause.cpp | 167 clause * clause_allocator::get_clause(clause_offset cls_off) const { in get_clause() function in sat::clause_allocator
247 out << c.get_clause()->id() << ": " << *c.get_clause(); in operator <<()
|
| H A D | sat_solver.h | 607 clause& get_clause(watch_list::iterator it) const { in get_clause() function
609 return get_clause(it->get_clause_offset()); in get_clause()
612 clause& get_clause(watched const& w) const { in get_clause() function
614 return get_clause(w.get_clause_offset()); in get_clause()
617 clause& get_clause(justification const& j) const { in get_clause() function
619 return get_clause(j.get_clause_offset()); in get_clause()
622 clause& get_clause(clause_offset cls_off) const { in get_clause() function
623 return *(cls_allocator().get_clause(cls_off)); in get_clause()
|
| H A D | sat_prob.cpp | 57 clause const& c = get_clause(cls_idx); in pick_var()
179 clause const& c = get_clause(i); in init_clauses()
287 out << get_clause(i) << " "; in display()
|
| H A D | sat_gc.cpp | 210 return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; in can_delete()
381 to_gc.push_back(cw.get_clause()); in gc_reinit_stack()
525 cw.get_clause()->set_removed(true);
531 cw.get_clause()->set_removed(true);
601 else if (w.is_clause() && !get_clause(w).was_removed())
|
| H A D | sat_integrity_checker.cpp | 178 VERIFY(!s.get_clause(w.get_clause_offset()).was_removed()); in check_watches()
205 SASSERT(c.is_binary() || c.get_clause()->on_reinit_stack()); in check_reinit_stack()
206 VERIFY(c.is_binary() || c.get_clause()->on_reinit_stack()); in check_reinit_stack()
|
| H A D | sat_prob.h | 90 inline clause const& get_clause(unsigned idx) const { return *m_clause_db[idx]; } in get_clause() function
|
| H A D | sat_watched.cpp | 125 … out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")"; in display_watch_list()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_ddfw.cpp | 243 clause const& c = get_clause(cls_idx); in flip()
266 clause const& c = get_clause(cls_idx); in flip()
322 clause const& c = get_clause(i); in init_clause_data()
465 clause const& c = get_clause(cf_idx); in select_max_same_sign()
504 for (literal lit : get_clause(cf_idx)) { in shift_weights()
517 out << get_clause(i) << " "; in display()
537 for (literal lit : get_clause(cl)) { in invariant()
570 for (literal lit : get_clause(i)) { in invariant()
577 for (literal lit : get_clause(cl)) { in invariant()
|
| H A D | sat_clause.h | 145 clause * get_clause(clause_offset cls_off) const;
180 clause * get_clause() const { SASSERT(!is_binary()); return m_cls; } in get_clause() function
181 bool was_removed() const { return !is_binary() && get_clause()->was_removed(); } in was_removed()
182 bool is_learned() const { return !is_binary() && get_clause()->is_learned(); } in is_learned()
|
| H A D | sat_clause.cpp | 167 clause * clause_allocator::get_clause(clause_offset cls_off) const { in get_clause() function in sat::clause_allocator
247 out << c.get_clause()->id() << ": " << *c.get_clause(); in operator <<()
|
| H A D | sat_solver.h | 565 clause& get_clause(watch_list::iterator it) const { in get_clause() function
567 return get_clause(it->get_clause_offset()); in get_clause()
570 clause& get_clause(watched const& w) const { in get_clause() function
572 return get_clause(w.get_clause_offset()); in get_clause()
575 clause& get_clause(justification const& j) const { in get_clause() function
577 return get_clause(j.get_clause_offset()); in get_clause()
580 clause& get_clause(clause_offset cls_off) const { in get_clause() function
581 return *(cls_allocator().get_clause(cls_off)); in get_clause()
|
| H A D | sat_prob.cpp | 57 clause const& c = get_clause(cls_idx); in pick_var()
179 clause const& c = get_clause(i); in init_clauses()
287 out << get_clause(i) << " "; in display()
|
| H A D | sat_gc.cpp | 210 return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; in can_delete()
381 to_gc.push_back(cw.get_clause()); in gc_reinit_stack()
525 cw.get_clause()->set_removed(true);
531 cw.get_clause()->set_removed(true);
601 else if (w.is_clause() && !get_clause(w).was_removed())
|
| H A D | sat_integrity_checker.cpp | 178 VERIFY(!s.get_clause(w.get_clause_offset()).was_removed()); in check_watches()
205 SASSERT(c.is_binary() || c.get_clause()->on_reinit_stack()); in check_reinit_stack()
206 VERIFY(c.is_binary() || c.get_clause()->on_reinit_stack()); in check_reinit_stack()
|
| H A D | sat_prob.h | 91 inline clause const& get_clause(unsigned idx) const { return *m_clause_db[idx]; } in get_clause() function
|
| H A D | sat_watched.cpp | 125 … out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")"; in display_watch_list()
|
| /dports/textproc/zorba/zorba-2.7.0/src/compiler/rewriter/rules/ |
| H A D | flwor_rules.cpp | 234 flwor_clause* clause = flwor.get_clause(i); in RULE_REWRITE_PRE()
281 flwor_clause* c = flwor.get_clause(i); in RULE_REWRITE_PRE()
469 flwor_clause* clause = flwor.get_clause(0); in RULE_REWRITE_PRE()
611 const flwor_clause& c = *flwor.get_clause(i); in collect_flw_vars()
759 const flwor_clause* clause = flwor.get_clause(i); in safe_to_fold_single_use()
1052 const flwor_clause* c = flwor.get_clause(i); in var_in_try_or_loop()
1402 flwor_clause* clause = flwor->get_clause(clausePos); in RULE_REWRITE_PRE()
1836 const flwor_clause* c = flwor->get_clause(i); in RULE_REWRITE_PRE()
1851 const flwor_clause* c = returnFlwor->get_clause(i); in RULE_REWRITE_PRE()
1862 flwor->add_clause(returnFlwor->get_clause(i)); in RULE_REWRITE_PRE()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_b_justification.h | 61 clause * get_clause() const { in get_clause() function
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_b_justification.h | 61 clause * get_clause() const { in get_clause() function
|
| /dports/devel/libdap/libdap-3.20.8/ |
| H A D | D4FilterClause.h | 75 D4FilterClause *get_clause(unsigned int i) { in get_clause() function
|
| /dports/misc/otter/otter-3.3f/mace2/ |
| H A D | part.c | 361 struct clause *n1 = get_clause(); in try_to_part()
362 struct clause *n2 = get_clause(); in try_to_part()
|
| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_justification.h | 77 clause * get_clause() const { return UNTAG(clause*, m_data); } in get_clause() function
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_justification.h | 77 clause * get_clause() const { return UNTAG(clause*, m_data); } in get_clause() function
|