Home
last modified time | relevance | path

Searched refs:decision_level (Results 1 – 25 of 56) sorted by relevance

123

/dports/math/yices/yices-2.6.2/src/mcsat/
H A Dtrail.c28 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 Dtrail.h59 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 Dpartial_solution.rs49 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 Dcore.rs208 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 Dsmt_core.c1508 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 Dsat_solver.c994 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 Dnew_sat_solver.c2837 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 Dnew_sat_solver2.c2474 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 Dtest_offset_equalities2.c1108 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 Didl_floyd_warshall.c1272 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 Drdl_floyd_warshall.c1502 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 Dpropagator.cc75 : 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 Dsqlstats.h136 , size_t decision_level
H A Dsqlitestats.h101 , size_t decision_level
/dports/math/cryptominisat/cryptominisat-5.8.0/src/
H A Dsqlstats.h136 , size_t decision_level
H A Dsqlitestats.h101 , size_t decision_level
/dports/math/yices/yices-2.6.2/src/solvers/bv/
H A Dbvsolver_types.h293 uint32_t decision_level; member
H A Dnew_bvsolver_types.h288 uint32_t decision_level; member
/dports/math/clingo/clingo-5.5.1/libpyclingo/clingo/tests/
H A Dtest_propagator.py32 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 Dassignment.lp23 for i in range(0, assignment.decision_level + 1):
H A Dpropagator.lp134 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 Doffset_equalities.c1502 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 Degraph.c2592 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 Dassignment.lp34 for i = 0, assignment.decision_level do
/dports/math/clingo/clingo-5.5.1/examples/clingo/gac/
H A Dapp.py160 for level in range(1, assignment.decision_level+1):

123