/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | trail.c | 28 trail->decision_level = 0; in trail_construct() 44 trail->decision_level = 0; in trail_destruct() 109 trail->decision_level ++; in trail_new_decision() 114 assert(trail->decision_level == trail->decision_level_base); in trail_new_base_level() 116 trail->decision_level_base = trail->decision_level; in trail_new_base_level() 120 assert(trail->decision_level == trail->decision_level_base); in trail_pop_base_level() 128 trail->decision_level --; in trail_undo_decision() 138 …rt((type == DECISION && level == trail->decision_level) || (type == PROPAGATION && level <= trail-… in trail_set_value() 211 if (x_level == trail->decision_level) { in trail_pop_propagation() 216 assert(x_level < trail->decision_level); in trail_pop_propagation() [all …]
|
H A D | trail.h | 59 uint32_t decision_level; member 163 return trail->decision_level == trail->decision_level_base; in trail_is_at_base_level()
|
/dports/lang/gleam/gleam-0.18.2/cargo-crates/pubgrub-0.2.1/src/internal/ |
H A D | partial_solution.rs | 49 decision_level: DecisionLevel, field 120 decision_level: self.current_decision_level, in add_derivation() 192 decision_level: DecisionLevel, in backtrack() 195 self.current_decision_level = decision_level; in backtrack() 197 if pa.smallest_decision_level > decision_level { in backtrack() 200 } else if pa.highest_decision_level <= decision_level { in backtrack() 212 while pa.dated_derivations.last().map(|dd| dd.decision_level) > Some(decision_level) in backtrack() 219 pa.highest_decision_level = pa.dated_derivations.last().unwrap().decision_level; in backtrack() 370 let (_, &(_, _, decision_level)) = satisfied_map in find_previous_satisfier() 374 decision_level.max(DecisionLevel(1)) in find_previous_satisfier() [all …]
|
H A D | core.rs | 208 decision_level: DecisionLevel, in backtrack() 211 .backtrack(decision_level, &self.incompatibility_store); in backtrack()
|
/dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
H A D | smt_core.c | 1508 s->decision_level = 0; in init_smt_core() 1731 s->decision_level = 0; in reset_smt_core() 2053 k = s->decision_level + 1; in decide_literal() 2054 s->decision_level = k; in decide_literal() 3000 d = s->decision_level; in try_cache_theory_clause() 5114 s->decision_level = k; in smt_push() 6124 if (k < s->decision_level) { in level_has_lower_activity() 6217 n = s->decision_level; in smt_partial_restart() 6262 n = s->decision_level; in smt_partial_restart_var() 6382 n = s->decision_level; in collect_decision_literals() [all …]
|
H A D | sat_solver.c | 994 solver->decision_level = 0; in init_sat_solver() 1232 assert(solver->decision_level == 0); in assign_literal() 1868 d = solver->decision_level + 1; in decide_variable() 1869 solver->decision_level = d; in decide_variable() 2709 sol->decision_level = back_level; in backtrack() 2723 assert(k <= sol->decision_level); in level_has_lower_activity() 2730 if (k < sol->decision_level) { in level_has_lower_activity() 2769 assert(sol->decision_level > 0); 2779 n = sol->decision_level; 2806 assert(sol->decision_level > 0); in partial_restart_var() [all …]
|
H A D | new_sat_solver.c | 2837 solver->decision_level = 0; in init_nsat_solver() 2996 solver->decision_level = 0; in reset_nsat_solver() 3559 k = solver->decision_level + 1; in nsat_decide_literal() 3560 solver->decision_level = k; in nsat_decide_literal() 8834 n = solver->decision_level; 8898 n = solver->decision_level; in partial_restart_using_list() 9537 n = solver->decision_level; in show_branch() 10035 k = solver->decision_level; in backtrack_one_level() 10054 solver->decision_level --; in backtrack_one_level() 10721 dl = solver->decision_level; in try_naive_search() [all …]
|
H A D | new_sat_solver2.c | 2474 solver->decision_level = 0; in init_nsat_solver() 2626 solver->decision_level = 0; in reset_nsat_solver() 2965 assert(solver->decision_level == 0); in nsat_base_literal() 3151 assert(solver->decision_level == 0); in assign_literal() 3188 k = solver->decision_level + 1; in nsat_decide_literal() 3189 solver->decision_level = k; in nsat_decide_literal() 7737 if (k < solver->decision_level) { in level_has_lower_rank() 7766 if (solver->decision_level > 0) { in partial_restart() 7777 n = solver->decision_level; in partial_restart() 7793 if (solver->decision_level > 0) { in full_restart() [all …]
|
/dports/math/yices/yices-2.6.2/tests/unit/ |
H A D | test_offset_equalities2.c | 1108 uint32_t decision_level; member 1132 bench->decision_level = 0; in init_test_bench() 1984 assert(bench->decision_level == bench->base_level); in test_push() 1991 bench->decision_level ++; in test_push() 2002 bench->decision_level ++; in test_increase_dlevel() 2011 assert(bench->decision_level > bench->base_level); in test_backtrack() 2017 bench->decision_level --; in test_backtrack() 2043 if (bench->decision_level > bench->base_level) { in test_pop() 2049 bench->decision_level --; in test_pop() 2060 bench->decision_level --; in test_pop() [all …]
|
/dports/math/yices/yices-2.6.2/src/solvers/floyd_warshall/ |
H A D | idl_floyd_warshall.c | 1272 if (solver->base_level == solver->decision_level && in idl_make_atom() 1334 assert(solver->decision_level == solver->base_level); in idl_add_axiom_edge() 1359 assert(solver->stack.top == solver->decision_level + 1); in idl_add_axiom_edge() 1418 assert(solver->stack.top == solver->decision_level + 1); in idl_add_edge() 1576 solver->decision_level ++; in idl_increase_decision_level() 1719 i = solver->decision_level; in idl_backtrack() 1729 solver->decision_level = back_level; in idl_backtrack() 1744 assert(solver->base_level == solver->decision_level); in idl_push() 1750 assert(solver->decision_level == solver->base_level); in idl_push() 1800 solver->decision_level = 0; in idl_reset() [all …]
|
H A D | rdl_floyd_warshall.c | 1502 if (solver->base_level == solver->decision_level && in rdl_make_atom() 1552 assert(solver->decision_level == solver->base_level); in rdl_axiom_edge() 1584 assert(solver->stack.top == solver->decision_level + 1); in rdl_axiom_edge() 1673 assert(solver->stack.top == solver->decision_level + 1); in rdl_add_edge() 1818 solver->decision_level ++; in rdl_increase_decision_level() 1967 i = solver->decision_level; in rdl_backtrack() 1977 solver->decision_level = back_level; in rdl_backtrack() 1992 assert(solver->base_level == solver->decision_level); in rdl_push() 1998 assert(solver->decision_level == solver->base_level); in rdl_push() 2048 solver->decision_level = 0; in rdl_reset() [all …]
|
/dports/math/clingo/clingo-5.5.1/libclingo/tests/ |
H A D | propagator.cc | 75 : decision_level(dl) in TrailItem() 77 uint32_t decision_level; member 247 uint32_t dl = ctl.assignment().decision_level(); in propagate() 248 if (state.trail.size() == 0 || state.trail.back().decision_level < dl) { in propagate() 400 REQUIRE(ass.decision_level() == 0); in init() 436 auto level = ass.decision_level(); in propagate()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | sqlstats.h | 136 , size_t decision_level
|
H A D | sqlitestats.h | 101 , size_t decision_level
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | sqlstats.h | 136 , size_t decision_level
|
H A D | sqlitestats.h | 101 , size_t decision_level
|
/dports/math/yices/yices-2.6.2/src/solvers/bv/ |
H A D | bvsolver_types.h | 293 uint32_t decision_level; member
|
H A D | new_bvsolver_types.h | 288 uint32_t decision_level; member
|
/dports/math/clingo/clingo-5.5.1/libpyclingo/clingo/tests/ |
H A D | test_propagator.py | 32 lvl = ass.decision_level 83 self._case.assertEqual(init.assignment.decision_level, 0)
|
/dports/math/clingo/clingo-5.5.1/app/clingo/tests/python/ |
H A D | assignment.lp | 23 for i in range(0, assignment.decision_level + 1):
|
H A D | propagator.lp | 134 if len(state.trail) == 0 or state.trail[-1][0] < control.assignment.decision_level: 135 state.trail.append((control.assignment.decision_level, len(state.stack)))
|
/dports/math/yices/yices-2.6.2/src/solvers/simplex/ |
H A D | offset_equalities.c | 1502 m->decision_level = 0; in init_offset_manager() 1550 m->decision_level = 0; in reset_offset_manager() 1831 if (m->base_level < m->decision_level) { in record_offset_poly() 1832 push_to_recheck(&m->recheck, m->decision_level, i); in record_offset_poly() 2295 k = m->decision_level + 1; in offset_manager_increase_decision_level() 2296 m->decision_level = k; in offset_manager_increase_decision_level() 2404 assert(k < m->decision_level && k + 1 < m->stack.size); in offset_manager_backtrack() 2437 m->decision_level = k; in offset_manager_backtrack() 2448 assert(m->base_level == m->decision_level); in offset_manager_push() 2522 assert(m->base_level > 0 && m->base_level == m->decision_level); in offset_manager_pop()
|
/dports/math/yices/yices-2.6.2/src/solvers/egraph/ |
H A D | egraph.c | 2592 if (egraph->base_level == egraph->decision_level in egraph_make_eq() 2629 if (egraph->base_level == egraph->decision_level) { in egraph_make_eq_term() 4503 k = egraph->decision_level + 1; in egraph_open_decision_level() 4504 egraph->decision_level = k; in egraph_open_decision_level() 4551 assert(egraph->decision_level == egraph->base_level); in egraph_push() 4595 egraph->decision_level = 0; in egraph_reset() 4926 n = egraph->decision_level; in egraph_local_backtrack() 4932 egraph->decision_level = back_level; in egraph_local_backtrack() 6361 assert(egraph->decision_level == egraph->base_level); in egraph_assert_axiom() 6381 assert(egraph->decision_level == egraph->base_level); in egraph_assert_eq_axiom() [all …]
|
/dports/math/clingo/clingo-5.5.1/app/clingo/tests/lua/ |
H A D | assignment.lp | 34 for i = 0, assignment.decision_level do
|
/dports/math/clingo/clingo-5.5.1/examples/clingo/gac/ |
H A D | app.py | 160 for level in range(1, assignment.decision_level+1):
|