/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | Solver.h | 190 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 248 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); } in abstractLevel() function
|
H A D | Solver.C | 298 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 351 if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ in litRedundant()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | searcher.h | 374 uint32_t abstractLevel(const uint32_t x) const; 439 inline uint32_t Searcher::abstractLevel(const uint32_t x) const
|
H A D | searcher.cpp | 214 abstract_level |= abstractLevel(learnt_clause[i].var()); in recursiveConfClauseMin() 985 && (abstractLevel(p2.var()) & abstract_levels) != 0 in litRedundant()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | searcher.h | 374 uint32_t abstractLevel(const uint32_t x) const; 439 inline uint32_t Searcher::abstractLevel(const uint32_t x) const in abstractLevel() function
|
H A D | searcher.cpp | 214 abstract_level |= abstractLevel(learnt_clause[i].var()); in recursiveConfClauseMin() 985 && (abstractLevel(p2.var()) & abstract_levels) != 0 in litRedundant()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | Solver.h | 252 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 320 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
H A D | Solver.cpp | 311 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 372 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ in litRedundant()
|
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
H A D | Solver.h | 277 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 349 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
/dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
H A D | Solver.h | 270 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 338 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | Solver.h | 277 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 349 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
H A D | Solver.h | 277 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 349 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
/dports/math/vampire/vampire-4.5.1/Minisat/core/ |
H A D | Solver.h | 283 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 355 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
H A D | Solver.h | 346 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 443 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
H A D | Solver.cc | 486 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 568 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ in litRedundant()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
H A D | Solver.h | 335 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 411 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
H A D | Glucose.cpp | 616 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 722 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ in litRedundant()
|
/dports/math/glucose/glucose-syrup-4.1/core/ |
H A D | Solver.h | 445 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 521 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
H A D | Solver.cc | 839 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 944 … if(reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0) { in litRedundant()
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
H A D | Solver.h | 430 …uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision l… 526 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } in abstractLevel() function
|
H A D | Solver.cc | 778 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 861 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ in litRedundant()
|
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
H A D | Solver.cpp | 313 …abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involve… in analyze() 374 if (reason(var(newP)) != CRef_Undef && (abstractLevel(var(newP)) & abstract_levels) != 0){ in litRedundant()
|