Home
last modified time | relevance | path

Searched refs:var_Undef (Results 1 – 25 of 58) sorted by relevance

123

/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dminisat_types.h56 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 Dminisat_varorder.h134 return var_Undef; in select()
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/
H A DSolverTypes.h35 #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 DSolver.C203 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 Dcms_breakid.cpp45 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 Dsolvertypesmini.h.in33 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 Dmatrixfinder.cpp80 if (table[v] == var_Undef) {
106 table.resize(solver->nVars(), var_Undef);
186 if (table[v] != var_Undef)
H A Dcms_breakid.h80 uint32_t symm_var = var_Undef;
H A Dintree.cpp278 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 Dcms_breakid.cpp45 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 Dsolvertypesmini.h.in33 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 Dmatrixfinder.cpp80 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 Dcms_breakid.h80 uint32_t symm_var = var_Undef;
H A Dintree.cpp278 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 Dsat-types.h11 #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 DSolverTypes.h42 #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 DSolver.cpp227 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 DSolver.cpp227 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 Dminisat.h49 #define var_Undef (int)(-1) macro
/dports/math/glpk/glpk-5.0/src/minisat/
H A Dminisat.h49 #define var_Undef (int)(-1) macro
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/
H A DSolver.cc257 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 DSolver.cc251 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 DSolver.cc251 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 DSolver.cc256 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 DsatVec.h135 static const int var_Undef = -1; variable

123