ASP-based solver: do not optimize on known dimensions

All the solution modes we use imply that we have to solve for all
the literals, except for "when possible".

Here we remove a minimization on the number of literals not
solved, and emit directly a fact when a literal *has* to be
solved.

4 files changed, 33 insertions, 30 deletions

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 56bf7b6a39..b602cdb6d4 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -779,6 +779,8 @@ class PyclingoDriver:
         self.control.load(os.path.join(parent_dir, "heuristic.lp"))
         self.control.load(os.path.join(parent_dir, "os_compatibility.lp"))
         self.control.load(os.path.join(parent_dir, "display.lp"))
+        if not setup.concretize_everything:
+            self.control.load(os.path.join(parent_dir, "when_possible.lp"))
         timer.stop("load")
 
         # Grounding is the first step in the solve -- it turns our facts
@@ -2360,8 +2362,8 @@ class SpackSolverSetup:
                         fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:])
                     )
 
-        if self.concretize_everything:
-            self.gen.fact(fn.concretize_everything())
+            if self.concretize_everything:
+                self.gen.fact(fn.solve_literal(idx))
 
     def _get_versioned_specs_from_pkg_requirements(self):
         """If package requirements mention versions that are not mentioned
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index 3268f581f7..ad5418b4be 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -7,10 +7,6 @@
 % This logic program implements Spack's concretizer
 %=============================================================================
 
-%-----------------------------------------------------------------------------
-% Map literal input specs to facts that drive the solve
-%-----------------------------------------------------------------------------
-
 #const root_node_id = 0.
 
 #const link_run = 0.
@@ -78,21 +74,9 @@ unification_set(SetID, VirtualNode) :- provider(PackageNode, VirtualNode), unifi
    not attr("virtual_node", node(ID2, Package)),
    max_nodes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1.
 
-% 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).
-
-% If concretize_everything() is a fact, then we cannot have unsolved specs
-:- literal_not_solved(ID), concretize_everything.
-
-% 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) }.
-
-opt_criterion(300, "number of input specs not concretized").
-#minimize{ 0@300: #true }.
-#minimize { 1@300,ID : literal_not_solved(ID) }.
+%-----------------------------------------------------------------------------
+% Map literal input specs to facts that drive the solve
+%-----------------------------------------------------------------------------
 
 % TODO: literals, at the moment, can only influence the "root" unification set. This needs to be extended later.
 
@@ -100,14 +84,14 @@ special_case("node_flag_source").
 special_case("depends_on").
 
 % Map constraint on the literal ID to facts on the node
-attr(Name, node(root_node_id, A1))             :- literal(LiteralID, Name, A1), literal_solved(LiteralID).
-attr(Name, node(root_node_id, A1), A2)         :- literal(LiteralID, Name, A1, A2), literal_solved(LiteralID).
-attr(Name, node(root_node_id, A1), A2, A3)     :- literal(LiteralID, Name, A1, A2, A3), literal_solved(LiteralID), not special_case(Name).
-attr(Name, node(root_node_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), literal_solved(LiteralID).
+attr(Name, node(root_node_id, A1))             :- literal(LiteralID, Name, A1), solve_literal(LiteralID).
+attr(Name, node(root_node_id, A1), A2)         :- literal(LiteralID, Name, A1, A2), solve_literal(LiteralID).
+attr(Name, node(root_node_id, A1), A2, A3)     :- literal(LiteralID, Name, A1, A2, A3), solve_literal(LiteralID), not special_case(Name).
+attr(Name, node(root_node_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), solve_literal(LiteralID).
 
 % Special cases where nodes occur in arguments other than A1
-attr("node_flag_source", node(root_node_id, A1), A2, node(root_node_id, A3)) :- literal(LiteralID, "node_flag_source", A1, A2, A3), literal_solved(LiteralID).
-attr("depends_on",       node(root_node_id, A1), node(root_node_id, A2), A3) :- literal(LiteralID, "depends_on",       A1, A2, A3), literal_solved(LiteralID).
+attr("node_flag_source", node(root_node_id, A1), A2, node(root_node_id, A3)) :- literal(LiteralID, "node_flag_source", A1, A2, A3), solve_literal(LiteralID).
+attr("depends_on",       node(root_node_id, A1), node(root_node_id, A2), A3) :- literal(LiteralID, "depends_on",       A1, A2, A3), solve_literal(LiteralID).
 
 #defined concretize_everything/0.
 #defined literal/1.
diff --git a/lib/spack/spack/solver/heuristic.lp b/lib/spack/spack/solver/heuristic.lp
index 7d923219aa..cd5d94978f 100644
--- a/lib/spack/spack/solver/heuristic.lp
+++ b/lib/spack/spack/solver/heuristic.lp
@@ -6,9 +6,6 @@
 %-----------------
 % Domain heuristic
 %-----------------
-#heuristic literal_solved(ID) : literal(ID). [1, sign]
-#heuristic literal_solved(ID) : literal(ID). [50, init]
-
 #heuristic attr("hash", node(0, Package), Hash) : literal(_, "root", Package). [45, init]
 #heuristic attr("root", node(0, Package)) : literal(_, "root", Package). [45, true]
 #heuristic attr("node", node(0, Package)) : literal(_, "root", Package). [45, true]
diff --git a/lib/spack/spack/solver/when_possible.lp b/lib/spack/spack/solver/when_possible.lp
new file mode 100644
index 0000000000..7a8ddfef1c
--- /dev/null
+++ b/lib/spack/spack/solver/when_possible.lp
@@ -0,0 +1,20 @@
+% Copyright 2013-2023 Lawrence Livermore National Security, LLC and other
+% Spack Project Developers. See the top-level COPYRIGHT file for details.
+%
+% SPDX-License-Identifier: (Apache-2.0 OR MIT)
+
+% Give clingo the choice to solve an input spec or not
+{ solve_literal(ID) } :- literal(ID).
+literal_not_solved(ID) :- not solve_literal(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 { solve_literal(ID) : literal(ID) }.
+
+opt_criterion(300, "number of input specs not concretized").
+#minimize{ 0@300: #true }.
+#minimize { 1@300,ID : literal_not_solved(ID) }.
+
+#heuristic literal_solved(ID) : literal(ID). [1, sign]
+#heuristic literal_solved(ID) : literal(ID). [50, init]