| /dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
| H A D | sat_th.cpp | 232 …th_explain::th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const… in th_explain() argument
235 m_num_literals = n_lits; in th_explain()
238 for (unsigned i = 0; i < n_lits; ++i) in th_explain()
240 …t_cast<enode_pair*>(reinterpret_cast<char*>(this) + sizeof(th_explain) + sizeof(literal) * n_lits); in th_explain()
246 …th_explain* th_explain::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned … in mk() argument
248 void* mem = r.allocate(get_obj_size(n_lits, n_eqs)); in mk()
250 …return new (sat::constraint_base::ptr2mem(mem)) th_explain(n_lits, lits, n_eqs, eqs, c, enode_pair… in mk()
269 …th_explain* th_explain::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, uns… in conflict() argument
270 return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr); in conflict()
|
| H A D | sat_th.h | 210 …th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::…
211 …static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs…
216 …static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned…
|
| /dports/lang/fpc-utils/fpc-3.2.2/utils/tply/ |
| H A D | yacctabl.pas | 95 n_lits : Integer;
438 inc(n_lits);
439 if n_lits>max_lits then fatal(lit_table_overflow);
440 sym_type^[n_lits-1] := 0;
441 sym_prec^[n_lits-1] := 0;
442 new_lit := n_lits-1;
447 if sym>n_lits then n_lits := sym;
448 if n_lits>max_lits then fatal(lit_table_overflow);
918 n_lits := 257;
|
| /dports/lang/fpc-source/fpc-3.2.2/utils/tply/ |
| H A D | yacctabl.pas | 95 n_lits : Integer;
438 inc(n_lits);
439 if n_lits>max_lits then fatal(lit_table_overflow);
440 sym_type^[n_lits-1] := 0;
441 sym_prec^[n_lits-1] := 0;
442 new_lit := n_lits-1;
447 if sym>n_lits then n_lits := sym;
448 if n_lits>max_lits then fatal(lit_table_overflow);
918 n_lits := 257;
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | sat_th.cpp | 232 …th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pa… in th_propagation() argument
233 m_num_literals = n_lits; in th_propagation()
236 for (unsigned i = 0; i < n_lits; ++i) in th_propagation()
238 …st<enode_pair*>(reinterpret_cast<char*>(this) + sizeof(th_propagation) + sizeof(literal) * n_lits); in th_propagation()
247 …th_propagation* th_propagation::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, u… in mk() argument
249 void* mem = r.allocate(get_obj_size(n_lits, n_eqs)); in mk()
251 return new (sat::constraint_base::ptr2mem(mem)) th_propagation(n_lits, lits, n_eqs, eqs); in mk()
|
| H A D | sat_th.h | 201 … th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
204 …static th_propagation* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n…
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | xchaff_solver.cpp | 181 int n_lits = lits.size(); in add_clause() local
183 while (lit_pool_free_space() <= n_lits + 1) { in add_clause()
198 clause(new_cl).init(lit_pool_end(), n_lits); in add_clause()
203 for (int i=0; i< n_lits; ++i){ in add_clause()
222 assert(_stats.is_solver_started || num_unknown == n_lits); in add_clause()
282 CDatabase::_stats.num_added_literals += n_lits; in add_clause()
284 if (n_lits == 1) _addedUnitClauses.push_back(new_cl); in add_clause()
|
| /dports/math/spot/spot-2.10.2/spot/twaalgos/ |
| H A D | mealy_machine.cc | 2275 unsigned n_lits() const in n_lits() function
3337 dotimeprint << "n literals " << mm_pb.n_lits() in try_build_min_machine()
|
| /dports/math/py-spot/spot-2.10.2/spot/twaalgos/ |
| H A D | mealy_machine.cc | 2275 unsigned n_lits() const in n_lits() function
3337 dotimeprint << "n literals " << mm_pb.n_lits() in try_build_min_machine()
|