unexpected user error (rule_DomainMinMax.minOfDomain ?)

[ott2]

I have a simple spec which:

• works fine unparameterised
• breaks if changing one letting to a given, and providing that in a param file: conjure: user error (rule_DomainMinMax.minOfDomain ?)
• breaks on a 2020-vintage conjure in the latter case with This should never happen, sorry!... IO Error rule_DomainMinMax.minOfDomain ?

Here are the files, with .txt endings due to github's faulty semantics for filenames.

test0.essence
test.essence
test.param

[ott2]

This is still happening with latest Conjure v2.5.1 (Repository version 843ec486d (2024-06-24 13:32:59 +0100)) compiled with GHC 9.4.

As an alternative to switching to CPMpy, I would really like to understand how to work around this. As far as I can tell this error is caused by Conjure being overzealous in its sanity checks. Note that I can't hardcode n because conjure is too slow to solve the full spec (of which this is a tiny extract) and I need to hand the problem to Minion or a SAT solver.

[ozgurakgun]

Hi @ott2 -

Obviously not ideal, but one suggested work around would be the following. Apologies, I didn't find time to look into this yet.

such that forAll i,j : int(0..4) .  {i + j*5 + n/2, (i+1)%5 + j*5 + n/2} in EHS
such that forAll edge_pair in EHS . exists i,j : int(0..4) . {i + j*5 + n/2, (i+1)%5 + j*5 + n/2} = edge_pair

Hope I didn't make a mistake/typo there!

[ozgurakgun]

Also, feel free to use an alternative if that's a better tool for the problem you are solving - I won't be offended :)