concretizer: emit facts for integrity constraints

lib/spack/spack/solver/asp.py

@@ -356,39 +356,6 @@ def rule(self, head, body):
             [atoms[s] for s in body_symbols] + rule_atoms
         )
 
-    def integrity_constraint(self, clauses, default_negated=None):
-        """Add an integrity constraint to the solver.
-
-        Args:
-            clauses: clauses to be added to the integrity constraint
-            default_negated: clauses to be added to the integrity
-                constraint after with a default negation
-        """
-        symbols, negated_symbols, atoms = _normalize(clauses), [], {}
-        if default_negated:
-            negated_symbols = _normalize(default_negated)
-
-        for s in symbols + negated_symbols:
-            atoms[s] = self.backend.add_atom(s)
-
-        symbols_str = ",".join(str(a) for a in symbols)
-        if negated_symbols:
-            negated_symbols_str = ",".join(
-                "not " + str(a) for a in negated_symbols
-            )
-            symbols_str += ",{0}".format(negated_symbols_str)
-        rule_str = ":- {0}.".format(symbols_str)
-        rule_atoms = self._register_rule_for_cores(rule_str)
-
-        # print rule before adding
-        self.out.write("{0}\n".format(rule_str))
-        self.backend.add_rule(
-            [],
-            [atoms[s] for s in symbols] +
-            [-atoms[s] for s in negated_symbols]
-            + rule_atoms
-        )
-
     def solve(
             self, solver_setup, specs, dump=None, nmodels=0,
             timers=False, stats=False, tests=False
@@ -588,11 +555,16 @@ def conflict_rules(self, pkg):
                 # TODO: of a rule and filter unwanted functions.
                 to_be_filtered = ['node_compiler_hard']
                 clauses = [x for x in clauses if x.name not in to_be_filtered]
-                external = fn.external(pkg.name)
 
-                self.gen.integrity_constraint(
+                # Emit facts based on clauses
-                    AspAnd(*clauses), AspAnd(external)
+                cond_id = self._condition_id_counter
-                )
+                self._condition_id_counter += 1
+                self.gen.fact(fn.conflict(cond_id, pkg.name))
+                for clause in clauses:
+                    self.gen.fact(fn.conflict_condition(
+                        cond_id, clause.name, *clause.args
+                    ))
+                self.gen.newline()
 
     def available_compilers(self):
         """Facts about available compilers."""

lib/spack/spack/solver/concretize.lp

@@ -59,6 +59,8 @@ dependency_conditions(P, D, T) :-
   dependency_conditions_hold(P, D, I),
   dependency_type(I, T).
 
+#defined dependency_type/2.
+
 % collect all the dependency conditions into a single conditional rule
 dependency_conditions_hold(Package, Dependency, ID) :-
   version(Package, Version)
@@ -82,6 +84,32 @@ dependency_conditions_hold(Package, Dependency, ID) :-
   dependency_condition(Package, Dependency, ID);
   node(Package).
 
+#defined dependency_condition/3.
+#defined required_dependency_condition/3.
+#defined required_dependency_condition/4.
+#defined required_dependency_condition/5.
+#defined required_dependency_condition/5.
+
+% general rules for conflicts
+:- node(Package) : conflict_condition(ID, "node", Package);
+   not external(Package) : conflict_condition(ID, "node", Package);
+   version(Package, Version) : conflict_condition(ID, "version", Package, Version);
+   version_satisfies(Package, Constraint) : conflict_condition(ID, "version_satisfies", Package, Constraint);
+   node_platform(Package, Platform) : conflict_condition(ID, "node_platform", Package, Platform);
+   node_os(Package, OS) : conflict_condition(ID, "node_os", Package, OS);
+   node_target(Package, Target) : conflict_condition(ID, "node_target", Package, Target);
+   variant_value(Package, Variant, Value) : conflict_condition(ID, "variant_value", Package, Variant, Value);
+   node_compiler(Package, Compiler) : conflict_condition(ID, "node_compiler", Package, Compiler);
+   node_compiler_version(Package, Compiler, Version) : conflict_condition(ID, "node_compiler_version", Package, Compiler, Version);
+   node_compiler_version_satisfies(Package, Compiler, Version) : conflict_condition(ID, "node_compiler_version_satisfies", Package, Compiler, Version);
+   node_flag(Package, FlagType, Flag) : conflict_condition(ID, "node_flag", Package, FlagType, Flag);
+   conflict(ID, Package).
+
+#defined conflict/2.
+#defined conflict_condition/3.
+#defined conflict_condition/4.
+#defined conflict_condition/5.
+
 % Implications from matching a dependency condition
 node(Dependency) :-
   dependency_conditions_hold(Package, Dependency, ID),
@@ -137,6 +165,9 @@ node_flag(Dependency, FlagType, Flag) :-
   depends_on(Package, Dependency),
   imposed_dependency_condition(ID, "node_flag", Dependency, FlagType, Flag).
 
+#defined imposed_dependency_condition/4.
+#defined imposed_dependency_condition/5.
+
 % if a virtual was required by some root spec, one provider is in the DAG
 1 { node(Package) : provides_virtual(Package, Virtual) } 1
  :- virtual_node(Virtual).