From 59acfe4f0b78ee9fa65afda0f89cff76b330fa27 Mon Sep 17 00:00:00 2001 From: Gregory Becker Date: Mon, 12 Dec 2022 15:51:38 -0800 Subject: [PATCH] solver: treat literals as conditions --- lib/spack/spack/solver/asp.py | 24 +++++++++++++++++------- lib/spack/spack/solver/concretize.lp | 16 +++------------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index 66d790c7dd2..7a47aace422 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -2300,17 +2300,26 @@ def setup(self, driver, specs, reuse=None): self.define_target_constraints() def literal_specs(self, specs): - for idx, spec in enumerate(specs): + for spec in specs: 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): - self.gen.fact(fn.literal(idx, *clause.args)) + self.gen.fact(fn.imposed_constraint(condition_id, *clause.args)) if clause.args[0] == "variant_set": - self.gen.fact( - fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:]) - ) + self.gen.fact(fn.imposed_constraint( + condition_id, "variant_default_value_from_cli", *clause.args[1:] + )) if self.concretize_everything: self.gen.fact(fn.concretize_everything()) @@ -2404,6 +2413,7 @@ class SpecBuilder(object): r"^virtual_node$", r"^virtual_root$", r"^.*holds?$", + r"^literal.*$", ] ) ) diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index 98327dcc501..d2f2cdb6fb1 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/lib/spack/spack/solver/concretize.lp @@ -12,8 +12,8 @@ %----------------------------------------------------------------------------- % Give clingo the choice to solve an input spec or not -{ literal_solved(ID) } :- literal(ID). -literal_not_solved(ID) :- not literal_solved(ID), literal(ID). +{ attr("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 :- 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 % looking for solutions to the ASP problem with "errors", which results % 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"). #minimize{ 0@300: #true }. #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 literal/1. -#defined literal/3. -#defined literal/4. -#defined literal/5. -#defined literal/6. % Attributes for node packages which must have a single value attr_single_value("version").