Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Negated Atom with Constant in Body causes unexpected behavior #434

Open
matzemathics opened this issue Nov 28, 2023 · 8 comments
Open

Negated Atom with Constant in Body causes unexpected behavior #434

matzemathics opened this issue Nov 28, 2023 · 8 comments
Assignees
Labels
bug Something isn't working planning engine
Milestone

Comments

@matzemathics
Copy link
Collaborator

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.

@matzemathics matzemathics added bug Something isn't working program analysis Issue related to global program analysis labels Nov 28, 2023
@mmarx mmarx added this to nemo Nov 29, 2023
@github-project-automation github-project-automation bot moved this to Todo in nemo Nov 29, 2023
@mmarx mmarx added this to the Release 0.4.0 milestone Nov 29, 2023
@monsterkrampe monsterkrampe self-assigned this Nov 29, 2023
@monsterkrampe
Copy link
Member

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
Copy link
Member

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
Copy link
Member

monsterkrampe commented Nov 29, 2023

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)

@monsterkrampe monsterkrampe removed their assignment Nov 29, 2023
@aannleax
Copy link
Member

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 monsterkrampe changed the title Negated atoms introduce implicit unsafe variables, leading to failiure in variable order generation. Negated Atom with Constant in Body causes unexpected behavior Nov 30, 2023
@monsterkrampe
Copy link
Member

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.

@monsterkrampe monsterkrampe added planning engine and removed program analysis Issue related to global program analysis labels Dec 1, 2023
@matzemathics
Copy link
Collaborator Author

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
Copy link
Member

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

@aannleax
Copy link
Member

Might potentially be solved by #512.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working planning engine
Projects
Status: Todo
Development

No branches or pull requests

4 participants