Home
last modified time | relevance | path

Searched defs:backtrack_level (Results 1 – 25 of 42) sorted by relevance

12

/dports/math/py-or-tools/or-tools-9.2/ortools/util/
H A Drev.h209 const int backtrack_level = first_op_index_of_next_level_[level]; in SetLevel() local
281 const int backtrack_level = first_added_key_of_next_level_[level]; in SetLevel() local
/dports/math/conauto/conauto-2.03/src/
H A Dseqpart.h49 int backtrack_level; member
H A Dseqpart.c592 …contained_cells ( int level, uint16_t *vertices, SeqPart *sp, Perm_Group *pg, int backtrack_level ) in process_contained_cells()
771 int backtrack_level; local
840 int backtrack_level; local
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/fd_solver/
H A Dpb2bv_solver.cpp122 …expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { flush_assertions(… in cube()
H A Denum2bv_solver.cpp129 expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { in cube()
H A Dbounded_int2bv_solver.cpp199 …expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { flush_assertions(… in cube()
/dports/math/z3/z3-z3-4.8.13/src/tactic/fd_solver/
H A Dpb2bv_solver.cpp126 …expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { flush_assertions(… in cube()
H A Denum2bv_solver.cpp133 expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { in cube()
H A Dbounded_int2bv_solver.cpp203 …expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { flush_assertions(… in cube()
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/
H A DSolver.cpp619 int backtrack_level; in search() local
714 int backtrack_level; in search() local
/dports/math/z3/z3-z3-4.8.13/src/muz/spacer/
H A Dspacer_pdr.cpp172 void model_search::backtrack_level(bool uses_level, model_node& n) { in backtrack_level() function in spacer::model_search
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/
H A Dspacer_pdr.cpp172 void model_search::backtrack_level(bool uses_level, model_node& n) { in backtrack_level() function in spacer::model_search
/dports/math/py-z3-solver/z3-z3-4.8.10/src/solver/
H A Dcombined_solver.cpp267 expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { in cube()
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/
H A DSolver.C577 int backtrack_level; in search() local
/dports/math/z3/z3-z3-4.8.13/src/solver/
H A Dcombined_solver.cpp272 expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { in cube()
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/
H A Dsqlitestats.cpp731 , uint32_t backtrack_level in dump_clause_stats()
H A Dsearcher.cpp1439 void Searcher::update_history_stats(size_t backtrack_level, uint32_t glue) in update_history_stats()
1808 uint32_t backtrack_level; in handle_conflict() local
/dports/math/cryptominisat/cryptominisat-5.8.0/src/
H A Dsqlitestats.cpp731 , uint32_t backtrack_level in dump_clause_stats()
H A Dsearcher.cpp1439 void Searcher::update_history_stats(size_t backtrack_level, uint32_t glue) in update_history_stats()
1808 uint32_t backtrack_level; in handle_conflict() local
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/
H A DSolver.cpp617 int backtrack_level; in search() local
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/
H A DSolver.cc711 int backtrack_level; in search() local
/dports/math/minisat/minisat-2.2.1/minisat/core/
H A DSolver.cc705 int backtrack_level; in search() local
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/
H A DSolver.cc705 int backtrack_level; in search() local
/dports/math/vampire/vampire-4.5.1/Minisat/core/
H A DSolver.cc710 int backtrack_level; in search() local
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/
H A DSolver.cc969 int backtrack_level; in search() local

12