From 66bda49c447f4031dd2274cc9901e09855289ac8 Mon Sep 17 00:00:00 2001
From: Gregory Becker <becker33@llnl.gov>
Date: Tue, 19 Apr 2022 15:33:32 -0700
Subject: [PATCH] solver: rework which facts are assumptions

---
 lib/spack/spack/error.py      |  4 ++--
 lib/spack/spack/main.py       |  2 +-
 lib/spack/spack/solver/asp.py | 25 +++++++++++++++++++------
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/lib/spack/spack/error.py b/lib/spack/spack/error.py
index 25ddccea1a5..bcb2aeb2186 100644
--- a/lib/spack/spack/error.py
+++ b/lib/spack/spack/error.py
@@ -10,9 +10,9 @@
 
 import llnl.util.tty as tty
 
-#: whether we should write stack traces or short error messages
+#: at what level we should write stack traces or short error messages
 #: this is module-scoped because it needs to be set very early
-debug = False
+debug = 0
 
 
 class SpackError(Exception):
diff --git a/lib/spack/spack/main.py b/lib/spack/spack/main.py
index feab2b6f818..7bee03dfcd1 100644
--- a/lib/spack/spack/main.py
+++ b/lib/spack/spack/main.py
@@ -490,7 +490,7 @@ def setup_main_options(args):
     # errors raised by spack.config.
 
     if args.debug:
-        spack.error.debug = True
+        spack.error.debug = args.debug
         spack.util.debug.register_interrupt_handler()
         spack.config.set('config:debug', True, scope='command_line')
         spack.util.environment.tracing_enabled = True
diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index a370ac4b517..e0f1e1c7aa7 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -504,13 +504,11 @@ def h2(self, name):
     def newline(self):
         self.out.write('\n')
 
-    def fact(self, head, assumption=False):
+    def fact(self, head):
         """ASP fact (a rule without a body).
 
         Arguments:
             head (AspFunction): ASP function to generate as fact
-            assumption (bool): If True and using cores, use this fact as a
-                choice point in ASP and include it in unsatisfiable cores
         """
         symbol = head.symbol() if hasattr(head, 'symbol') else head
 
@@ -518,9 +516,24 @@ def fact(self, head, assumption=False):
 
         atom = self.backend.add_atom(symbol)
 
-        # with `--show-cores=full or --show-cores=minimized, make all facts
-        # choices/assumptions, otherwise only if assumption=True
-        choice = self.cores and (full_cores or assumption)
+        assumption_names = [
+            'conflict', 'condition', 'error', 'variant',
+            'rule', 'deprecated', 'node_flag_set',
+            'node_compiler_version_set', 'node_compiler_set', 'variant_set',
+            'node_target_set', 'node_os_set', 'node_platform_set',
+            'node_platform_default', 'node_compiler_version_satisfies', 'node_version_satisfies',
+            'external_spec_selected', 'no_flags', 'variant_value', 'version',
+            'depends_on', 'hash', 'node_flag_compiler_default', 'node_flag_source',
+            'build', 'node', 'root',
+        ]
+
+        # At high debug levels, include internal errors in output
+        if spack.error.debug > 2:
+            assumption_names.append('internal_error')
+
+        # Only functions relevant for constructing good error messages are
+        # assumptions, and only when using cores.
+        choice = self.cores and symbol.name in assumption_names
 
         self.backend.add_rule([atom], [], choice=choice)
         if choice: