Negated Atom with Constant in Body causes unexpected behavior

[matzemathics]

Following program

a(1) :- ~b(1).

is normalized to

a(1) :- ~b(?x), ?x = 1.

Now ?x is a unsafe variable, which the variable order generation code is not prepared to handle, leading to a runtime error:

Variable order must contain an entry for every variable.

This is one half of the problem in #428.

[monsterkrampe]

Seems to be tricky since some part of the execution planning process rely on the fact that the variable order does not include variables that only occur in negated atoms. I will investigate further.

[monsterkrampe]

Also, I'm not getting the mentioned error. With

a(1) :- ~b(1).

I do not get an error at all but the result for a is empty. If I input the normalized version directly, i.e.

a(1) :- ~b(?X), ?X = 1.

I get an error but another one:

thread 'main' panicked at nemo/src/program_analysis/type_inference/position_graph.rs:157:22:
The loop at the top went through all head atoms
stack backtrace:
   0: rust_begin_unwind
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/std/src/panicking.rs:645:5
   1: core::panicking::panic_fmt
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/core/src/panicking.rs:72:14
   2: core::panicking::panic_display
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/core/src/panicking.rs:177:5
   3: core::panicking::panic_str
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/core/src/panicking.rs:152:5
   4: core::option::expect_failed
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/core/src/option.rs:1980:5
   5: core::option::Option<T>::expect
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/core/src/option.rs:894:21
   6: nemo::program_analysis::type_inference::position_graph::<impl nemo::util::labeled_graph::LabeledGraph<nemo::program_analysis::type_inference::position_graph::PredicatePosition,nemo::program_analysis::type_inference::position_graph::PositionGraphEdge,petgraph::Directed>>::from_rules
             at ./nemo/src/program_analysis/type_inference/position_graph.rs:155:38
   7: nemo::program_analysis::type_inference::infer_types
             at ./nemo/src/program_analysis/type_inference.rs:50:26
   8: nemo::program_analysis::analysis::<impl nemo::model::chase_model::program::ChaseProgram>::analyze
             at ./nemo/src/program_analysis/analysis.rs:392:49
   9: nemo::execution::execution_engine::ExecutionEngine<Strategy>::initialize
             at ./nemo/src/execution/execution_engine.rs:93:24
  10: nmo::run
             at ./nemo-cli/src/main.rs:138:46
  11: nmo::main
             at ./nemo-cli/src/main.rs:241:5
  12: core::ops::function::FnOnce::call_once
             at /rustc/4cb3beec86178baff601529389306a4949b077ce/library/core/src/ops/function.rs:250:5

[monsterkrampe]

I think this is rather an issue in planning than in the variable order generation. I will create a separate issue for the type inference error though. (#435)

[aannleax]

Yes I would also expect this to be planning issue, because normally the planning code is responsible for handling fresh variables by augmenting the given variable order somehow

[monsterkrampe]

After the fix in #435 both

a(1) :- ~b(1).

and

a(1) :- ~b(?X), ?X = 1.

have the same behavior of deriving no facts for a, even though a(1) should be derived.

[matzemathics]

I did some further investigation, and it seems addressing this needs some larger architectural changes. Currently there is just no way to handle tables with 0 columns through the PartialTrieScan interface, even though they can come up as intermediary results. In particular, we would have to differentiate the two cases of an empty table and the table, which contains the ()-tuple, for which it is not clear how to represent them through the current interface.

[monsterkrampe]

I think this indeed the same issue as in #193.

[aannleax]

Might potentially be solved by #512.