/dports/lang/nim/nim-1.6.2/compiler/ |
H A D | vmconv.nim | 10 ## see also reverse operation `toLit` 19 proc toLit*[T](a: T): PNode = 27 else: toLit(a[]) 30 for ai in fields(a): result.add toLit(ai) 34 result.add toLit(ai) 40 reti.add k.toLit 41 reti.add ai.toLit
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/vars/ |
H A D | int-var-el.h | 12 Lit getNELit(int v) const { return toLit(base_vlit+2*v); } in getNELit() 13 Lit getEQLit(int v) const { return toLit(base_vlit+2*v+1); } in getEQLit() 14 Lit getGELit(int v) const { return toLit(base_blit+2*v); } in getGELit() 15 Lit getLELit(int v) const { return toLit(base_blit+2*v+1); } in getLELit() 47 Lit getEQLit2(int v) const { return toLit(base_vlit+2*v+1); } in getEQLit2()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
H A D | abcSat.c | 692 Vec_IntPush( vVars, toLit(pNode->Id) ); in Abc_NodeAddClauses() 716 Vec_IntPush( vVars, toLit(pFanin->Id) ); in Abc_NodeAddClauses() 720 Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) ); in Abc_NodeAddClauses() 741 Vec_IntPush( vVars, toLit(pFanin->Id) ); in Abc_NodeAddClauses() 745 Vec_IntPush( vVars, toLit(pNode->Id) ); in Abc_NodeAddClauses() 776 Vec_IntPush( vVars, toLit(pFanin->Id) ); in Abc_NodeAddClausesTop() 777 Vec_IntPush( vVars, toLit(pNode->Id) ); in Abc_NodeAddClausesTop() 787 Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) ); in Abc_NodeAddClausesTop() 799 Vec_IntPush( vVars, toLit(pNode->Id) ); in Abc_NodeAddClausesTop() 808 Vec_IntPush( vVars, toLit(pFanin->Id) ); in Abc_NodeAddClausesTop() [all …]
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | sccfinder.cpp | 104 const Lit vertLit = Lit::toLit(vertex); in tarjan() 152 bool rhs = Lit::toLit(tmp[0]).sign() in add_bin_xor_in_tmp() 153 ^ Lit::toLit(tmp[i]).sign(); in add_bin_xor_in_tmp() 155 BinaryXor binxor(Lit::toLit(tmp[0]).var(), Lit::toLit(tmp[i]).var(), rhs); in add_bin_xor_in_tmp()
|
H A D | propby_backup.h | 147 return ~Lit::toLit(data1); in getAncestor() 165 return Lit::toLit(data1); in lit2() 173 return Lit::toLit(data2); in lit3()
|
H A D | propby.h | 150 return ~Lit::toLit(data1); in getAncestor() 168 return Lit::toLit(data1); in lit2()
|
H A D | clausecleaner.cpp | 116 && !solver->watches[Lit::toLit(wsLit2)].empty() in clean_implicit_clauses() 118 solver->watches.prefetch(Lit::toLit(wsLit2).toInt()); in clean_implicit_clauses() 121 const Lit lit = Lit::toLit(wsLit); in clean_implicit_clauses() 306 const Lit lit = Lit::toLit(wsLit); in remove_and_clean_all()
|
H A D | watched.h | 151 return Lit::toLit(data1); in lit2() 215 return Lit::toLit(data1); in getBlockedLit()
|
H A D | watched_backup.h | 143 return Lit::toLit(data1); in lit2() 211 return Lit::toLit(data1); in getBlockedLit()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | sccfinder.cpp | 104 const Lit vertLit = Lit::toLit(vertex); in tarjan() 152 bool rhs = Lit::toLit(tmp[0]).sign() in add_bin_xor_in_tmp() 153 ^ Lit::toLit(tmp[i]).sign(); in add_bin_xor_in_tmp() 155 BinaryXor binxor(Lit::toLit(tmp[0]).var(), Lit::toLit(tmp[i]).var(), rhs); in add_bin_xor_in_tmp()
|
H A D | propby_backup.h | 147 return ~Lit::toLit(data1); in getAncestor() 165 return Lit::toLit(data1); in lit2() 173 return Lit::toLit(data2); in lit3()
|
H A D | propby.h | 150 return ~Lit::toLit(data1); in getAncestor() 168 return Lit::toLit(data1); in lit2()
|
H A D | clausecleaner.cpp | 116 && !solver->watches[Lit::toLit(wsLit2)].empty() in clean_implicit_clauses() 118 solver->watches.prefetch(Lit::toLit(wsLit2).toInt()); in clean_implicit_clauses() 121 const Lit lit = Lit::toLit(wsLit); in clean_implicit_clauses() 306 const Lit lit = Lit::toLit(wsLit); in remove_and_clean_all()
|
H A D | watched.h | 151 return Lit::toLit(data1); in lit2() 215 return Lit::toLit(data1); in getBlockedLit()
|
H A D | watched_backup.h | 143 return Lit::toLit(data1); in lit2() 211 return Lit::toLit(data1); in getBlockedLit()
|
/dports/www/hs-postgrest/postgrest-8.0.0/_cabal_deps/haskell-src-meta-0.8.7/src/Language/Haskell/Meta/Syntax/ |
H A D | Translate.hs | 36 class ToLit a where toLit :: a -> TH.Lit 120 toLit = TH.CharL function 122 toLit = TH.StringL function 124 toLit = TH.IntegerL function 126 toLit = TH.IntegerL . toInteger function 128 toLit = TH.RationalL . toRational function 130 toLit = TH.RationalL . toRational function 193 toLit (Exts.Char _ a _) = TH.CharL a function 194 toLit (Exts.String _ a _) = TH.StringL a function 195 toLit (Exts.Int _ a _) = TH.IntegerL a function [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | satVec.h | 142 static inline lit toLit (int v) { return v + v; } in toLit() function 148 static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } in lit_read()
|
/dports/math/stp/stp-2.3.3/lib/Sat/ |
H A D | RissCore.cpp | 73 for(int i = 0 ; i < ps.size(); ++ i) v.push_(Riss::toLit(Minisat::toInt(ps[i]))); in addClause() 97 for(int i = 0 ; i < assumps.size(); ++ i) v.push_(Riss::toLit(Minisat::toInt(assumps[i]))); in propagateWithAssumptions()
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/globals/ |
H A D | table.cpp | 26 sat.addClause(toLit(base_lit+2*i), x[j]->getLit(t[i][j], 1)); in table_GAC() 45 else sup[k].push(toLit(base_lit+2*i+1)); in table_GAC()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/mpi/ |
H A D | DataSync.cpp | 238 Lit lit = ~Lit::toLit(wsLit); in syncFromMPI() 242 Lit otherLit = Lit::toLit(buf[at]); in syncFromMPI() 252 Lit lit = ~Lit::toLit(wsLit); in syncFromMPI() 256 Lit otherLit = Lit::toLit(buf[at]); in syncFromMPI() 258 Lit otherLit2 = Lit::toLit(buf[at]); in syncFromMPI() 299 Lit lit1 = ~Lit::toLit(wsLit); in syncToMPI() 321 Lit lit1 = ~Lit::toLit(wsLit); in syncToMPI() 363 Lit lit1 = ~Lit::toLit(wsLit); in shareBinData() 431 Lit lit1 = ~Lit::toLit(wsLit); in shareTriData()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/mpi/ |
H A D | DataSync.cpp | 238 Lit lit = ~Lit::toLit(wsLit); in syncFromMPI() 242 Lit otherLit = Lit::toLit(buf[at]); in syncFromMPI() 252 Lit lit = ~Lit::toLit(wsLit); in syncFromMPI() 256 Lit otherLit = Lit::toLit(buf[at]); in syncFromMPI() 258 Lit otherLit2 = Lit::toLit(buf[at]); in syncFromMPI() 299 Lit lit1 = ~Lit::toLit(wsLit); in syncToMPI() 321 Lit lit1 = ~Lit::toLit(wsLit); in syncToMPI() 363 Lit lit1 = ~Lit::toLit(wsLit); in shareBinData() 431 Lit lit1 = ~Lit::toLit(wsLit); in shareTriData()
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/ldsb/ |
H A D | ldsb.cpp | 185 q = toLit(toInt(p) - base_a + base_b); in getSymLit() 191 q = toLit(toInt(p) - base_b + base_a); in getSymLit() 351 q = toLit(toInt(p) - a*2 + b*2); in getSymLit() 356 q = toLit(toInt(p) - b*2 + a*2); in getSymLit() 498 return toLit(toInt(p) - base_r1 + base_r2); in getSymLit() 503 return toLit(toInt(p) - base_r2 + base_r1); in getSymLit() 676 return toLit(toInt(p) - v*2 + v2*2); in getSymLit() 680 return toLit(toInt(p) - v*2 + v2*2); in getSymLit()
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | minisat_types.h | 71 static Lit toLit (int i) { return Lit(i); }; in toLit() function 152 void toLit (std::vector<Lit>& literals) const;
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/ |
H A D | fraSat.c | 83 pLits[0] = toLit( 0 ); in Fra_NodesAreEquiv() 244 pLits[0] = toLit( 0 ); in Fra_NodesAreImp() 352 pLits[0] = toLit( 0 ); in Fra_NodesAreClause() 442 pLits[0] = toLit( 0 ); in Fra_NodeIsConst()
|
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | SolverTypes.h | 46 friend Lit toLit (int i); // Inverse of 'toInt()' 59 inline Lit toLit (int i) { Lit p; p.x = i; return p; } in toLit() function
|