nmr_check.pl -- Detect OLON rules and construct nmr_check

Detect OLON rules and construct nmr_check.

Terminology:

OLON: a loop with an odd number of default. negations in its circular call dependency path.
CHS: Coinductive Hypothesis Set, i.e., an atom that is true due to coinduction, i.e. because it unifies with an ancestor.
NMR check: non-monotonic reasoning check (from Computing Stable Models of Normal Logic Programs Without Grounding by Kyle Marple et al.

author: - Kyle Marple
version: - 20170127
See also: - An OLON is a loop with an odd number of default. negations in its circular call dependency path, from "Layered Models Top-Down Querying of Normal Logic Programs" by LM Pereira, PADL09.; - "Galliwasp: A Goal-Directed Answer Set Solver" by Kyle Marple and Gopal Gupta, LOPSTR 2012 for details on the NMR check
license: - BSD-3

generate_nmr_check(+Module) is det

Get the rules in the program containing odd loops and compute the NMR check. After this step, headless rules are useless, so remove them and add a fact for the negation of the dummy head (_false_0). Call generate_nmr_check/0 instead of this.

nmr_check(+OLONrules:list, -NmrCheck:list) is det[private]

Build the nmr_check.

Arguments:

`OLONrules`	- List of rules to create NMR sub-checks for.
`NmrCheck`	- List of NMR sub-check goals.

olon_rules(+Rules:list, +Module, -OLONrules:list) is det[private]

Determine which of the original rules are part of odd loops, and return them in a list.

Arguments:

`RuleIn`	- Input list of rules.
`OLONrules`	- `Rules` for which NMR sub-checks will need to be created.

dfs(+Nodes:list, -OLONs:list, -OrdinaryPaths:list, -PositiveLoops:list) is det[private]

Use depth first search to detect: cycles with no negation, cycles with even (>2) negation, paths with no cycle and cycles with odd negation. A list of paths will be returned for each type. Wrapper for dfs2/8.

Arguments:

`Nodes`	- `Nodes` in the call graph.
`OLONs`	- Paths containing odd loops. A list of lists of arcs, with each sublist representing a path containing an odd loop.
`OrdinaryPaths`	- Paths containing no odd loops and no even loops without an intervening negation. A list of lists of arcs, with each sublist representing a path containing only ordinary rules.
`PositiveLoops`	- Path with cycles that have no negation. A list of lists of arcs, with each sublist representing a path containing a positive loop.

dfs2(+Nodes:list, +Tested:list, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det[private]

Test each node in case the graph isn't connected. For a visited node, dfs3/11 will return quickly as no paths will be expanded.

Arguments:

`Nodes`	- `Nodes` in the call graph.
`Tested`	- List of visited nodes with negation, so that we only visit each node at most once for each negation option: no negation, odd negation and even negation. Elements are of the form `v(X, N)`, where X is the node and N is 0 = no negations, 1 = odd negs or 2 = even > 0 negs.
`OlonIn`	- Input list of paths containing OLONs.
`OlonOut`	- Output list of paths containing OLONs.
`OrdIn`	- Input list of ordinary paths.
`OrdOut`	- Output list of ordinary paths.
`PosIn`	- Input list of paths with cycles and no negations.
`PosOut`	- Output list of paths with cycles and no negations.

dfs3(+Arcs:list, +VisitedIn:list, -VisitedOut:list, +Path:list, +Negations:int, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det[private]

The main traversal. Traverse each arc for a node, but don't recursively search previously visited nodes.

Arguments:

`Arcs`	- The list of arcs in the call graph that originate at the last node in the current path.
`VisitedIn`	- Input list of visited nodes with negation, so that we only visit each node at most once for each negation option: no negation, odd negation and even negation. Elements are of the form `v(X, N)`, where X is the node and N is 0 = no negations, 1 = odd negs or 2 = even > 0 negs.
`VisitedOut`	- Output list of visited nodes.
`Path`	- List of arcs forming the path currently being examined.
`Negations`	- 0 = no negations, 1 = odd negs or 2 = even > 0 negs
`OlonIn`	- Input list of paths containing OLONs.
`OlonOut`	- Output list of paths containing OLONs.
`OrdIn`	- Input list of ordinary paths.
`OrdOut`	- Output list of ordinary paths.
`PosIn`	- Input list of paths with cycles and no negations.
`PosOut`	- Output list of paths with cycles and no negations.

check_cycle(+Node:list, +Path:list, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det[private]

Get the cycle and classify by number of negations.

Arguments:

`Node`	- A node in the call graph.
`Path`	- List of arcs forming the path currently being examined.
`OlonIn`	- Input list of paths containing OLONs.
`OlonOut`	- Output list of paths containing OLONs.
`OrdIn`	- Input list of ordinary paths.
`OrdOut`	- Output list of ordinary paths.
`PosIn`	- Input list of paths with cycles and no negations.
`PosOut`	- Output list of paths with cycles and no negations.

get_cycle(+Node:list, +Path:list, -Cycle:list, -Negations:int) is det[private]

Get the portion of the path forming the cycle on node X. Count the negations as we go. Will fail if path doesn't have a cycle over X. Wrapper for get_cycle2/5.

Arguments:

`Node`	- A node in `Path`.
`Path`	- List of arcs forming the path currently being examined.
`Cycle`	- List of arcs forming a cycle on `Node`.
`Negations`	- The number of negations in `Cycle`.

get_cycle2(+Node:list, +Path:list, -Cycle:list, +NegsIn:int, -NegsOut:int) is det[private]

See get_cycle/4. Call that instead.

Arguments:

`Node`	- A node in `Path`.
`Path`	- List of arcs forming the path currently being examined.
`Cycle`	- List of arcs forming a cycle on the original node.
`NegsIn`	- Input number of negations in `Cycle`.
`NegsOut`	- Output number of negations in `Cycle`.

classify_cycle(+Negs:int, +Cycle:list, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det[private]

Put the cycle into the right group based on number of negations.

Arguments:

`Negs`	- Number of negations in `Cycle`.
`Cycle`	- List of arcs forming a cycle.
`OlonIn`	- Input list of paths containing OLONs.
`OlonOut`	- Output list of paths containing OLONs.
`OrdIn`	- Input list of ordinary paths.
`OrdOut`	- Output list of ordinary paths.
`PosIn`	- Input list of paths with cycles and no negations.
`PosOut`	- Output list of paths with cycles and no negations.

update_negation(+NegsIn1:int, +NegsIn2:int, -NegsOut:int) is det[private]

Update negation value. 0 = no negations, 1 = odd negs, 2 = even > 0 negs.

Arguments:

`NegsIn`	- Input negation value 1.
`NegsIn2`	- Input negation value 2.
`NegsOut`	- Output negation value.

set_append(+Element:callable, +Set:list, +SetOut:list) is det[private]

Append Elements only if not already present in Set.

Arguments:

`Element`	- The element to append.
`Set`	- Input set.
`SetOut`	- Output set.

extract_ids(+Cycles:list, -IDs:list) is det[private]

Given a list of cycles, get the unique rules IDs.

Arguments:

`Cycles`	- List of cycles in the call graph. Each cycle is a list of arcs.
`IDs`	- List of rule `IDs` from `Cycles`.

extract_ids2(+Cycles:list, +IdsIn:list, -IdsOut:list) is det[private]

Get the lists of ids from each path and merge them.

Arguments:

`Cycles`	- List of cycles in the call graph. Each cycle is a list of arcs.
`IdsIn`	- Input list of rules IDs from `Cycles`.
`IdsOut`	- Output list of rules IDs from `Cycles`.

extract_ids3(+Cycle:list, +IdsIn:list, -IdsOut:list) is det[private]

Get a list of IDs from a single path, extracting the rule ID for each arc.

Arguments:

`Cycle`	- A list of arcs representing a cycle in the call graph.
`IdsIn`	- Input list of rules IDs from Cycles.
`IdsOut`	- Output list of rules IDs from Cycles.

divide_rules(+RulesIn:list, +IDs:list, -Members:list, -Nonmembers:list) is det[private]

Split rules based on ID list membership.

Arguments:

`RulesIn`	- Input list of rules.
`IDs`	- A list of rule `IDs`.
`Members`	- Rules whose ID is a member of `IDs`.
`Nonmembers`	- Rules whose ID is not in `IDs`.

get_headless_rules(+RulesIn:list, +HeadlessIn:list, -HeadlessOut:list) is det[private]

Get rules with the head '_false', indicating the rule was headless in the original program, and thus an OLON rule.

Arguments:

`RulesIn`	- Input rule list.
`HeadlessIn`	- Input list of headless rules (head = 1).
`HeadlessOut`	- Output list of headless rules (head = 1).

olon_chks(+RulesIn:list, -NMRCheck:list, +Counter:int) is det[private]

For each OLON rule, create a check that contains the negation of the rule's head by copying the rule and adding the negation if not present. Create the duals here since we can discard the unused non-dual. Add the new (dual) rule's head to the list of nmr checks. Use the original rule's ID for the goal ID in the NMR check. When adding the negation of the head to a rule, set the ID to ensure that it will be the last goal in the rule.

Arguments:

`RulesIn`	- List of rules to create NMR sub-checks for.
`NMRCheck`	- List of NMR sub-check goals.
`Counter`	- `Counter` used to ensure sub-check heads are unique.

assign_unique_ids(+ListIn:list, -ListOut:list) is det[private]

Give each rule or goal a unique ID to allow individual members to be identified later. Wrapper for assign_unique_ids2/3. Note that list order is not changed. The IDs are sequential, and allow the original order to be restored by sorting later.

Arguments:

`ListIn`	- A list of rules or goals without attached IDs.
`ListOut`	- A list of rules or goals with unique IDs attached.

assign_unique_ids2(+ListIn:list, -ListOut:list, +Counter:int) is det[private]

Assign each rule or goal (int) a unique ID, the current value of Counter. Call assign_unique_ids/2 instead of this predicate.

Arguments:

`ListIn`	- A list of rules or goals without attached IDs.
`ListOut`	- A list of rules or goals with unique IDs attached.
`Counter`	- The next ID to assign.

create_dcc_rules(+Rc, +Module) is det[private]

Create dcc rules to check consistency on-the-fly