| /dports/math/z3/z3-z3-4.8.13/src/sat/ |
| H A D | sat_clause_use_list.h | 30 clause_vector m_clauses; variable
56 SASSERT(!m_clauses.contains(&c)); in insert()
58 m_clauses.push_back(&c); in insert()
65 SASSERT(m_clauses.contains(&c)); in erase_not_removed()
67 m_clauses.erase(&c); in erase_not_removed()
74 SASSERT(m_clauses.contains(&c)); in erase()
93 m_clauses.finalize(); in reset()
102 clause_vector & m_clauses; variable
109 iterator(clause_vector & v):m_clauses(v), m_size(v.size()), m_i(0) { in iterator()
115 clause & curr() const { SASSERT(!at_end()); return *(m_clauses[m_i]); } in curr()
[all …]
|
| H A D | sat_clause_use_list.cpp | 26 for (clause* c : m_clauses) in check_invariant()
31 for (clause* c : m_clauses) in check_invariant()
43 if (!m_clauses[m_i]->was_removed()) { in consume()
44 m_clauses[m_j] = m_clauses[m_i]; in consume()
54 m_clauses.shrink(m_j); in ~iterator()
|
| H A D | sat_ddfw.cpp | 36 for (auto& ci : m_clauses) { in ~ddfw()
131 unsigned idx = m_clauses.size(); in add()
141 for (auto& ci : m_clauses) { in add()
144 m_clauses.reset(); in add()
166 for (clause* c : s.m_clauses) { in add()
293 for (auto& ci : m_clauses) { in do_reinit_weights()
298 for (auto& ci : m_clauses) { in do_reinit_weights()
319 unsigned sz = m_clauses.size(); in init_clause_data()
321 auto& ci = m_clauses[i]; in init_clause_data()
486 auto& cf = m_clauses[cf_idx]; in shift_weights()
[all …]
|
| H A D | sat_model_converter.cpp | 83 for (literal l : e.m_clauses) { in operator ()()
230 e.m_clauses.push_back(null_literal); in insert()
239 e.m_clauses.push_back(l1); in insert()
240 e.m_clauses.push_back(l2); in insert()
241 e.m_clauses.push_back(null_literal); in insert()
252 e.m_clauses.push_back(c[i]); in insert()
253 e.m_clauses.push_back(null_literal); in insert()
263 e.m_clauses.push_back(null_literal); in insert()
309 for (literal l : entry.m_clauses) { in display()
361 for (literal l : e.m_clauses) { in max_var()
[all …]
|
| H A D | sat_prob.cpp | 79 clause_info& ci = m_clauses[cls_idx]; in flip()
94 clause_info& ci = m_clauses[cls_idx]; in flip()
115 m_clauses.push_back(clause_info()); in add()
145 for (clause* c : s.m_clauses) { in add()
175 for (unsigned i = 0; i < m_clauses.size(); ++i) { in init_clauses()
176 clause_info& ci = m_clauses[i]; in init_clauses()
285 unsigned num_cls = m_clauses.size(); in display()
288 auto const& ci = m_clauses[i]; in display()
|
| H A D | sat_parallel.cpp | 206 if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) { in _from_solver()
209 …am() << "(sat-parallel refresh :from " << m_num_clauses << " :to " << s.m_clauses.size() << ")\n";… in _from_solver()
212 m_num_clauses = s.m_clauses.size(); in _from_solver()
269 if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) { in copy_solver()
272 m_num_clauses = s.m_clauses.size(); in copy_solver()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_clause_use_list.h | 30 clause_vector m_clauses; variable
56 SASSERT(!m_clauses.contains(&c)); in insert()
58 m_clauses.push_back(&c); in insert()
65 SASSERT(m_clauses.contains(&c)); in erase_not_removed()
67 m_clauses.erase(&c); in erase_not_removed()
74 SASSERT(m_clauses.contains(&c)); in erase()
93 m_clauses.finalize(); in reset()
102 clause_vector & m_clauses; variable
109 iterator(clause_vector & v):m_clauses(v), m_size(v.size()), m_i(0) { in iterator()
115 clause & curr() const { SASSERT(!at_end()); return *(m_clauses[m_i]); } in curr()
[all …]
|
| H A D | sat_clause_use_list.cpp | 26 for (clause* c : m_clauses) in check_invariant()
31 for (clause* c : m_clauses) in check_invariant()
43 if (!m_clauses[m_i]->was_removed()) { in consume()
44 m_clauses[m_j] = m_clauses[m_i]; in consume()
54 m_clauses.shrink(m_j); in ~iterator()
|
| H A D | sat_ddfw.cpp | 36 for (auto& ci : m_clauses) { in ~ddfw()
131 unsigned idx = m_clauses.size(); in add()
141 for (auto& ci : m_clauses) { in add()
144 m_clauses.reset(); in add()
166 for (clause* c : s.m_clauses) { in add()
293 for (auto& ci : m_clauses) { in do_reinit_weights()
298 for (auto& ci : m_clauses) { in do_reinit_weights()
319 unsigned sz = m_clauses.size(); in init_clause_data()
321 auto& ci = m_clauses[i]; in init_clause_data()
486 auto& cf = m_clauses[cf_idx]; in shift_weights()
[all …]
|
| H A D | sat_model_converter.cpp | 83 for (literal l : e.m_clauses) { in operator ()()
231 e.m_clauses.push_back(null_literal); in insert()
240 e.m_clauses.push_back(l1); in insert()
241 e.m_clauses.push_back(l2); in insert()
242 e.m_clauses.push_back(null_literal); in insert()
253 e.m_clauses.push_back(c[i]); in insert()
254 e.m_clauses.push_back(null_literal); in insert()
264 e.m_clauses.push_back(null_literal); in insert()
310 for (literal l : entry.m_clauses) { in display()
362 for (literal l : e.m_clauses) { in max_var()
[all …]
|
| H A D | sat_prob.cpp | 79 clause_info& ci = m_clauses[cls_idx]; in flip()
94 clause_info& ci = m_clauses[cls_idx]; in flip()
115 m_clauses.push_back(clause_info()); in add()
145 for (clause* c : s.m_clauses) { in add()
175 for (unsigned i = 0; i < m_clauses.size(); ++i) { in init_clauses()
176 clause_info& ci = m_clauses[i]; in init_clauses()
285 unsigned num_cls = m_clauses.size(); in display()
288 auto const& ci = m_clauses[i]; in display()
|
| H A D | sat_parallel.cpp | 206 if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) { in _from_solver()
209 …am() << "(sat-parallel refresh :from " << m_num_clauses << " :to " << s.m_clauses.size() << ")\n";… in _from_solver()
212 m_num_clauses = s.m_clauses.size(); in _from_solver()
269 if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) { in copy_solver()
272 m_num_clauses = s.m_clauses.size(); in copy_solver()
|
| /dports/lang/mono/mono-5.10.1.57/mcs/class/referencesource/System.Data.Entity/System/Data/Mapping/ViewGeneration/Structures/ |
| H A D | CaseStatement.cs | 39 m_clauses = new List<WhenThen>(); in CaseStatement()
51 private List<WhenThen> m_clauses; field in System.Data.Mapping.ViewGeneration.Structures.CaseStatement
67 get { return m_clauses; }
84 foreach (WhenThen whenThen in m_clauses) in DeepQualify()
87 result.m_clauses.Add(newClause); in DeepQualify()
107 m_clauses.Add(new WhenThen(condition, value)); in AddWhenThen()
122 foreach (WhenThen whenThen in m_clauses)
138 foreach (WhenThen whenThen in m_clauses)
186 foreach (WhenThen clause in m_clauses) in Simplify()
219 m_clauses = clauses; in Simplify()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/opt/ |
| H A D | pb_sls.cpp | 137 m_clauses.reset(); in reset()
156 m_clauses.push_back(cls); in add()
277 display(out, m_clauses[i]); in display()
329 init_occ(m_clauses, m_hard_occ); in init()
334 if (!eval(m_clauses[i])) { in init()
468 clause& cls = m_clauses[j]; in flip()
565 m_clauses.push_back(cls); in mk_literal()
609 m_clauses.push_back(cls); in mk_literal()
614 m_clauses.push_back(cls); in mk_literal()
619 m_clauses.push_back(cls); in mk_literal()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/opt/ |
| H A D | pb_sls.cpp | 137 m_clauses.reset(); in reset()
156 m_clauses.push_back(cls); in add()
277 display(out, m_clauses[i]); in display()
329 init_occ(m_clauses, m_hard_occ); in init()
334 if (!eval(m_clauses[i])) { in init()
468 clause& cls = m_clauses[j]; in flip()
565 m_clauses.push_back(cls); in mk_literal()
609 m_clauses.push_back(cls); in mk_literal()
614 m_clauses.push_back(cls); in mk_literal()
619 m_clauses.push_back(cls); in mk_literal()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/tactic/ |
| H A D | unit_subsumption_tactic.cpp | 27 expr_ref_vector m_clauses; member
38 m_clauses(m) { in unit_subsumption_tactic()
94 expr_ref fml(mk_not(m, m_clauses.get(j)), m); in prune_clause()
98 m_context.assert_expr(m_clauses.get(j)); in prune_clause()
132 return new_bool(m_clause_count, m_clauses, "#clause"); in new_clause()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/tactic/ |
| H A D | unit_subsumption_tactic.cpp | 27 expr_ref_vector m_clauses; member
38 m_clauses(m) { in unit_subsumption_tactic()
94 expr_ref fml(mk_not(m, m_clauses.get(j)), m); in prune_clause()
98 m_context.assert_expr(m_clauses.get(j)); in prune_clause()
132 return new_bool(m_clause_count, m_clauses, "#clause"); in new_clause()
|
| /dports/math/z3/z3-z3-4.8.13/src/test/ |
| H A D | sorting_network.cpp | 148 expr_ref_vector m_clauses; member
177 m_clauses.push_back(mk_or(m, n, lits)); in mk_clause()
200 for (expr* cls : ext.m_clauses) { in test_eq1()
224 ext.m_clauses.reset(); in test_eq1()
247 for (expr* cl : ext.m_clauses) { in test_sorting_eq()
281 ext.m_clauses.reset(); in test_sorting_eq()
302 for (expr* cls : ext.m_clauses) { in test_sorting_le()
338 ext.m_clauses.reset(); in test_sorting_le()
360 for (expr* cls : ext.m_clauses) { in test_sorting_ge()
429 for (expr* cls : ext.m_clauses) { in test_at_most_1()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
| H A D | sorting_network.cpp | 148 expr_ref_vector m_clauses; member
177 m_clauses.push_back(mk_or(m, n, lits)); in mk_clause()
200 for (expr* cls : ext.m_clauses) { in test_eq1()
224 ext.m_clauses.reset(); in test_eq1()
247 for (expr* cl : ext.m_clauses) { in test_sorting_eq()
281 ext.m_clauses.reset(); in test_sorting_eq()
302 for (expr* cls : ext.m_clauses) { in test_sorting_le()
338 ext.m_clauses.reset(); in test_sorting_le()
360 for (expr* cls : ext.m_clauses) { in test_sorting_ge()
429 for (expr* cls : ext.m_clauses) { in test_at_most_1()
[all …]
|
| /dports/lang/gcc12-devel/gcc-12-20211205/gcc/cp/ |
| H A D | logic.cc | 226 m_clauses.emplace_back (t); in formula()
227 m_current = m_clauses.begin (); in formula()
249 return *m_clauses.insert (std::next (m_current), *m_current); in branch()
263 return m_clauses.begin (); in begin()
270 return m_clauses.begin (); in begin()
277 return m_clauses.end (); in end()
284 return m_clauses.end (); in end()
292 m_clauses.erase (i); in erase()
295 std::list<clause> m_clauses; /* The list of clauses. */ member
|
| /dports/lang/gcc11-devel/gcc-11-20211009/gcc/cp/ |
| H A D | logic.cc | 226 m_clauses.emplace_back (t); in formula()
227 m_current = m_clauses.begin (); in formula()
249 return *m_clauses.insert (std::next (m_current), *m_current); in branch()
263 return m_clauses.begin (); in begin()
270 return m_clauses.begin (); in begin()
277 return m_clauses.end (); in end()
284 return m_clauses.end (); in end()
292 m_clauses.erase (i); in erase()
295 std::list<clause> m_clauses; /* The list of clauses. */ member
|
| /dports/lang/solidity/solidity_0.8.11/libsolidity/ast/ |
| H A D | AST.cpp | 970 solAssert(m_clauses.size() > 0, ""); in successClause()
971 return m_clauses[0].get(); in successClause()
976 for (size_t i = 1; i < m_clauses.size(); ++i) in panicClause()
977 if (m_clauses[i]->errorName() == "Panic") in panicClause()
978 return m_clauses[i].get(); in panicClause()
984 for (size_t i = 1; i < m_clauses.size(); ++i) in errorClause()
985 if (m_clauses[i]->errorName() == "Error") in errorClause()
986 return m_clauses[i].get(); in errorClause()
992 for (size_t i = 1; i < m_clauses.size(); ++i) in fallbackClause()
993 if (m_clauses[i]->errorName().empty()) in fallbackClause()
[all …]
|
| /dports/devel/avr-gcc/gcc-10.2.0/gcc/cp/ |
| H A D | logic.cc | 243 m_clauses.push_back (t); in formula()
244 m_current = m_clauses.begin (); in formula()
266 m_clauses.push_back (*m_current); in branch()
267 return m_clauses.back (); in branch()
281 return m_clauses.begin (); in begin()
288 return m_clauses.begin (); in begin()
295 return m_clauses.end (); in end()
302 return m_clauses.end (); in end()
305 std::list<clause> m_clauses; /* The list of clauses. */ member
|
| /dports/lang/gcc10-devel/gcc-10-20211008/gcc/cp/ |
| H A D | logic.cc | 243 m_clauses.push_back (t); in formula()
244 m_current = m_clauses.begin (); in formula()
266 m_clauses.push_back (*m_current); in branch()
267 return m_clauses.back (); in branch()
281 return m_clauses.begin (); in begin()
288 return m_clauses.begin (); in begin()
295 return m_clauses.end (); in end()
302 return m_clauses.end (); in end()
305 std::list<clause> m_clauses; /* The list of clauses. */ member
|
| /dports/misc/cxx_atomics_pic/gcc-11.2.0/gcc/cp/ |
| H A D | logic.cc | 228 m_clauses.push_back (t); in formula()
229 m_current = m_clauses.begin (); in formula()
251 m_clauses.push_back (*m_current); in branch()
252 return m_clauses.back (); in branch()
266 return m_clauses.begin (); in begin()
273 return m_clauses.begin (); in begin()
280 return m_clauses.end (); in end()
287 return m_clauses.end (); in end()
290 std::list<clause> m_clauses; /* The list of clauses. */ member
|