Coverage Summary for Class: CausalityAnalysis (it.unibo.tuprolog.argumentation.causality.runtime)

 package it.unibo.tuprolog.argumentation.causality.runtime
 
 import it.unibo.tuprolog.argumentation.core.Arg2pSolver
 import it.unibo.tuprolog.argumentation.core.Arg2pSolverFactory
 import it.unibo.tuprolog.argumentation.core.dsl.arg2pScope
 import it.unibo.tuprolog.argumentation.core.flags.ArgumentLabellingMode
 import it.unibo.tuprolog.argumentation.core.model.Argument
 import it.unibo.tuprolog.argumentation.core.model.Graph
 import it.unibo.tuprolog.argumentation.core.model.LabelledArgument
 import it.unibo.tuprolog.argumentation.core.model.mining.graph
 import it.unibo.tuprolog.argumentation.core.model.terms.TermValues
 import it.unibo.tuprolog.argumentation.core.runtime.settings.FlagsBuilder
 import it.unibo.tuprolog.argumentation.core.runtime.settings.Settings
 import it.unibo.tuprolog.argumentation.core.runtime.theory.RuleAnnotations
 import it.unibo.tuprolog.core.Atom
 import it.unibo.tuprolog.core.Clause
 import it.unibo.tuprolog.core.Struct
 import it.unibo.tuprolog.core.Term
 import it.unibo.tuprolog.core.parsing.parse
 import it.unibo.tuprolog.solve.ExecutionContext
 import it.unibo.tuprolog.solve.MutableSolver
 import it.unibo.tuprolog.solve.Solution
 import it.unibo.tuprolog.solve.primitive.Solve
 import it.unibo.tuprolog.theory.Theory
 import it.unibo.tuprolog.theory.parsing.parse
 import it.unibo.tuprolog.unify.Unificator
 import it.unibo.tuprolog.core.List as PlList
 
 private const val GRAPH_CACHE_SIZE = 256
 
 /**
  * The causal analysis of a theory, for the primitives of the causality module: the graphs of the theory and of its
  * interventions, labelled by a solver of its own with grounded semantics (the other flags those of the solver asking),
  * and the NESS and but-for checks on them. The theory is the static knowledge base of the solver asking
  * ([Solve.Request]); what it prints goes to the standard output of that solver.
  */
 internal class CausalityAnalysis {
     // The solver labelling the graphs, built at the first of them: a solver of arg2p not testing causality pays nothing
     private var labelling: MutableSolver? = null
 
     // The solver labelling the graphs, printing where the solver asking does
     private fun solverFor(request: Solve.Request<ExecutionContext>): MutableSolver {
         val output = request.context.standardOutput
         val solver =
             labelling ?: Arg2pSolverFactory
                 .solverOf(
                     Arg2pSolver.default(listOf(FlagsBuilder(graphExtensions = emptyList(), argumentLabellingMode = "grounded").create())),
                     theory = "",
                     output = output,
                 ).also { labelling = it }
         if (solver.standardOutput !== output) solver.setStandardOutput(output)
         return solver
     }
 
     // The same theory is solved over and over (the base theory, or the same intervention in different checks): the
     // graphs are only read afterwards, hence they are shared
     private val graphCache = mutableMapOf<Pair<String, String>, Graph>()
 
     /** The graph of [theory] for [query], labelled */
     private fun graphOf(
         request: Solve.Request<ExecutionContext>,
         theory: Theory,
         query: Term,
     ): Graph {
         // the identifiers of the clauses too: the same text is a different theory with them (see RuleAnnotations)
         val text = theory.toString(asPrologText = true) + theory.joinToString(",") { RuleAnnotations.of(it).orEmpty() }
         val key = text to query.toString()
         graphCache[key]?.let { return it }
         if (graphCache.size >= GRAPH_CACHE_SIZE) graphCache.clear()
         val solver = solverFor(request)
         solver.resetStaticKb()
         // the theory as it is, not parsed again from its text: its clauses keep their tags
         solver.loadStaticKb(theory)
         val solution = solver.solve(Struct.of("answerQuery", query)).first()
         // an error is not a graph: raised again, and not kept
         if (solution is Solution.Halt) throw solution.exception
         return solver.graph().also { graphCache[key] = it }
     }
 
     private fun concludes(
         argument: Argument,
         statement: Term,
     ) = Unificator.default.match(Term.parse(argument.conclusion, TermValues.operators), statement)
 
     private fun attackers(
         argument: Argument,
         graph: Graph,
     ): List<LabelledArgument> =
         graph.attacks
             .filter { it.target.identifier == argument.identifier }
             .map { attack -> graph.labellings.first { attack.attacker.identifier == it.argument.identifier } }
 
     // The arguments IN defending argument along the attacks: a grounded chain explaining its label
     private fun supporters(
         argument: Argument,
         graph: Graph,
         chain: List<String>,
     ): List<LabelledArgument> =
         if (argument.identifier in chain) {
             emptyList()
         } else {
             graph.labellings.filter { argument.identifier == it.argument.identifier && it.label == "in" } +
                 attackers(argument, graph).flatMap { attacker ->
                     attackers(attacker.argument, graph)
                         .filter { it.argument.identifier != argument.identifier }
                         .flatMap { supporters(it.argument, graph, chain + argument.identifier) }
                 }
         }
 
     // The support set of effect: the union of all its explanations
     private fun supports(
         graph: Graph,
         effect: Term,
     ): Sequence<Argument> =
         graph.labellings
             .asSequence()
             .filter { concludes(it.argument, effect) }
             .flatMap { supporters(it.argument, graph, emptyList()) }
             .map { it.argument }
 
     // The theory of the solver asking, with its flags (those of its libraries too) as facts, but the semantics, which
     // is that of the analysis: its own flag facts give way to them
     private fun theory(request: Solve.Request<ExecutionContext>): Theory {
         val theory = request.context.staticKb
         val settings = Settings.of(request.context) ?: return theory
         val except = setOf(ArgumentLabellingMode.predicate())
         return Theory.of(
             theory.unificator,
             theory.clauses.filterNot { settings.states(it) } + settings.facts(request.context, except),
         )
     }
 
     // The theory with the statements of intervention as axioms, each named after its statement
     private fun intervened(
         request: Solve.Request<ExecutionContext>,
         intervention: PlList,
     ): Theory =
         theory(request).plus(
             Theory.of(
                 intervention.toList().map { statement ->
                     Clause.of(Struct.of(":->", Atom.of("fk${statement.hashCode() and Int.MAX_VALUE}"), statement))
                 },
             ),
         )
 
     /** Some argument for [statement] is IN in the grounded labelling of the theory */
     fun isAccepted(
         request: Solve.Request<ExecutionContext>,
         statement: Term,
     ): Boolean = graphOf(request, theory(request), statement).labellings.any { it.label == "in" && concludes(it.argument, statement) }
 
     private fun baseSupports(
         request: Solve.Request<ExecutionContext>,
         effect: Term,
     ): List<Term> = supports(graphOf(request, theory(request), effect), effect).map { it.termRepresentation() }.toList()
 
     // The IN attackers, after intervention, of the supports of effect it makes OUT or UND
     private fun interventionAttackers(
         request: Solve.Request<ExecutionContext>,
         intervention: PlList,
         supports: List<Term>,
         effect: Term,
     ): List<Argument> =
         graphOf(request, intervened(request, intervention), effect).let { graph ->
             graph.labellings
                 .filter { it.label == "out" || it.label == "und" }
                 .filter { a -> supports.any { b -> Unificator.default.match(a.argument.termRepresentation(), b) } }
                 .flatMap { a -> attackers(a.argument, graph).filter { it.label == "in" } }
                 .map { it.argument }
                 .distinct()
         }
 
     private fun properSubsets(
         request: Solve.Request<ExecutionContext>,
         intervention: PlList,
     ): List<PlList> =
         arg2pScope {
             request
                 .solve("properSubsets"(intervention, X))
                 .filter { it.isYes }
                 .map { it.substitution[X]!!.castToList() }
                 .toList()
         }
 
     /** The interventions removing [cause], on the rules of the graph of [effect] */
     fun interventions(
         request: Solve.Request<ExecutionContext>,
         cause: Term,
         effect: Term,
     ): Sequence<PlList> {
         val rules =
             PlList.of(
                 graphOf(request, theory(request), effect)
                     .arguments
                     .map { it.topRule }
                     .filter { it != "none" }
                     .map { Term.parse(it, TermValues.operators) },
             )
         return arg2pScope {
             request
                 .solve("generateInterventions"(rules, cause, X))
                 .filter { it.isYes }
                 .map { it.substitution[X]!!.castToList() }
         }
     }
 
     /**
      * The NESS condition of ICAIL 2025: an explanation of [effect] (a grounded chain) is refuted by [intervention],
      * and by none of its proper subsets
      */
     fun nessOriginal(
         request: Solve.Request<ExecutionContext>,
         intervention: PlList,
         effect: Term,
     ): Boolean {
         val supports = baseSupports(request, effect)
         if (supports.isEmpty()) return false
         val attackers = interventionAttackers(request, intervention, supports, effect)
         return attackers.isNotEmpty() &&
             (
                 intervention.estimatedLength <= 1 ||
                     properSubsets(request, intervention).none { interventionAttackers(request, it, supports, effect).isNotEmpty() }
             )
     }
 
     /**
      * The revised NESS condition: an explanation of [effect] is refuted by [intervention] (an IN attacker), and no
      * proper subset of it refutes it with the same attackers
      */
     fun ness(
         request: Solve.Request<ExecutionContext>,
         intervention: PlList,
         effect: Term,
     ): Boolean {
         val supports = baseSupports(request, effect)
         if (supports.isEmpty()) return false
         val attackers = interventionAttackers(request, intervention, supports, effect).map { it.termRepresentation() }
         return attackers.isNotEmpty() &&
             (
                 intervention.estimatedLength <= 1 ||
                     properSubsets(request, intervention).none { subset ->
                         val others = interventionAttackers(request, subset, supports, effect).map { it.termRepresentation() }
                         attackers.all { a -> others.any { b -> Unificator.default.match(a, b) } }
                     }
             )
     }
 
     /** The but-for condition: an argument for [effect] is IN, and none is after [intervention] */
     fun butFor(
         request: Solve.Request<ExecutionContext>,
         intervention: PlList,
         effect: Term,
     ): Boolean =
         isAccepted(request, effect) &&
             graphOf(request, intervened(request, intervention), effect).labellings.none {
                 it.label == "in" && concludes(it.argument, effect)
             }
 }