zhangyiss/spack
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

solver: treat literals as conditions

Browse Source
This commit is contained in:
Gregory Becker 2022-12-12 15:51:38 -08:00
parent 004ff9d4e2
commit 59acfe4f0b
2 changed files with 20 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
lib/spack/spack/solver/asp.py
View File

@ -2300,17 +2300,26 @@ def setup(self, driver, specs, reuse=None):
self.define_target_constraints() self.define_target_constraints()
def literal_specs(self, specs): def literal_specs(self, specs):
for idx, spec in enumerate(specs): for spec in specs:
self.gen.h2("Spec: %s" % str(spec)) self.gen.h2("Spec: %s" % str(spec))
self.gen.fact(fn.literal(idx))
self.gen.fact(fn.literal(idx, "virtual_root" if spec.virtual else "root", spec.name)) # cannot use self.condition because it requires condition requirements
condition_id = next(self._condition_id_counter)
self.gen.fact(fn.condition(condition_id, "%s is provided as input spec" % spec))
self.gen.fact(fn.literal(condition_id))
self.gen.fact(fn.condition_requirement(condition_id, "literal_solved", condition_id))
self.gen.fact(fn.imposed_constraint(
condition_id, "virtual_root" if spec.virtual else "root", spec.name
))
for clause in self.spec_clauses(spec): for clause in self.spec_clauses(spec):
self.gen.fact(fn.literal(idx, *clause.args)) self.gen.fact(fn.imposed_constraint(condition_id, *clause.args))
if clause.args[0] == "variant_set": if clause.args[0] == "variant_set":
self.gen.fact( self.gen.fact(fn.imposed_constraint(
fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:]) condition_id, "variant_default_value_from_cli", *clause.args[1:]
) ))
if self.concretize_everything: if self.concretize_everything:
self.gen.fact(fn.concretize_everything()) self.gen.fact(fn.concretize_everything())
@ -2404,6 +2413,7 @@ class SpecBuilder(object):
r"^virtual_node$", r"^virtual_node$",
r"^virtual_root$", r"^virtual_root$",
r"^.*holds?$", r"^.*holds?$",
r"^literal.*$",
] ]
) )
) )

16
lib/spack/spack/solver/concretize.lp
View File

@ -12,8 +12,8 @@
%----------------------------------------------------------------------------- %-----------------------------------------------------------------------------
% Give clingo the choice to solve an input spec or not % Give clingo the choice to solve an input spec or not
{ literal_solved(ID) } :- literal(ID). { attr("literal_solved", ID) } :- literal(ID).
literal_not_solved(ID) :- not literal_solved(ID), literal(ID). literal_not_solved(ID) :- not attr("literal_solved", ID), literal(ID).
% If concretize_everything() is a fact, then we cannot have unsolved specs % If concretize_everything() is a fact, then we cannot have unsolved specs
:- literal_not_solved(ID), concretize_everything. :- literal_not_solved(ID), concretize_everything.
@ -21,24 +21,14 @@ literal_not_solved(ID) :- not literal_solved(ID), literal(ID).
% Make a problem with "zero literals solved" unsat. This is to trigger % Make a problem with "zero literals solved" unsat. This is to trigger
% looking for solutions to the ASP problem with "errors", which results % looking for solutions to the ASP problem with "errors", which results
% in better reporting for users. See #30669 for details. % in better reporting for users. See #30669 for details.
1 { literal_solved(ID) : literal(ID) }. 1 { attr("literal_solved", ID) : literal(ID) }.
opt_criterion(300, "number of input specs not concretized"). opt_criterion(300, "number of input specs not concretized").
#minimize{ 0@300: #true }. #minimize{ 0@300: #true }.
#minimize { 1@300,ID : literal_not_solved(ID) }. #minimize { 1@300,ID : literal_not_solved(ID) }.
% Map constraint on the literal ID to the correct PSID
attr(Name, A1) :- literal(LiteralID, Name, A1), literal_solved(LiteralID).
attr(Name, A1, A2) :- literal(LiteralID, Name, A1, A2), literal_solved(LiteralID).
attr(Name, A1, A2, A3) :- literal(LiteralID, Name, A1, A2, A3), literal_solved(LiteralID).
attr(Name, A1, A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), literal_solved(LiteralID).
#defined concretize_everything/0. #defined concretize_everything/0.
#defined literal/1. #defined literal/1.
#defined literal/3.
#defined literal/4.
#defined literal/5.
#defined literal/6.
% Attributes for node packages which must have a single value % Attributes for node packages which must have a single value
attr_single_value("version"). attr_single_value("version").