search

potassco / clingcon

⛓️ Extension of clingo to handle constraints over integers
https://potassco.org/
MIT License
25 stars 4 forks source link

Unfreeze Translation Literals #42

Closed MaxOstrowski closed 4 years ago

MaxOstrowski commented 4 years ago

Literals added during translation that are not order literals could be unfrozen.

After checking for add_literal in the translate methods of the constraints, only libclingcon/src/constraints.cc ll 909 uses add_literal directly, and these are imho the only literals that could be added unfrozen. Is this correct ? In my opinion these literals are already checked for truth values and are not worth to be unfrozen, as clasp probably can't do anything with them.

The original idea would be to add unfrozen literals in libclingcon/clingcon/base.hh ll 303 only if state_ == InitState::Translate. The problem here is that during the translation, order literals could get introduced that need to be frozen. They are also added using the same add_literal function. The question that I now have is, if line 307 (updating stats for literals added during translation) is still correct/intended, as order literals are counted too.

rkaminsk commented 4 years ago

In case of the = and != translation, the old literal of the theory atom could be unfrozen (but there is no API for this (and one would have be careful about this)). Another interesting thing would be to unfreeze if everything has been translated. But again there is no API for this. I think that providing a sensible API for this would be very involved and I won't approach this any time soon.

MaxOstrowski commented 4 years ago

The question that I now have is, if line 307 (updating stats for literals added during translation) is still correct/intended, as order literals are counted too.

I intended to count all literals added during translation. And I think the line does what I intended to implement. :smile: It is always possible to make the statistics more fine-granular. I would only do this with some idea to investigate some behavior in mind.

MaxOstrowski commented 4 years ago

Just some curiosity on my side, everything fine. Closing this. PS: If you edit my posts I do not get a notification :hand_over_mouth:

rkaminsk commented 4 years ago

Just some curiosity on my side, everything fine. Closing this. PS: If you edit my posts I do not get a notification hand_over_mouth

I must have been tired. I wanted to quote reply but something different happened.