mercurylang/mercury
1
0
Fork 0
mirror of https://github.com/Mercury-Language/mercury.git synced 2025-12-06 07:49:02 +00:00
Code Issues Projects Releases Wiki Activity
Files
master
mercury/grade_lib/grade_solver.m
Julien Fischer 40575f7cce Update more copyright notices. 
browser/*.m:
grade_lib/*.m:
mdbcomp/*.m:
profiler/*.m:
ssdb/*.m:
     As above.
2024-12-29 20:53:29 +11:00

1199 lines
48 KiB
Mathematica
Raw Permalink Blame History

%---------------------------------------------------------------------------%
% vim: ts=4 sw=4 et ft=mercury
%---------------------------------------------------------------------------%
% Copyright (C) 2016, 2018, 2020, 2024 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%---------------------------------------------------------------------------%
%
% This module implements the solver for grade problems.
%
% The state of the solver consists of a set of solver variables, each with
% a set of possible values. A grade problem narrows the set of possible
% values of some of the solver variables. Solving a grade problem
% consists of finding an assignment of a single possible value to each
% solver variable that simultaneously satisfies all the requirements
% imposed by the Mercury grade system. (Two example requirements are
% "Boehm-Demers-Weiser gc requires targeting C" and "Trail segments require
% trailing.") The propagation part of the solver uses these requirements
% to continually narrow the set of possible values of solver variables
% until no more such narrowing is possible.
%
% Most grade problems are underspecified. For example, the solutions of
% the grade problem that asks for (a) declarative debugging and (b) trailing
% include none.decldebug.tr, asm_fast.decldebug.tr, none.decldebug.tr.rbmm,
% none.decldebug.tr.profall, and many, many more.
%
% For grade problems that have more than one solution, we want to return
% the solution that is "best" in some sense. We have two ways to make such
% choices:
%
% - we can choose in the ABSOLUTE space of all possible valid grades, or
%
% - we can choose RELATIVE to a specified set of grades, such as the set of
% installed grades.
%
% When we are looking for absolute solutions, we use labeling. A labeling
% step looks for solver variables with two or more values that are still
% possible, picks the highest priority such variable, and binds it to the
% most preferred value of that variable. (The priority list and the notion
% of preference among values are encoded in the solver state, which is
% initialized by grade_setup.m based on the solver var specs and requirement
% specs in grade_spec.m.) It then invokes propagation again to process
% the implications of that choice. If propagation still does not arrive
% either at failure (some solver variable has no possible values) or success
% (all solver variables have exactly one possible value), it invokes labelling
% again. This continues as long as needed. Since both labelling and
% propagation monotonically remove possible values from solver variables,
% the process is guaranteed to terminate, and to do so reasonably quickly.
%
% When we are looking for the best match relative to a specified set of grades,
% intended to be the set of already installed grades, we don't do labelling.
% Instead, after discarding the installed grades that don't match the results
% of propagation, we repeatedly find the highest priority solver variable
% that has two or more matches in the remaining set of installed grades,
% and discard the installed grades in the set that map that variable
% to any value but the most preferred still-possible value of that variable.
% We stop when the set has been whittled down a single installed grade.
:- module grade_lib.grade_solver.
:- interface.
:- import_module grade_lib.grade_spec.
:- import_module grade_lib.grade_state.
:- import_module list.
:- import_module map.
:- import_module one_or_more.
:- type solve_counts
---> solve_counts(
sc_num_label_steps :: int,
sc_num_passes :: int,
sc_num_req_tests :: int
).
% An abstract piece of information from which failure trees can be
% extracted by failure_info_to_failure_trees.
%
:- type failure_info.
% Maps every solver variable to its assigned value.
%
:- type success_soln_map == map(solver_var_id, solver_var_value_id).
:- type solution
---> soln_failure(
% The grade problem we were asked to solve is inconsistent.
% The failure_info encodes the cause of the inconsistencies;
% it can be decoded with failure_info_to_failure_trees.
failure_info
)
; soln_success(
% The grade problem we were asked to solve is consistent;
% this is the "best" solution.
success_soln_map
).
% See the description of absolute solutions in the comment at the top
% of the module.
%
:- pred solve_absolute(solver_info::in, solve_counts::out, solution::out)
is det.
%---------------------------------------------------------------------------%
:- type installed_grade
---> installed_grade(
% The name of the installed grade.
string,
% The setting of every solver variable in the installed grade.
success_soln_map
).
% In the search for the best installed grade, when we make a choice,
% should we commit to that choice, or should we be prepared to backtrack
% if the initial choice turns out not to lead to a solution?
% XXX This should not be needed; should_not_commit does NOT lead
% to any solutions that should_commit does not lead to. However,
% I (zs) could not be 100% sure of that without implementing
% should_not_commit, and trying it out.
:- type should_commit
---> should_commit
; should_not_commit.
:- type installed_grade_solution
---> installed_grade_spec_is_inconsistent(
% The grade problem we were asked to solve is inconsistent.
% The failure_info encodes the cause of the inconsistencies;
% it can be decoded with failure_info_to_failure_trees.
failure_info
)
; installed_grade_success(
% The grade problem we were asked to solve is consistent;
% this is the "best" solution among the installed grades.
installed_grade
)
; no_such_installed_grade.
% The grade problem we were asked to solve is consistent,
% but the set of installed grades we were given does not include
% *any* of its solutions.
% See the description of relative solutions in the comment at the top
% of the module.
%
:- pred solve_best_installed_grade(solver_info::in, should_commit::in,
list(installed_grade)::in,
solve_counts::out, installed_grade_solution::out) is det.
%---------------------------------------------------------------------------%
% solver_var_map_to_str(Prefix, SolverVarMap):
%
% Print the contents of the given solver map to a string.
% For each solver variable, and each potential value of that variable,
% print whether the value is still possible, and if not, why not.
% Add the given string as a prefix before every line.
%
% Abort if we detect that a supposed invariant of the solver map
% data structure does not actually hold.
%
:- func solver_var_map_to_str(string, solver_var_map) = string.
% solver_var_map_to_str(Prefix, Soln):
%
% Print whether the solution is a success or a failure. If a success,
% print the selected values of the solver variables as a sequence of lines
% of the form SolverVar = SolverVarValue.
% Add the given string as a prefix before every line.
%
:- func soln_to_str(string, solution) = string.
%---------------------------------------------------------------------------%
:- type failure_tree
---> failure_tree(
% The solving process fails when we find that
% a solver variable has no possible value.
solver_var_id,
% This is the solver variable.
list(why_var_is_not_value)
% For each of the values that this variable may ordinarily
% have, and which was not ruled out by autoconfiguration
% or directly by the user, this says why that value has been
% ruled out. (The qualifications mean we have an entry
% in this list only for values that were ruled out
% by propagation.)
).
:- type why_var_is_not_value
---> why_var_is_not_value(
solver_var_value_id,
% The value that was ruled out.
requirement_id,
string,
% The id and the description of the requirement that ruled out
% the solver var having this value.
list(failure_tree)
% We can apply a requirement (in either direction) only if
% the *other* variable involved in the requirement had some
% of *its* values ruled out. (If all solver variables had
% all their values marked as possible, no propagation
% could ever take place.)
%
% If some of values of the other variable were also ruled out
% by propagation, this field will be a singleton list
% containing the reason why those values were ruled out.
% Otherwise, it will be the empty list.
).
:- func failure_info_to_failure_trees(failure_info)
= one_or_more(failure_tree).
%---------------------------------------------------------------------------%
:- implementation.
:- import_module grade_lib.grade_setup.
:- import_module var_value_names.
:- import_module assoc_list.
:- import_module bool.
:- import_module int.
:- import_module maybe.
:- import_module pair.
:- import_module require.
:- import_module set.
:- import_module string.
%---------------------------------------------------------------------------%
solve_absolute(SolverInfo, SolveCounts, Soln) :-
SolverInfo = solver_info(Requirements, SolverVarPriorities, SolverVarMap0),
SolveCounts0 = solve_counts(0, 0, 0),
solve_absolute_loop(Requirements, Requirements, _FinalRequirements,
SolverVarPriorities, SolverVarMap0,
SolveCounts0, SolveCounts, Soln).
%---------------------------------------------------------------------------%
:- pred solve_absolute_loop(list(requirement)::in,
list(requirement)::in, list(requirement)::out,
list(solver_var_id)::in, solver_var_map::in,
solve_counts::in, solve_counts::out, solution::out) is det.
solve_absolute_loop(AllRequirements, !CurRequirements,
!.SolverVarPriorities, !.SolverVarMap, !SolveCounts, Soln) :-
propagate_to_fixpoint(!CurRequirements, !SolverVarMap, !SolveCounts),
are_we_at_solution(AllRequirements, !.SolverVarMap, MaybeSoln),
(
MaybeSoln = yes(Soln)
;
MaybeSoln = no,
NumLabelSteps0 = !.SolveCounts ^ sc_num_label_steps,
!SolveCounts ^ sc_num_label_steps := NumLabelSteps0 + 1,
label_step(!SolverVarPriorities, !SolverVarMap),
solve_absolute_loop(AllRequirements, !CurRequirements,
!.SolverVarPriorities, !.SolverVarMap, !SolveCounts, Soln)
).
%---------------------------------------------------------------------------%
:- type maybe_changed
---> not_changed
; changed.
:- type maybe_found_failure
---> have_not_found_failure
; found_failure.
:- pred propagate_to_fixpoint(list(requirement)::in, list(requirement)::out,
solver_var_map::in, solver_var_map::out,
solve_counts::in, solve_counts::out) is det.
propagate_to_fixpoint(Requirements0, Requirements, !SolverVarMap,
!SolveCounts) :-
NumPasses0 = !.SolveCounts ^ sc_num_passes,
NumReqTests0 = !.SolveCounts ^ sc_num_req_tests,
NumPasses = NumPasses0 + 1,
NumReqTests = NumReqTests0 + list.length(Requirements0),
!SolveCounts ^ sc_num_passes := NumPasses,
!SolveCounts ^ sc_num_req_tests := NumReqTests,
propagate_pass(Requirements0, [], RevRequirements1, !SolverVarMap,
not_changed, Changed, have_not_found_failure, FoundFailure),
list.reverse(RevRequirements1, Requirements1),
trace [compile_time(flag("debug_solver")), io(!TIO)]
(
(
FoundFailure = have_not_found_failure,
FoundFailureSuffix = ""
;
FoundFailure = found_failure,
FoundFailureSuffix = " (found failure)"
),
list.length(Requirements0, NumReqs0),
list.length(Requirements1, NumReqs1),
SolverVarMapStr = solver_var_map_to_str(" ", !.SolverVarMap),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr, "\nAFTER PROPAGATE PASS %d, #reqs %d -> %d%s\n",
[i(NumPasses0), i(NumReqs0), i(NumReqs1), s(FoundFailureSuffix)],
!TIO),
io.write_string(StdErr, SolverVarMapStr, !TIO),
io.nl(StdErr, !TIO)
),
(
FoundFailure = found_failure,
% The next pass may have one of two results. Either it will return
% not_changed, in which case the pass is wasted, or it will return
% changed, with some of the changes being implications of the failure
% we have already found. (For example, if X = x1 implies Y in {y1,y2},
% then having no possible value left for Y in this pass may leave
% no possible value for X in the next pass.) However, no further
% pass can turn the failure back to a success, so there is no point
% in doing such passes. There is point in NOT doing them: it allows
% a failure error message to report the actual cause of the failure,
% not its implications in later passes.
% XXX Should we try to eliminate recording the implications of
% the first failure in the *same pass*? And how would we distinguish
% them from unrelated failures in the same pass?
Requirements = Requirements1
;
FoundFailure = have_not_found_failure,
(
Changed = not_changed,
Requirements = Requirements1
;
Changed = changed,
propagate_to_fixpoint(Requirements1, Requirements, !SolverVarMap,
!SolveCounts)
)
).
:- pred propagate_pass(list(requirement)::in,
list(requirement)::in, list(requirement)::out,
solver_var_map::in, solver_var_map::out,
maybe_changed::in, maybe_changed::out,
maybe_found_failure::in, maybe_found_failure::out) is det.
propagate_pass([], !RevRequirements, !SolverVarMap, !Changed, !FoundFailure).
propagate_pass([Requirement | Requirements], !RevRequirements,
!SolverVarMap, !Changed, !FoundFailure) :-
Requirement = requirement(ReqId, ReqDesc,
IfVarId, IfValueId, ThenVarId, ReqThenValueIds),
trace [compile_time(flag("debug_solver")), io(!TIO)] (
ReqId = requirement_id(ReqIdNum0),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr, "Considering Req %d (%s)\n",
[i(ReqIdNum0), s(ReqDesc)], !TIO)
),
% The requirement represents the implication:
%
% (IfVarId = IfValueId) -> (ThenVarId in ReqThenValueIds)
%
map.lookup(!.SolverVarMap, IfVarId, IfVar0),
IfVar0 = solver_var(IfCntAll, IfCntPoss0, IfValues0),
( if is_value_possible(IfValues0, IfValueId, is_possible) then
map.lookup(!.SolverVarMap, ThenVarId, ThenVar0),
ThenVar0 = solver_var(ThenCntAll, ThenCntPoss0, ThenValues0),
( if some_value_is_possible(ThenValues0, ReqThenValueIds) then
( if IfCntPoss0 = 1 then
% We know that (IfVarId = IfValueId). We can therefore
% impose (ThenVarId in ReqThenValueIds). This won't need
% to be imposed again.
KeepReq = no,
ReqAppl = requirement_application(ReqId, ReqDesc,
narrow_then_values),
restrict_possibilities_to(ReqThenValueIds, ReqAppl,
0, ThenCntPoss, ThenValues0, ThenValues),
( if ThenCntPoss < ThenCntPoss0 then
trace [compile_time(flag("debug_solver")), io(!TIO)] (
ReqId = requirement_id(ReqIdNum),
ThenVarName = string.string(ThenVarId),
ThenValueNames0 = list_poss_values(ThenValues0),
ThenValueNames = list_poss_values(ThenValues),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr, "Req %d (%s) updates then_var %s\n",
[i(ReqIdNum), s(ReqDesc), s(ThenVarName)], !TIO),
io.format(StdErr, " %s -> %s\n\n",
[s(ThenValueNames0), s(ThenValueNames)], !TIO)
),
ThenVar = solver_var(ThenCntAll, ThenCntPoss, ThenValues),
map.det_update(ThenVarId, ThenVar, !SolverVarMap),
!:Changed = changed,
( if ThenCntPoss = 0 then
!:FoundFailure = found_failure
else
true
)
else
% The condition (ThenVarId in ReqThenValueIds)
% already held, so nothing has changed.
trace [compile_time(flag("debug_solver")), io(!TIO)] (
ReqId = requirement_id(ReqIdNum),
ThenVarName = string.string(ThenVarId),
ThenValueNames0 = list_poss_values(ThenValues0),
ThenValueNames = list_poss_values(ThenValues),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr,
"Req %d (%s) pre-holds for then_var %s\n",
[i(ReqIdNum), s(ReqDesc), s(ThenVarName)], !TIO),
io.format(StdErr,
" %s -> %s\n\n",
[s(ThenValueNames0), s(ThenValueNames)], !TIO)
)
)
else
KeepReq = yes
)
else
% Since (ThenVarId in ReqThenValueIds) is false,
% we can impose (IfVarId = IfValueId) being false as well.
% This won't need to be imposed again.
KeepReq = no,
IfCntPoss = IfCntPoss0 - 1,
ReqAppl = requirement_application(ReqId, ReqDesc, delete_if_value),
set_value_to_not_possible(IfValueId, ReqAppl, IfValues0, IfValues),
trace [compile_time(flag("debug_solver")), io(!TIO)] (
ReqId = requirement_id(ReqIdNum),
IfVarName = string.string(IfVarId),
IfValueNames0 = list_poss_values(IfValues0),
IfValueNames = list_poss_values(IfValues),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr, "Req %d (%s) updates if_var %s\n",
[i(ReqIdNum), s(ReqDesc), s(IfVarName)], !TIO),
io.format(StdErr, " %s -> %s\n\n",
[s(IfValueNames0), s(IfValueNames)], !TIO)
),
IfVar = solver_var(IfCntAll, IfCntPoss, IfValues),
map.det_update(IfVarId, IfVar, !SolverVarMap),
!:Changed = changed,
( if IfCntPoss = 0 then
!:FoundFailure = found_failure
else
true
)
)
else
% We already know that (IfVarId = IfValueId) is false.
% Since false implies anything, the requirement is already met.
trace [compile_time(flag("debug_solver")), io(!TIO)] (
ReqId = requirement_id(ReqIdNum),
IfVarName = string.string(IfVarId),
IfValueName = string.string(IfValueId),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr, "Deleting Req %d (%s): %s is not %s\n\n",
[i(ReqIdNum), s(ReqDesc), s(IfVarName), s(IfValueName)], !TIO)
),
KeepReq = no
),
(
KeepReq = no
;
KeepReq = yes,
!:RevRequirements = [Requirement | !.RevRequirements]
),
propagate_pass(Requirements, !RevRequirements, !SolverVarMap,
!Changed, !FoundFailure).
:- pred some_value_is_possible(list(solver_var_value)::in,
list(solver_var_value_id)::in) is semidet.
some_value_is_possible(Values, [SearchValueId | SearchValueIds]) :-
( if is_value_possible(Values, SearchValueId, is_possible) then
true
else
some_value_is_possible(Values, SearchValueIds)
).
:- pred is_value_possible(list(solver_var_value)::in,
solver_var_value_id::in, solver_var_value_possible::out) is det.
is_value_possible([], _, _) :-
unexpected($pred, "did not find value").
is_value_possible([Value | Values], SearchValueId, Possible) :-
Value = solver_var_value(ValueId, ValuePossible),
( if ValueId = SearchValueId then
Possible = ValuePossible
else
is_value_possible(Values, SearchValueId, Possible)
).
:- pred set_value_to_not_possible(solver_var_value_id::in,
requirement_application::in,
list(solver_var_value)::in, list(solver_var_value)::out) is det.
set_value_to_not_possible(_SetValueId, _ReqAppl, [], _) :-
unexpected($pred, "value not found").
set_value_to_not_possible(SetValueId, ReqAppl,
[HeadValue0 | TailValues0], Values) :-
HeadValue0 = solver_var_value(ValueId, _Possible0),
( if SetValueId = ValueId then
Possible = not_possible(npw_requirement(ReqAppl)),
HeadValue = solver_var_value(ValueId, Possible),
Values = [HeadValue | TailValues0]
else
set_value_to_not_possible(SetValueId, ReqAppl,
TailValues0, TailValues),
Values = [HeadValue0 | TailValues]
).
:- pred restrict_possibilities_to(list(solver_var_value_id)::in,
requirement_application::in, int::in, int::out,
list(solver_var_value)::in, list(solver_var_value)::out) is det.
restrict_possibilities_to(!.SetValueIds, _ReqAppl, !CntPoss, [], []) :-
expect(unify(!.SetValueIds, []), $pred, "value not found").
restrict_possibilities_to(!.SetValueIds, ReqAppl, !CntPoss,
[HeadValue0 | TailValues0], [HeadValue | TailValues]) :-
HeadValue0 = solver_var_value(ValueId, Possible0),
( if list.delete_first(!.SetValueIds, ValueId, !:SetValueIds) then
(
Possible0 = is_possible,
!:CntPoss = !.CntPoss + 1
;
Possible0 = not_possible(_)
),
HeadValue = HeadValue0
else
Possible = not_possible(npw_requirement(ReqAppl)),
HeadValue = solver_var_value(ValueId, Possible)
),
restrict_possibilities_to(!.SetValueIds, ReqAppl, !CntPoss,
TailValues0, TailValues).
%---------------------------------------------------------------------------%
:- func list_poss_values(list(solver_var_value)) = string.
list_poss_values(SolverVarValues) = Str :-
accumulate_poss_value_strings(SolverVarValues, [], RevPossStrs),
list.reverse(RevPossStrs, PossStrs),
Str = "[" ++ string.join_list(", ", PossStrs) ++ "]".
:- pred accumulate_poss_value_strings(list(solver_var_value)::in,
list(string)::in, list(string)::out) is det.
accumulate_poss_value_strings([], !RevPossStrs).
accumulate_poss_value_strings([SolverVarValue | SolverVarValues],
!RevPossStrs) :-
SolverVarValue = solver_var_value(ValueId, Possible),
(
Possible = is_possible,
!:RevPossStrs = [string.string(ValueId) | !.RevPossStrs]
;
Possible = not_possible(_)
),
accumulate_poss_value_strings(SolverVarValues, !RevPossStrs).
%---------------------------------------------------------------------------%
:- pred label_step(list(solver_var_id)::in, list(solver_var_id)::out,
solver_var_map::in, solver_var_map::out) is det.
label_step(!SolverVarPriorities, !SolverMap) :-
find_first_undetermined_var(!SolverVarPriorities, !.SolverMap,
FirstVarId, FirstVar0),
FirstVar0 = solver_var(CntAll, _CntPoss0, FirstValues0),
find_first_possible_value_and_commit(FirstVarId,
FirstValues0, FirstValues),
CntPoss = 1,
FirstVar = solver_var(CntAll, CntPoss, FirstValues),
map.det_update(FirstVarId, FirstVar, !SolverMap).
:- pred find_first_undetermined_var(
list(solver_var_id)::in, list(solver_var_id)::out,
solver_var_map::in, solver_var_id::out, solver_var::out) is det.
find_first_undetermined_var([], _, _, _, _) :-
unexpected($pred, "no undetermined var").
find_first_undetermined_var([SolverVarId | SolverVarIds], LaterSolverVarIds,
SolverMap, FirstVarId, FirstVar) :-
map.lookup(SolverMap, SolverVarId, SolverVar),
SolverVar = solver_var(_CntAll, CntPoss, _Values),
( if CntPoss > 1 then
FirstVarId = SolverVarId,
FirstVar = SolverVar,
LaterSolverVarIds = SolverVarIds
else
find_first_undetermined_var(SolverVarIds, LaterSolverVarIds,
SolverMap, FirstVarId, FirstVar)
).
:- pred find_first_possible_value_and_commit(solver_var_id::in,
list(solver_var_value)::in, list(solver_var_value)::out) is det.
find_first_possible_value_and_commit(_VarId, [], []) :-
unexpected($pred, "no possible value").
find_first_possible_value_and_commit(VarId, [Value0 | Values0],
[Value | Values]) :-
Value0 = solver_var_value(ValueId, Possible0),
(
Possible0 = is_possible,
trace [compile_time(flag("debug_solver")), io(!TIO)] (
solver_var_name(VarName, VarId),
solver_var_value_name(ValueName, ValueId),
io.stderr_stream(StdErr, !TIO),
io.format(StdErr, "\nLABELING sets %s to %s\n",
[s(VarName), s(ValueName)], !TIO)
),
Value = Value0,
set_values_not_possible_labeling(Values0, Values)
;
Possible0 = not_possible(_),
Value = Value0,
find_first_possible_value_and_commit(VarId, Values0, Values)
).
:- pred set_values_not_possible_labeling(
list(solver_var_value)::in, list(solver_var_value)::out) is det.
set_values_not_possible_labeling([], []).
set_values_not_possible_labeling([Value0 | Values0], [Value | Values]) :-
Value0 = solver_var_value(ValudId, Possible0),
(
Possible0 = is_possible,
Possible = not_possible(npw_labeling),
Value = solver_var_value(ValudId, Possible)
;
Possible0 = not_possible(_),
Value = Value0
),
set_values_not_possible_labeling(Values0, Values).
%---------------------------------------------------------------------------%
:- pred are_we_at_solution(list(requirement)::in, solver_var_map::in,
maybe(solution)::out) is det.
are_we_at_solution(Requirements, SolverVarMap, MaybeSoln) :-
map.foldl2(cnt_poss_classes, SolverVarMap, [], ZeroCntVarIds, 0, NumMore),
(
ZeroCntVarIds = [HeadZeroCntVarId | TailZeroCntVarIds],
FailureInfo = failure_info(Requirements, SolverVarMap,
one_or_more(HeadZeroCntVarId, TailZeroCntVarIds)),
MaybeSoln = yes(soln_failure(FailureInfo))
;
ZeroCntVarIds = [],
( if NumMore = 0 then
map.foldl(accumulate_the_one_poss_value, SolverVarMap,
[], OnePossValues),
map.from_rev_sorted_assoc_list(OnePossValues, SuccessSoln),
MaybeSoln = yes(soln_success(SuccessSoln))
else
MaybeSoln = no
)
).
:- pred cnt_poss_classes(solver_var_id::in, solver_var::in,
list(solver_var_id)::in, list(solver_var_id)::out,
int::in, int::out) is det.
cnt_poss_classes(SolverVarId, SolverVar, !ZeroCntVarIds, !NumMore) :-
SolverVar = solver_var(_CntAll, CntPoss, _Values),
( if CntPoss = 0 then
!:ZeroCntVarIds = [SolverVarId | !.ZeroCntVarIds]
else if CntPoss = 1 then
true
else
!:NumMore = !.NumMore + 1
).
:- pred accumulate_the_one_poss_value(solver_var_id::in, solver_var::in,
assoc_list(solver_var_id, solver_var_value_id)::in,
assoc_list(solver_var_id, solver_var_value_id)::out) is det.
accumulate_the_one_poss_value(VarId, SolverVar, !OnePossValues) :-
SolverVar = solver_var(_CntAll, _CntPoss, Values),
get_poss_values(Values, PossValueIds),
( if PossValueIds = [ValueId] then
!:OnePossValues = [VarId - ValueId | !.OnePossValues]
else
unexpected($pred, "number of possible values is not one")
).
:- pred get_poss_values(list(solver_var_value)::in,
list(solver_var_value_id)::out) is det.
get_poss_values([], []).
get_poss_values([SolverVarValue | SolverVarValues], PossValueIds) :-
get_poss_values(SolverVarValues, PossValueIdsTail),
SolverVarValue = solver_var_value(ValueId, Possible),
(
Possible = is_possible,
PossValueIds = [ValueId | PossValueIdsTail]
;
Possible = not_possible(_),
PossValueIds = PossValueIdsTail
).
%---------------------------------------------------------------------------%
solve_best_installed_grade(SolverInfo, Commit, InstalledGrades0, SolveCounts,
InstalledGradeSoln) :-
list.sort_and_remove_dups(InstalledGrades0, InstalledGrades),
SolverInfo = solver_info(Requirements, SolverVarPriorities, SolverVarMap0),
SolveCounts0 = solve_counts(0, 0, 0),
propagate_to_fixpoint(Requirements, _Requirements,
SolverVarMap0, SolverVarMap, SolveCounts0, SolveCounts),
are_we_at_solution(Requirements, SolverVarMap, MaybeSoln),
(
MaybeSoln = yes(Soln),
(
Soln = soln_failure(FailureInfo),
InstalledGradeSoln =
installed_grade_spec_is_inconsistent(FailureInfo)
;
Soln = soln_success(SuccMap),
map.to_sorted_assoc_list(SuccMap, SuccPairs),
list.filter(match_success_map(SuccPairs), InstalledGrades,
MatchingInstalledGrades),
(
MatchingInstalledGrades = [],
InstalledGradeSoln = no_such_installed_grade
;
MatchingInstalledGrades = [MatchingInstalledGrade],
InstalledGradeSoln =
installed_grade_success(MatchingInstalledGrade)
;
MatchingInstalledGrades = [_, _ | _],
% The same grade cannot occur in InstalledGrades twice.
unexpected($pred, "MatchingInstalledGrades = [_, _ | _]")
)
)
;
MaybeSoln = no,
list.filter(
is_installed_grade_viable(SolverVarMap, SolverVarPriorities),
InstalledGrades, ViableInstalledGrades),
(
ViableInstalledGrades = [],
InstalledGradeSoln = no_such_installed_grade
;
ViableInstalledGrades =
[HeadViableInstalledGrade | TailViableInstalledGrades],
pick_best_viable_grade(SolverVarMap, SolverVarPriorities, Commit,
HeadViableInstalledGrade, TailViableInstalledGrades,
MaybeBestInstalledGrade),
(
MaybeBestInstalledGrade = yes(BestInstalledGrade),
InstalledGradeSoln =
installed_grade_success(BestInstalledGrade)
;
MaybeBestInstalledGrade = no,
% XXX This shouldn't happen with should_not_commit,
% but may (or may not) happen with should_commit. Let's see.
InstalledGradeSoln = no_such_installed_grade
)
)
).
:- pred match_success_map(assoc_list(solver_var_id, solver_var_value_id)::in,
installed_grade::in) is semidet.
match_success_map(SuccPairs, InstalledGrade) :-
InstalledGrade = installed_grade(_GradeName, GradeSuccMap),
map.to_sorted_assoc_list(GradeSuccMap, GradeSuccPairs),
SuccPairs = GradeSuccPairs.
:- pred is_installed_grade_viable(solver_var_map::in,
list(solver_var_id)::in, installed_grade::in) is semidet.
is_installed_grade_viable(_SolverVarMap, [], _InstalledGrade).
is_installed_grade_viable(SolverVarMap, [VarId | VarIds], InstalledGrade) :-
InstalledGrade = installed_grade(_GradeName, GradeSuccMap),
map.lookup(SolverVarMap, VarId, SolverVar),
map.lookup(GradeSuccMap, VarId, GradeValueId),
SolverVar = solver_var(_CntAll, _CntPoss, Values),
is_value_possible(GradeValueId, Values),
is_installed_grade_viable(SolverVarMap, VarIds, InstalledGrade).
:- pred is_value_possible(solver_var_value_id::in,
list(solver_var_value)::in) is semidet.
is_value_possible(GradeValueId, [Value | Values]) :-
Value = solver_var_value(ValueId, Possible),
( if GradeValueId = ValueId then
Possible = is_possible
else
is_value_possible(GradeValueId, Values)
).
:- pred pick_best_viable_grade(solver_var_map::in,
list(solver_var_id)::in, should_commit::in,
installed_grade::in, list(installed_grade)::in,
maybe(installed_grade)::out) is det.
pick_best_viable_grade(SolverVarMap0, SolverVarPriorities, Commit,
HeadViableInstalledGrade, TailViableInstalledGrades,
MaybeBestInstalledGrade) :-
(
TailViableInstalledGrades = [],
MaybeBestInstalledGrade = yes(HeadViableInstalledGrade)
;
TailViableInstalledGrades = [_ | _],
InstalledGrades =
[HeadViableInstalledGrade | TailViableInstalledGrades],
pick_first_var_with_viable_choice(InstalledGrades, SolverVarMap0,
SolverVarPriorities, SelectedVarId, SelectedVarViableValueIds,
LaterVarIds),
SelectedVarViableValueIds =
one_or_more(FirstViableValueId, LaterViableValueIds),
pick_first_viable_value(SolverVarMap0, SolverVarPriorities, Commit,
InstalledGrades, SelectedVarId, LaterVarIds,
FirstViableValueId, LaterViableValueIds, MaybeBestInstalledGrade)
).
:- pred pick_first_viable_value(solver_var_map::in,
list(solver_var_id)::in, should_commit::in, list(installed_grade)::in,
solver_var_id::in, list(solver_var_id)::in,
solver_var_value_id::in, list(solver_var_value_id)::in,
maybe(installed_grade)::out) is det.
pick_first_viable_value(SolverVarMap0, SolverVarPriorities, Commit,
InstalledGrades, SelectedVarId, LaterVarIds,
FirstViableValueId, LaterViableValueIds, MaybeBestInstalledGrade) :-
assign_var_in_map(npw_labeling, SelectedVarId, FirstViableValueId,
SolverVarMap0, SolverVarMap1),
list.filter(
is_installed_grade_viable(SolverVarMap1, SolverVarPriorities),
InstalledGrades, FirstValueInstalledGrades),
(
FirstValueInstalledGrades =
[HeadFirstInstalledGrade | TailFirstInstalledGrades]
;
FirstValueInstalledGrades = [],
unexpected($pred, "FirstValueInstalledGrades = []")
),
pick_best_viable_grade(SolverVarMap1, LaterVarIds, Commit,
HeadFirstInstalledGrade, TailFirstInstalledGrades,
FirstMaybeBestInstalledGrade),
(
FirstMaybeBestInstalledGrade = yes(_),
MaybeBestInstalledGrade = FirstMaybeBestInstalledGrade
;
FirstMaybeBestInstalledGrade = no,
(
Commit = should_commit,
MaybeBestInstalledGrade = FirstMaybeBestInstalledGrade
;
Commit = should_not_commit,
(
LaterViableValueIds = [],
MaybeBestInstalledGrade = FirstMaybeBestInstalledGrade
;
LaterViableValueIds =
[FirstLaterViableValueId | LaterLaterViableValueIds],
pick_first_viable_value(SolverVarMap0, SolverVarPriorities,
Commit, InstalledGrades, SelectedVarId, LaterVarIds,
FirstLaterViableValueId, LaterLaterViableValueIds,
MaybeBestInstalledGrade)
)
)
).
:- pred pick_first_var_with_viable_choice(list(installed_grade)::in,
solver_var_map::in, list(solver_var_id)::in,
solver_var_id::out, one_or_more(solver_var_value_id)::out,
list(solver_var_id)::out) is det.
pick_first_var_with_viable_choice(_InstalledGrades, _SolverVarMap, [],
_, _, _) :-
unexpected($pred, "none of the viable installed grades are really viable").
pick_first_var_with_viable_choice(InstalledGrades, SolverVarMap,
[VarId | VarIds], SelectedVarId, SelectedVarViableValueIds,
LaterVarIds) :-
map.lookup(SolverVarMap, VarId, SolverVar),
SolverVar = solver_var(_CntAll, CntPoss, Values),
( if
CntPoss > 1,
list.filter_map(
is_value_possible_and_available(InstalledGrades, VarId),
Values, ViableValueIds),
ViableValueIds = [HeadViableValueId | TailViableValueIds]
then
SelectedVarId = VarId,
SelectedVarViableValueIds =
one_or_more(HeadViableValueId, TailViableValueIds),
LaterVarIds = VarIds
else
pick_first_var_with_viable_choice(InstalledGrades, SolverVarMap,
VarIds, SelectedVarId, SelectedVarViableValueIds, LaterVarIds)
).
:- pred is_value_possible_and_available(list(installed_grade)::in,
solver_var_id::in, solver_var_value::in, solver_var_value_id::out)
is semidet.
is_value_possible_and_available(InstalledGrades, VarId, Value, ValueId) :-
Value = solver_var_value(ValueId, Possible),
Possible = is_possible,
is_value_available(InstalledGrades, VarId, ValueId).
:- pred is_value_available(list(installed_grade)::in,
solver_var_id::in, solver_var_value_id::in) is semidet.
is_value_available([InstalledGrade | InstalledGrades], VarId, ValueId) :-
InstalledGrade = installed_grade(_GradeName, GradeSuccMap),
map.lookup(GradeSuccMap, VarId, GradeValueId),
( if ValueId = GradeValueId then
true
else
is_value_available(InstalledGrades, VarId, ValueId)
).
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
solver_var_map_to_str(Prefix, SolverVarMap) = Str :-
map.to_sorted_assoc_list(SolverVarMap, SolverAssocList),
SolverVarStrs = list.map(solver_var_pair_to_str(Prefix), SolverAssocList),
Str = string.append_list(SolverVarStrs).
:- func solver_var_pair_to_str(string, pair(solver_var_id, solver_var))
= string.
solver_var_pair_to_str(Prefix, SolverVarName - SolverVar) = Str :-
SolverVar = solver_var(_CntAll, _CntPoss, _Values),
Str = Prefix ++ solver_var_to_str(SolverVarName, SolverVar).
:- func solver_var_to_str(solver_var_id, solver_var) = string.
solver_var_to_str(VarId, SolverVar) = Str :-
SolverVar = solver_var(_CntAll, CntPoss, Values),
solver_var_name(VarName, VarId),
ValuesStrs = list.map(solver_var_value_to_str(CntPoss), Values),
ValuesStr = string.join_list(", ", ValuesStrs),
expect(unify(CntPoss, count_possible_values(Values)), $pred,
"CntPoss mismatch"),
string.format("solver var %s: %d possible\n\t%s\n",
[s(VarName), i(CntPoss), s(ValuesStr)], Str).
:- func solver_var_value_to_str(int, solver_var_value) = string.
solver_var_value_to_str(CntPoss, SolverVarValue) = Str :-
SolverVarValue = solver_var_value(ValueId, Possible),
solver_var_value_name(ValueName, ValueId),
(
Possible = is_possible,
( if CntPoss = 1 then
string.format("%s yes", [s(ValueName)], Str)
else
string.format("%s maybe", [s(ValueName)], Str)
)
;
Possible = not_possible(WhyNot),
(
WhyNot = npw_config,
string.format("%s no (config)", [s(ValueName)], Str)
;
WhyNot = npw_user,
string.format("%s no (user)", [s(ValueName)], Str)
;
WhyNot = npw_requirement(ReqAppl),
ReqAppl = requirement_application(ReqId, _ReqDesc, ReqDir),
ReqId = requirement_id(ReqIdNum),
( ReqDir = narrow_then_values, ReqDirStr = "narrow_then_values"
; ReqDir = delete_if_value, ReqDirStr = "delete_if_value"
),
string.format("%s no (req %d, %s)",
[s(ValueName), i(ReqIdNum), s(ReqDirStr)], Str)
;
WhyNot = npw_labeling,
string.format("%s no (labeling)", [s(ValueName)], Str)
)
).
:- func count_possible_values(list(solver_var_value)) = int.
count_possible_values([]) = 0.
count_possible_values([SolverVarValue | SolverVarValues]) = N :-
NTail = count_possible_values(SolverVarValues),
SolverVarValue = solver_var_value(_Name, Possible),
(
Possible = is_possible,
N = NTail + 1
;
Possible = not_possible(_),
N = NTail
).
%---------------------------------------------------------------------------%
soln_to_str(Prefix, Soln) = Str :-
(
Soln = soln_failure(FailureInfo),
FailureStr = Prefix ++ "FAILURE\n",
( if Prefix = "" then
IndentStr = " "
else
IndentStr = Prefix
),
FailureTrees = failure_info_to_failure_trees(FailureInfo),
FailureTrees = one_or_more(HeadFailureTree, TailFailureTrees),
HeadFailureStr = failure_tree_to_string(Prefix, IndentStr,
HeadFailureTree),
TailFailureStrs = list.map(failure_tree_to_string(Prefix, IndentStr),
TailFailureTrees),
Str = FailureStr ++ HeadFailureStr ++
string.append_list(TailFailureStrs) ++ "\n"
;
Soln = soln_success(SuccMap),
SuccessStr = Prefix ++ "SUCCESS\n",
map.to_assoc_list(SuccMap, SuccessValues),
SuccessValueStrs =
list.map(success_value_to_str(Prefix), SuccessValues),
Str = SuccessStr ++ string.append_list(SuccessValueStrs)
).
:- func failure_tree_to_string(string, string, failure_tree) = string.
failure_tree_to_string(CurIndentStr, EachIndentStr, FailureTree) = Str :-
FailureTree = failure_tree(VarId, WhyNots),
solver_var_name(VarName, VarId),
(
WhyNots = [],
string.format(
"%sconfiguration and user settings leave no valid value for %s\n",
[s(CurIndentStr), s(VarName)], Str)
;
WhyNots = [HeadWhyNot | TailWhyNots],
(
TailWhyNots = [],
HeadWhyNot = why_var_is_not_value(_ValueId, _ReqId, ReqDesc,
SubTrees),
% solver_var_value_name(ValueName, ValueId),
SubTreeStrs = list.map(
failure_tree_to_string(CurIndentStr ++ EachIndentStr,
EachIndentStr),
SubTrees),
Str = CurIndentStr ++ ReqDesc ++ "\n" ++
string.append_list(SubTreeStrs)
;
TailWhyNots = [_ | _],
HeadStr = failure_tree_why_not_to_string(CurIndentStr,
EachIndentStr, VarId, VarName, HeadWhyNot),
TailStrs = list.map(
failure_tree_why_not_to_string(CurIndentStr, EachIndentStr,
VarId, VarName),
TailWhyNots),
Str = string.append_list([HeadStr | TailStrs])
)
).
:- func failure_tree_why_not_to_string(string, string, solver_var_id,
string, why_var_is_not_value) = string.
failure_tree_why_not_to_string(CurIndentStr, EachIndentStr, _VarId, VarName,
WhyNot) = Str :-
WhyNot = why_var_is_not_value(ValueId, _ReqId, ReqDesc, SubTrees),
solver_var_value_name(ValueName, ValueId),
string.format("%sThe variable %s may not be %s because: %s\n",
[s(CurIndentStr), s(VarName), s(ValueName), s(ReqDesc)], WhyNotStr),
SubTreeStrs = list.map(
failure_tree_to_string(CurIndentStr ++ EachIndentStr, EachIndentStr),
SubTrees),
Str = WhyNotStr ++ string.append_list(SubTreeStrs).
:- func success_value_to_str(string,
pair(solver_var_id, solver_var_value_id)) = string.
success_value_to_str(Prefix, VarId - ValueId) = Str :-
solver_var_name(VarName, VarId),
solver_var_value_name(ValueName, ValueId),
string.format("%s%s = %s\n", [s(Prefix), s(VarName), s(ValueName)], Str).
%---------------------------------------------------------------------------%
:- type failure_info
---> failure_info(
list(requirement),
% The full, unmodified list of requirements involved in
% the solution process. We use this to map requirement_ids
% to the requirements themselves.
solver_var_map,
% The solver var map when we discovered the inconsistency.
one_or_more(solver_var_id)
% The solver variables that have no possible values.
).
failure_info_to_failure_trees(FailureInfo) = FailureTrees :-
FailureInfo = failure_info(_Requirements, _SolverVarMap, ZeroCntVarIds),
ZeroCntVarIds = one_or_more(HeadZeroCntVarId, TailZeroCntVarIds),
zero_count_var_to_failure_tree(FailureInfo,
HeadZeroCntVarId, HeadFailureTree),
list.map(zero_count_var_to_failure_tree(FailureInfo),
TailZeroCntVarIds, TailFailureTrees),
FailureTrees = one_or_more(HeadFailureTree, TailFailureTrees).
:- pred zero_count_var_to_failure_tree(failure_info::in,
solver_var_id::in, failure_tree::out) is det.
zero_count_var_to_failure_tree(FailureInfo, ZeroCntVarId, FailureTree) :-
FailureInfo = failure_info(_Requirements, SolverVarMap, _ZeroCntVarIds),
map.lookup(SolverVarMap, ZeroCntVarId, SolverVar),
SolverVar = solver_var(_CntAll, _CntPoss, Values),
list.foldl(accumulate_why_var_is_not_values(FailureInfo, ZeroCntVarId),
Values, [], RevWhyNots),
list.reverse(RevWhyNots, WhyNots),
FailureTree = failure_tree(ZeroCntVarId, WhyNots).
:- pred var_not_values_to_failure_tree(failure_info::in,
solver_var_id::in, set(solver_var_value_id)::in, failure_tree::out) is det.
var_not_values_to_failure_tree(FailureInfo, VarId, ValueIds, FailureTree) :-
FailureInfo = failure_info(_Requirements, SolverVarMap, _ZeroCntVarIds),
map.lookup(SolverVarMap, VarId, SolverVar),
SolverVar = solver_var(_CntAll, _CntPoss, Values),
list.filter(solver_var_value_in_set(ValueIds), Values, ValuesInSet),
list.foldl(accumulate_why_var_is_not_values(FailureInfo, VarId),
ValuesInSet, [], RevWhyNots),
list.reverse(RevWhyNots, WhyNots),
FailureTree = failure_tree(VarId, WhyNots).
:- pred solver_var_value_in_set(set(solver_var_value_id)::in,
solver_var_value::in) is semidet.
solver_var_value_in_set(ValueIds, VarValue) :-
VarValue = solver_var_value(ValueId, _Possible),
set.contains(ValueIds, ValueId).
:- pred accumulate_why_var_is_not_values(failure_info::in,
solver_var_id::in, solver_var_value::in,
list(why_var_is_not_value)::in, list(why_var_is_not_value)::out) is det.
accumulate_why_var_is_not_values(FailureInfo, _VarId, VarValue, !RevWhyNots) :-
VarValue = solver_var_value(ValueId, Possible),
(
Possible = is_possible
;
Possible = not_possible(NotPossibleWhy),
(
NotPossibleWhy = npw_user
% Nothing to report; the user should already know
% why the solver var cannot be this value.
;
NotPossibleWhy = npw_config
% XXX Should we report this, and if yes, how?
;
NotPossibleWhy = npw_labeling,
% We should get here only if labelling has converted
% a solvable problem into an unsolvable one.
unexpected($pred, "npw_labeling")
;
NotPossibleWhy = npw_requirement(ReqAppl),
ReqAppl = requirement_application(ReqId, ReqDesc, ReqDir),
FailureInfo = failure_info(Requirements, _, _),
find_requirement_by_id(Requirements, ReqId, AppliedRequirement),
AppliedRequirement = requirement(_AppReqId, _AppReqDesc,
IfVarId, IfValueId, ThenVarId, ThenValueIds),
(
ReqDir = delete_if_value,
var_not_values_to_failure_tree(FailureInfo,
ThenVarId, set.list_to_set(ThenValueIds), SubTree)
;
ReqDir = narrow_then_values,
var_not_values_to_failure_tree(FailureInfo,
IfVarId, set.make_singleton_set(IfValueId), SubTree)
),
SubTree = failure_tree(_, SubWhyNots),
(
SubWhyNots = [],
SubTrees = []
;
SubWhyNots = [_ | _],
SubTrees = [SubTree]
),
WhyNot = why_var_is_not_value(ValueId, ReqId, ReqDesc, SubTrees),
!:RevWhyNots = [WhyNot | !.RevWhyNots]
)
).
:- pred find_requirement_by_id(list(requirement)::in, requirement_id::in,
requirement::out) is det.
find_requirement_by_id([], _, _) :-
unexpected($pred, "id not in list").
find_requirement_by_id([Requirement | Requirements], ReqId, IdRequirement) :-
( if Requirement ^ req_id = ReqId then
IdRequirement = Requirement
else
find_requirement_by_id(Requirements, ReqId, IdRequirement)
).
%---------------------------------------------------------------------------%
:- end_module grade_lib.grade_solver.
%---------------------------------------------------------------------------%
Reference in New Issue View Git Blame Copy Permalink