potassco / potassco/constraint-handler

Similarly named operators are indistinguishable.

Open
#170 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Python
Stars
3
Forks
0
Avg merge
1d 19h
Merged PRs (30d)
20

Description

While trying to continue despite my issues described in #169 , I found another, even deeper, issue with the union type Operator in schemas/expression.py.

I'll first describe how I basically found it and then what the implications are.

Problem Description

Imagine an operation using isin on a set is run in the ground engine. Given the respective expression.Operation(eo, eargs) in the evaluator.py created from that operation, one would expect that o = self.expr(eo) would be the operator isin. More specifically, one would likely expect that o == myset.Operator.isin would hold.

In general, one would expect this:

print(o == myset.Operator.isin)
print(o is myset.Operator.isin)

to print True twice, since one used an operation on a set and thus the operator should be identical to that of the set.

But it's not. This prints False twice.

Instead, what does print True twice is this:

print(o == multimap.Operator.isin)
print(o is multimap.Operator.isin)

But why? We used the operation on a set, not on a multimap, so why do we get multimap?

Because myClorm neither uses the multimap.Operator nor the set.Operator directly. Instead, it uses the union expression.Operator. There, multimap comes before myset in the list, hence isin which applies to both, is resolved to multimap.

The following simple example program shows that the operator resolves to multimap:

import clingo

import constraint_handler.myClorm as myClorm
from constraint_handler.schemas import expression
import constraint_handler.set as myset
import constraint_handler.multimap as multimap

sym = clingo.Function("isin", [])
op = myClorm.cltopy(sym, expression.Operator)

print("clingo symbol        :", sym)
print("python value         :", op)
print("type                 :", type(op))
print("module               :", type(op).__module__)
print("equals set operator  :", op == myset.Operator.isin)
print("is set operator      :", op is myset.Operator.isin)

print(op == myset.Operator.isin)
print(op is myset.Operator.isin)
print(op == multimap.Operator.isin)
print(op is multimap.Operator.isin)

One naively may think one could do:

print(op == expression.Operator.isin)
print(op is expression.Operator.isin)

But that of course wouldn't work since the Operator in expression is not an enum but a union type.

Deeper Problem

I repeat, operators with the same name are resolved to the one coming first in the union declaration.

This means that right now isin from set is never used!

Because the evaluator itself uses the specific operators as match cases to then call the correct sub-evaluator:

case multimap.Operator():
    print("multimap",o)
    return self.multimap.operator(o, args)
case myset.Operator():
    print("set",o)
    return self.set.operator(o, args)

I've added these two prints just to show with the next part:

variable_define(bli,my_set, operation(set_make, (val(int,1),(val(int,2),(val(int,3),()))))).
variable_define(bla,my_find, operation(isin, (val(int,1),(variable(my_set),())))).
defaultEngine(ground).

that his actually uses the multimap.Operator.isin to resolve the isin operation.

Reading from .\x.lp
set set_make
multimap isin
Solving...
Answer: 1 (Time: 0.251s)
value(my_set,val(set,set((val(int,3),(val(int,1),(val(int,2),()))))))
value(my_find,val(bool,true))
SATISFIABLE

While we're currently lucky that the implementation for multimap.Operator.isin is precisely what would be expected for set.Operator.isin, this is only a lucky coincidence.

When we include add to add elements to sets, multimaps or other datatypes, this would no longer work out this nicely and may result in unexpected behaviour or crashes since it would try to use the arithmetic.Operator.add for everything.

Resolution

In short, the operator resolution has to be made context aware in some way. An easy way would be to use "name spaces" to avoid collisions (set_isin,multimap_isin) but this makes the code even more verbose, Another way would be to make the resolution itself smarter for operators with clashing names.

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start in schemas/expression.py and evaluator.py, then trace how cltopy resolves symbols into the union type expression.Operator. Reproduce the isin example with set.Operator and multimap.Operator, and inspect the evaluator's operator match cases. Done means operators with colliding names resolve to the contextually correct implementation without breaking the existing sub-evaluators.

Written by the indexing model from the issue text.

Assessment

Tech stack
python
Domain
backend
Issue type
Bug
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.