Home
last modified time | relevance | path

Searched refs:learnt (Results 1 – 25 of 1058) sorted by relevance

12345678910>>...43

/dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/
H A DSolverTypes.h139 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 DSolverTypes.h126 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 DSolverTypes.h135 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 DSolverTypes.h163 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 DSolverTypes.h115 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 Dsat-types.h80 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 DSolverTypes.h149 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 DSolverTypes.h143 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 DSolverTypes.h143 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 DSolverTypes.h148 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 DDataSync.cpp387 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 DDataSync.h41 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 DDataSync.cpp387 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 DDataSync.h41 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 Dminisat_types.h119 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 DSolverTypes.h143 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 Dchuffed.msc.in25 ["--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 Dminisat.c343 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 Dminisat.c343 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 Da3com-huawei-mac-information.mib99 "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 Dhh3c-mac-information.mib99 "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 Dh3c-mac-information.mib99 "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 DA3COM-HUAWEI-MAC-INFORMATION-MIB99 "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 DTWLSolver.cpp1479 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 DMAC-NOTIFICATION-MIB31 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

12345678910>>...43