| /dports/math/py-or-tools/or-tools-9.2/ortools/sat/ |
| H A D | clause.h | 376 struct BinaryClause { struct
377 BinaryClause(Literal _a, Literal _b) : a(_a), b(_b) {} in BinaryClause() argument
378 bool operator==(BinaryClause o) const { return a == o.a && b == o.b; }
379 bool operator!=(BinaryClause o) const { return a != o.a || b != o.b; }
392 bool Add(BinaryClause c) { in Add() argument
404 const std::vector<BinaryClause>& newly_added() const { return newly_added_; } in newly_added()
409 std::vector<BinaryClause> newly_added_;
|
| H A D | sat_solver.h | 347 bool AddBinaryClauses(const std::vector<BinaryClause>& clauses);
348 const std::vector<BinaryClause>& NewlyAddedBinaryClauses();
|
| H A D | sat_solver.cc | 376 CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1]))); in AddLearnedClauseAndEnqueueUnitPropagation()
452 if (!track_binary_clauses_ || binary_clauses_.Add(BinaryClause(a, b))) { in AddBinaryClauseInternal()
919 bool SatSolver::AddBinaryClauses(const std::vector<BinaryClause>& clauses) { in AddBinaryClauses()
922 for (BinaryClause c : clauses) { in AddBinaryClauses()
933 const std::vector<BinaryClause>& SatSolver::NewlyAddedBinaryClauses() { in NewlyAddedBinaryClauses()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | hyperengine.h | 49 …set<BinaryClause> needToAddBinClause; ///<We store here hyper-binary clauses to be added at …
50 set<BinaryClause> uselessBin;
|
| H A D | solvertypes.h | 177 class BinaryClause {
179 BinaryClause(const Lit _lit1, const Lit _lit2, const bool _red) : in BinaryClause() function
187 bool operator<(const BinaryClause& other) const
197 bool operator==(const BinaryClause& other) const
226 inline std::ostream& operator<<(std::ostream& os, const BinaryClause val)
|
| H A D | hyperengine.cpp | 182 needToAddBinClause.insert(BinaryClause(p, ~deepestAncestor, true)); in add_hyper_bin()
529 const BinaryClause clauseToRemove( in remove_bin_clause()
550 std::set<BinaryClause>::iterator it = needToAddBinClause.find(clauseToRemove); in remove_bin_clause()
622 uselessBin.insert(BinaryClause(~p, lit, k->red())); in prop_bin_with_ancestor_info()
|
| H A D | str_impl_w_impl.h | 68 vector<BinaryClause> binsToAdd;
|
| H A D | clausecleaner.h | 63 vector<BinaryClause> toAttach;
|
| H A D | propengine.h | 242 bool satisfied(const BinaryClause& bin);
310 inline bool PropEngine::satisfied(const BinaryClause& bin) in satisfied()
|
| H A D | str_impl_w_impl.cpp | 69 for(const BinaryClause& bin: str_impl_data.binsToAdd) { in str_impl_w_impl()
|
| H A D | varreplacer.h | 174 vector<BinaryClause> delayed_attach_bin;
|
| H A D | clausecleaner.cpp | 253 for(const BinaryClause& bincl: toAttach) { in update_solver_stats()
|
| H A D | varreplacer.cpp | 504 for(const BinaryClause& bincl : delayed_attach_bin) { in replaceImplicit()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | hyperengine.h | 49 …set<BinaryClause> needToAddBinClause; ///<We store here hyper-binary clauses to be added at …
50 set<BinaryClause> uselessBin;
|
| H A D | solvertypes.h | 177 class BinaryClause {
179 BinaryClause(const Lit _lit1, const Lit _lit2, const bool _red) : in BinaryClause() function
187 bool operator<(const BinaryClause& other) const
197 bool operator==(const BinaryClause& other) const
226 inline std::ostream& operator<<(std::ostream& os, const BinaryClause val)
|
| H A D | hyperengine.cpp | 182 needToAddBinClause.insert(BinaryClause(p, ~deepestAncestor, true)); in add_hyper_bin()
529 const BinaryClause clauseToRemove( in remove_bin_clause()
550 std::set<BinaryClause>::iterator it = needToAddBinClause.find(clauseToRemove); in remove_bin_clause()
622 uselessBin.insert(BinaryClause(~p, lit, k->red())); in prop_bin_with_ancestor_info()
|
| H A D | str_impl_w_impl.h | 68 vector<BinaryClause> binsToAdd;
|
| H A D | clausecleaner.h | 63 vector<BinaryClause> toAttach;
|
| H A D | propengine.h | 242 bool satisfied(const BinaryClause& bin);
310 inline bool PropEngine::satisfied(const BinaryClause& bin) in satisfied()
|
| H A D | str_impl_w_impl.cpp | 69 for(const BinaryClause& bin: str_impl_data.binsToAdd) { in str_impl_w_impl()
|
| H A D | varreplacer.h | 174 vector<BinaryClause> delayed_attach_bin;
|
| H A D | clausecleaner.cpp | 253 for(const BinaryClause& bincl: toAttach) { in update_solver_stats()
|
| /dports/math/py-or-tools/or-tools-9.2/ortools/bop/ |
| H A D | bop_base.h | 219 const std::vector<sat::BinaryClause>& NewlyAddedBinaryClauses() const;
281 std::vector<sat::BinaryClause> binary_clauses;
|
| H A D | bop_base.cc | 109 for (sat::BinaryClause c : learned_info.binary_clauses) { in MergeLearnedInfo()
249 const std::vector<sat::BinaryClause>& ProblemState::NewlyAddedBinaryClauses() in NewlyAddedBinaryClauses()
|
| H A D | bop_fs.cc | 405 for (const sat::BinaryClause& clause : in SynchronizeIfNeeded()
|