/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | minisat_types.h | 56 const int var_Undef = -1; variable 64 Lit() : x(2*var_Undef) {} // (lit_Undef) in Lit() 95 const Lit lit_Undef(var_Undef, false); // }- Useful special constants. 96 const Lit lit_Error(var_Undef, true ); // }
|
H A D | minisat_varorder.h | 134 return var_Undef; in select()
|
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | SolverTypes.h | 35 #define var_Undef (-1) macro 41 Lit() : x(2*var_Undef) { } // (lit_Undef) in Lit() 66 const Lit lit_Undef(var_Undef, false); // }- Useful special constants. 67 const Lit lit_Error(var_Undef, true ); // }
|
H A D | Solver.C | 203 Var next = var_Undef; in pickBranchLit() 212 while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !decision_var[next]) in pickBranchLit() 214 next = var_Undef; in pickBranchLit() 227 return next == var_Undef ? lit_Undef : Lit(next, sign); in pickBranchLit()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | cms_breakid.cpp | 45 if (symm_var != var_Undef) { in updateVars() 431 if (symm_var == var_Undef) { in break_symms_in_cms() 475 if (symm_var == var_Undef) { in start_new_solving() 486 symm_var = var_Undef; in start_new_solving() 494 symm_var = var_Undef; in start_new_solving() 500 if (symm_var != var_Undef) { in update_var_after_varreplace()
|
H A D | solvertypesmini.h.in | 33 constexpr uint32_t var_Undef(0xffffffffU >> 4); 43 constexpr Lit() : x(var_Undef<<1) {} // (lit_Undef) 94 static const Lit lit_Undef(var_Undef, false); // Useful special constants. 95 static const Lit lit_Error(var_Undef, true ); //
|
H A D | matrixfinder.cpp | 80 if (table[v] == var_Undef) { 106 table.resize(solver->nVars(), var_Undef); 186 if (table[v] != var_Undef)
|
H A D | cms_breakid.h | 80 uint32_t symm_var = var_Undef;
|
H A D | intree.cpp | 278 if (tmp.var_reason_changed != var_Undef) { in tree_look() 305 reset_reason_stack.push_back(ResetReason(var_Undef, PropBy())); in handle_lit_popped_from_queue()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | cms_breakid.cpp | 45 if (symm_var != var_Undef) { in updateVars() 431 if (symm_var == var_Undef) { in break_symms_in_cms() 475 if (symm_var == var_Undef) { in start_new_solving() 486 symm_var = var_Undef; in start_new_solving() 494 symm_var = var_Undef; in start_new_solving() 500 if (symm_var != var_Undef) { in update_var_after_varreplace()
|
H A D | solvertypesmini.h.in | 33 constexpr uint32_t var_Undef(0xffffffffU >> 4); 43 constexpr Lit() : x(var_Undef<<1) {} // (lit_Undef) 94 static const Lit lit_Undef(var_Undef, false); // Useful special constants. 95 static const Lit lit_Error(var_Undef, true ); //
|
H A D | matrixfinder.cpp | 80 if (table[v] == var_Undef) { in belong_same_matrix() 106 table.resize(solver->nVars(), var_Undef); in findMatrixes() 186 if (table[v] != var_Undef) in findMatrixes()
|
H A D | cms_breakid.h | 80 uint32_t symm_var = var_Undef;
|
H A D | intree.cpp | 278 if (tmp.var_reason_changed != var_Undef) { in tree_look() 305 reset_reason_stack.push_back(ResetReason(var_Undef, PropBy())); in handle_lit_popped_from_queue()
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
H A D | sat-types.h | 11 #define var_Undef (-1) macro 16 Lit() : x(2*var_Undef) { } // (lit_Undef) in Lit() 42 const Lit lit_Undef(var_Undef, false); // }- Useful special constants. 43 const Lit lit_Error(var_Undef, true ); // }
|
/dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
H A D | SolverTypes.h | 42 #define var_Undef (-1) macro 69 const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants. 70 const Lit lit_Error = mkLit(var_Undef, true ); // }
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | Solver.cpp | 227 Var next = var_Undef; in pickBranchLit() 236 while (next == var_Undef || value(next) != l_Undef || !decision[next]) in pickBranchLit() 238 next = var_Undef; in pickBranchLit() 243 …return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[n… in pickBranchLit()
|
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
H A D | Solver.cpp | 227 Var next = var_Undef; in pickBranchLit() 237 while (next == var_Undef || value(next) != l_Undef || !decision[next]) in pickBranchLit() 239 next = var_Undef; in pickBranchLit() 244 return (next == var_Undef) ? lit_Undef : in pickBranchLit()
|
/dports/math/igraph/igraph-0.9.5/vendor/glpk/minisat/ |
H A D | minisat.h | 49 #define var_Undef (int)(-1) macro
|
/dports/math/glpk/glpk-5.0/src/minisat/ |
H A D | minisat.h | 49 #define var_Undef (int)(-1) macro
|
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
H A D | Solver.cc | 257 Var next = var_Undef; in pickBranchLit() 266 while (next == var_Undef || value(next) != l_Undef || !decision[next]) in pickBranchLit() 268 next = var_Undef; in pickBranchLit() 274 if (next == var_Undef) in pickBranchLit()
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | Solver.cc | 251 Var next = var_Undef; in pickBranchLit() 260 while (next == var_Undef || value(next) != l_Undef || !decision[next]) in pickBranchLit() 262 next = var_Undef; in pickBranchLit() 268 if (next == var_Undef) in pickBranchLit()
|
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
H A D | Solver.cc | 251 Var next = var_Undef; in pickBranchLit() 260 while (next == var_Undef || value(next) != l_Undef || !decision[next]) in pickBranchLit() 262 next = var_Undef; in pickBranchLit() 268 if (next == var_Undef) in pickBranchLit()
|
/dports/math/vampire/vampire-4.5.1/Minisat/core/ |
H A D | Solver.cc | 256 Var next = var_Undef; in pickBranchLit() 265 while (next == var_Undef || value(next) != l_Undef || !decision[next]) in pickBranchLit() 267 next = var_Undef; in pickBranchLit() 273 if (next == var_Undef) in pickBranchLit()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | satVec.h | 135 static const int var_Undef = -1; variable
|