/dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
H A D | SolverTypes.h | 139 unsigned learnt : 1; member 149 Clause(const V& ps, bool use_extra, bool learnt) { in Clause() argument 151 header.learnt = learnt; in Clause() 160 if (header.learnt) in Clause() 178 bool learnt () const { return header.learnt; } in learnt() function 226 CRef alloc(const Lits& ps, bool learnt = false) 230 bool use_extra = learnt | extra_clause_field; 233 new (lea(cid)) Clause(ps, use_extra, learnt); 257 cr = to.alloc(c, c.learnt()); in reloc() 390 …if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != … in subsumes() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | SolverTypes.h | 126 unsigned learnt : 1; member 136 Clause(const V& ps, bool use_extra, bool learnt) { in Clause() argument 138 header.learnt = learnt; in Clause() 147 if (header.learnt) in Clause() 165 bool learnt () const { return header.learnt; } in learnt() function 209 CRef alloc(const Lits& ps, bool learnt = false) 213 bool use_extra = learnt | extra_clause_field; 216 new (lea(cid)) Clause(ps, use_extra, learnt); 240 cr = to.alloc(c, c.learnt()); in reloc() 246 if (to[cr].learnt()) to[cr].activity() = c.activity(); in reloc() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
H A D | SolverTypes.h | 135 unsigned learnt : 1; member 150 Clause(const V& ps, bool use_extra, bool learnt) { in Clause() argument 152 header.learnt = learnt; in Clause() 162 if (header.learnt) in Clause() 180 bool learnt () const { return header.learnt; } in learnt() function 232 CRef alloc(const Lits& ps, bool learnt = false) 236 bool use_extra = learnt | extra_clause_field; 239 new (lea(cid)) Clause(ps, use_extra, learnt); 263 cr = to.alloc(c, c.learnt()); in reloc() 269 if (to[cr].learnt()) { in reloc() [all …]
|
/dports/math/glucose/glucose-syrup-4.1/core/ |
H A D | SolverTypes.h | 163 unsigned learnt : 1; member 185 Clause(const V& ps, int _extra_size, bool learnt) { in Clause() argument 188 header.learnt = learnt; in Clause() 201 if (header.learnt) in Clause() 229 bool learnt () const { return header.learnt; } in learnt() function 230 void nolearnt () { header.learnt = false;} in nolearnt() 300 bool use_extra = learnt | extra_clause_field; 303 new (lea(cid)) Clause(ps, extra_size, learnt); 327 cr = to.alloc(c, c.learnt(), c.wasImported()); in reloc() 333 if (to[cr].learnt()) { in reloc() [all …]
|
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | SolverTypes.h | 115 Clause(const V& ps, bool learnt) { in Clause() argument 116 size_etc = (ps.size() << 3) | (uint32_t)learnt; in Clause() 118 if (learnt) extra.act = 0; else calcAbstraction(); } in Clause() 122 friend Clause* Clause_new(const V& ps, bool learnt); 127 bool learnt () const { return size_etc & 1; } in learnt() function 147 Clause* Clause_new(const V& ps, bool learnt) { in Clause_new() argument 151 return new (mem) Clause(ps, learnt); } in Clause_new()
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
H A D | sat-types.h | 80 unsigned int learnt : 1; // is it a learnt clause 91 Clause(const V& ps, bool learnt) { in Clause() argument 95 this->learnt = learnt; in Clause() 111 if (learnt) { in resize() 131 static Clause* Clause_new(const V& ps, bool learnt = false) { 132 int mem_size = sizeof(Clause) + ps.size() * sizeof(Lit) + (learnt ? 3 : 0) * sizeof(int); 134 Clause* newClause = new (mem) Clause(ps, learnt);
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
H A D | SolverTypes.h | 149 unsigned learnt : 1; member 159 Clause(const V& ps, bool use_extra, bool learnt) { in Clause() argument 161 header.learnt = learnt; in Clause() 170 if (header.learnt) in Clause() 188 bool learnt () const { return header.learnt; } in learnt() function 234 CRef alloc(const Lits& ps, bool learnt = false) 238 bool use_extra = learnt | extra_clause_field; 241 new (lea(cid)) Clause(ps, use_extra, learnt); 384 assert(!header.learnt); assert(!other.header.learnt); in subsumes()
|
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
H A D | SolverTypes.h | 143 unsigned learnt : 1; member 152 Clause(const vec<Lit>& ps, bool use_extra, bool learnt) { in Clause() argument 154 header.learnt = learnt; in Clause() 163 if (header.learnt) in Clause() 179 if (header.learnt) in Clause() 198 bool learnt () const { return header.learnt; } in learnt() function 245 CRef alloc(const vec<Lit>& ps, bool learnt = false) 249 bool use_extra = learnt | extra_clause_field; 251 new (lea(cid)) Clause(ps, use_extra, learnt); 258 bool use_extra = from.learnt() | extra_clause_field; in alloc() [all …]
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | SolverTypes.h | 143 unsigned learnt : 1; member 152 Clause(const vec<Lit>& ps, bool use_extra, bool learnt) { in Clause() argument 154 header.learnt = learnt; in Clause() 163 if (header.learnt) in Clause() 179 if (header.learnt) in Clause() 198 bool learnt () const { return header.learnt; } in learnt() function 245 CRef alloc(const vec<Lit>& ps, bool learnt = false) 249 bool use_extra = learnt | extra_clause_field; 251 new (lea(cid)) Clause(ps, use_extra, learnt); 258 bool use_extra = from.learnt() | extra_clause_field; in alloc() [all …]
|
/dports/math/vampire/vampire-4.5.1/Minisat/core/ |
H A D | SolverTypes.h | 148 unsigned learnt : 1; member 157 Clause(const vec<Lit>& ps, bool use_extra, bool learnt) { in Clause() argument 159 header.learnt = learnt; in Clause() 168 if (header.learnt) in Clause() 184 if (header.learnt) in Clause() 203 bool learnt () const { return header.learnt; } in learnt() function 264 CRef alloc(const vec<Lit>& ps, bool learnt = false) 268 bool use_extra = learnt | extra_clause_field; 270 new (lea(cid)) Clause(ps, use_extra, learnt); 277 bool use_extra = from.learnt() | extra_clause_field; in alloc() [all …]
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/mpi/ |
H A D | DataSync.cpp | 387 void DataSync::signalNewBinClause(const T& ps, const bool learnt) in signalNewBinClause() argument 390 signalNewBinClause(ps[0], ps[1], learnt); in signalNewBinClause() 396 void DataSync::signalNewBinClause(Lit lit1, Lit lit2, const bool learnt) in signalNewBinClause() argument 399 newBinClauses.push_back(BinClause(lit1, lit2, learnt)); in signalNewBinClause() 403 void DataSync::signalNewTriClause(const T& ps, const bool learnt) in signalNewTriClause() argument 406 signalNewTriClause(ps[0], ps[1], ps[2], learnt); in signalNewTriClause() 511 Clause* c = solver.addClauseInt(tmp, 0, cl.learnt, 3, true); in syncTriFromOthers() 581 solver.addClauseInt(lits, 0, bins[i].learnt, 2, true); in syncBinFromOthers() 599 addOneBinToOthers(it->lit1, it->lit2, it->learnt); in syncBinToOthers() 616 if (it->lit2 == lit2 && it->learnt == learnt) return; in addOneBinToOthers() [all …]
|
H A D | DataSync.h | 41 template <class T> void signalNewBinClause(const T& ps, const bool learnt = true); 42 void signalNewBinClause(Lit lit1, Lit lit2, const bool learnt = true); 43 template <class T> void signalNewTriClause(const T& ps, const bool learnt = true); 44 … void signalNewTriClause(const Lit lit1, const Lit lit2, const Lit lit3, const bool learnt = true);
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/mpi/ |
H A D | DataSync.cpp | 387 void DataSync::signalNewBinClause(const T& ps, const bool learnt) in signalNewBinClause() argument 390 signalNewBinClause(ps[0], ps[1], learnt); in signalNewBinClause() 396 void DataSync::signalNewBinClause(Lit lit1, Lit lit2, const bool learnt) in signalNewBinClause() argument 399 newBinClauses.push_back(BinClause(lit1, lit2, learnt)); in signalNewBinClause() 403 void DataSync::signalNewTriClause(const T& ps, const bool learnt) in signalNewTriClause() argument 406 signalNewTriClause(ps[0], ps[1], ps[2], learnt); in signalNewTriClause() 511 Clause* c = solver.addClauseInt(tmp, 0, cl.learnt, 3, true); in syncTriFromOthers() 581 solver.addClauseInt(lits, 0, bins[i].learnt, 2, true); in syncBinFromOthers() 599 addOneBinToOthers(it->lit1, it->lit2, it->learnt); in syncBinToOthers() 616 if (it->lit2 == lit2 && it->learnt == learnt) return; in addOneBinToOthers() [all …]
|
H A D | DataSync.h | 41 template <class T> void signalNewBinClause(const T& ps, const bool learnt = true); 42 void signalNewBinClause(Lit lit1, Lit lit2, const bool learnt = true); 43 template <class T> void signalNewTriClause(const T& ps, const bool learnt = true); 44 … void signalNewTriClause(const Lit lit1, const Lit lit2, const Lit lit3, const bool learnt = true);
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | minisat_types.h | 119 Clause(bool learnt, const std::vector<Lit>& ps, CVC3::Theorem theorem, in Clause() argument 121 d_size_learnt = (ps.size() << 1) | (int)learnt; in Clause() 134 bool learnt () const { return d_size_learnt & 1; } in learnt() function 145 DebugAssert(learnt(), "MiniSat::Types:activity: not a lemma"); in activity() 149 DebugAssert(learnt(), "MiniSat::Types:setActivity: not a lemma"); in setActivity()
|
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
H A D | SolverTypes.h | 143 unsigned learnt : 1; member 154 header.learnt = learnt_; in Clause() 163 if (header.learnt) in Clause() 179 if (header.learnt) in Clause() 198 bool learnt () const { return header.learnt; } in learnt() function 245 CRef alloc(const vec<Lit>& ps, bool learnt = false) 249 bool use_extra = learnt | extra_clause_field; 251 new (lea(cid)) Clause(ps, use_extra, learnt); 258 bool use_extra = from.learnt() | extra_clause_field; in alloc() 442 assert(!header.learnt); assert(!other.header.learnt); in subsumes()
|
/dports/math/chuffed/chuffed-e04bedd/ |
H A D | chuffed.msc.in | 25 ["--n-of-learnts", "The maximal number of learnt clauses", "int", "100000"], 26 … ["--learnts-mlimit", "The maximal memory limit for learnt clauses in Bytes", "int", "500000000"], 27 …["--sort-learnt-level", "Sort literals in a learnt clause based on their decision level", "bool", … 29 ["--bin-clause-opt", "Optimise learnt clauses of length 2", "bool:on:off", "true"], 32 ["--exclude-introduced", "Exclude introduced variables from learnt clauses", "bool", "false"],
|
/dports/math/igraph/igraph-0.9.5/vendor/glpk/minisat/ |
H A D | minisat.c | 343 assert(learnt >= 0 && learnt < 2); in clause_new() 347 c->size_learnt = (size << 1) | learnt; in clause_new() 358 if (learnt) in clause_new() 656 veci_push(learnt,lit_Undef); in solver_analyze() 671 veci_push(learnt,q); in solver_analyze() 691 veci_push(learnt,q); in solver_analyze() 704 *veci_begin(learnt) = lit_neg(p); in solver_analyze() 706 lits = veci_begin(learnt); in solver_analyze() 722 veci_resize(learnt,j); in solver_analyze() 738 for (i = 0; i < veci_size(learnt); i++) in solver_analyze() [all …]
|
/dports/math/glpk/glpk-5.0/src/minisat/ |
H A D | minisat.c | 343 assert(learnt >= 0 && learnt < 2); in clause_new() 347 c->size_learnt = (size << 1) | learnt; in clause_new() 358 if (learnt) in clause_new() 656 veci_push(learnt,lit_Undef); in solver_analyze() 671 veci_push(learnt,q); in solver_analyze() 691 veci_push(learnt,q); in solver_analyze() 704 *veci_begin(learnt) = lit_neg(p); in solver_analyze() 706 lits = veci_begin(learnt); in solver_analyze() 722 veci_resize(learnt,j); in solver_analyze() 738 for (i = 0; i < veci_size(learnt); i++) in solver_analyze() [all …]
|
/dports/net-mgmt/netdisco-mibs/netdisco-mibs-4.010/3com/ |
H A D | a3com-huawei-mac-information.mib | 99 "The number of MAC addresses that learnt by the device since the 145 as soon as there is a MAC address learnt or removed." 202 will cache the MAC address information that learnt on the interface." 240 MAC address information learnt or removed. The object is valid 273 "This object is the MAC information that learnt or removed 282 1 - MAC learnt. 304 address is learnt or removed and has size of 2 octets." 327 MAC address information learnt or removed. The object is valid 368 "This object is the MAC information that learnt or removed 377 1 - MAC learnt. [all …]
|
/dports/net-mgmt/netdisco-mibs/netdisco-mibs-4.010/h3c/ |
H A D | hh3c-mac-information.mib | 99 "The number of MAC addresses that learnt by the device since the 145 as soon as there is a MAC address learnt or removed." 202 will cache the MAC address information that learnt on the interface." 240 MAC address information learnt or removed. The object is valid 273 "This object is the MAC information that learnt or removed 282 1 - MAC learnt. 304 address is learnt or removed and has size of 2 octets." 327 MAC address information learnt or removed. The object is valid 368 "This object is the MAC information that learnt or removed 377 1 - MAC learnt. [all …]
|
/dports/net-mgmt/netdisco-mibs/netdisco-mibs-4.010/huawei/ |
H A D | h3c-mac-information.mib | 99 "The number of MAC addresses that learnt by the device since the 145 as soon as there is a MAC address learnt or removed." 202 will cache the MAC address information that learnt on the interface." 240 MAC address information learnt or removed. The object is valid 273 "This object is the MAC information that learnt or removed 282 1 - MAC learnt. 304 address is learnt or removed and has size of 2 octets." 327 MAC address information learnt or removed. The object is valid 368 "This object is the MAC information that learnt or removed 377 1 - MAC learnt. [all …]
|
/dports/net-mgmt/observium/observium/mibs/a3com/ |
H A D | A3COM-HUAWEI-MAC-INFORMATION-MIB | 99 "The number of MAC addresses that learnt by the device since the 145 as soon as there is a MAC address learnt or removed." 202 will cache the MAC address information that learnt on the interface." 240 MAC address information learnt or removed. The object is valid 273 "This object is the MAC information that learnt or removed 282 1 - MAC learnt. 304 address is learnt or removed and has size of 2 octets." 327 MAC address information learnt or removed. The object is valid 368 "This object is the MAC information that learnt or removed 377 1 - MAC learnt. [all …]
|
/dports/math/vampire/vampire-4.5.1/SAT/ |
H A D | TWLSolver.cpp | 1479 ASS_REP(isFalse(learnt),learnt); in runSatLoop() 1481 if(learnt->length()==0) { in runSatLoop() 1482 throw UnsatException(learnt); in runSatLoop() 1484 if(learnt->length()==1) { in runSatLoop() 1485 SATLiteral lit = (*learnt)[0]; in runSatLoop() 1489 handleTopLevelConflict(learnt); in runSatLoop() 1492 makeForcedAssignment(lit, learnt); in runSatLoop() 1501 handleTopLevelConflict(learnt); in runSatLoop() 1507 insertIntoWatchIndex(learnt); in runSatLoop() 1509 ASS(isFalse((*learnt)[1])); in runSatLoop() [all …]
|
/dports/net-mgmt/librenms/librenms-21.5.1/mibs/fs/ |
H A D | MAC-NOTIFICATION-MIB | 31 devices when there are MAC addresses learnt or removed from 111 there is MAC address learnt or removed by the device. 124 "Indicates the number of MAC addresses learnt by the 144 learnt or removed from the device's forwarding database. 231 1 - MAC learnt. 240 interface from which the MAC address is learnt and has size 268 at each interface when MAC address is learnt or removed." 313 mnMacChangedNotification when a MAC address which it learnt 320 interface learnt previously is removed from the forwarding 325 interface learnt previously is removed from the forwarding
|