unsat when LUP is active

[JoD]

vocabulary V {
    type Num isa int
    cd(Num,Num,Num) // Common divider
    gcd(Num,Num,Num) // Greatest common divider
}

theory T:V {
    {! x y z: cd(x,y,z) <- x % z = 0 & y % z = 0.}
    {! x y z: gcd(x, y, z) <- (cd(x,y,z) & (!w: cd(x,y,w) => w =< z)).}
}

structure S:V {
    Num = { 1 .. 2 }
}

[Bart Bogaerts]

I see two issues

1. This should be handled by xsb @jjansen
2. BDDS are wrong when there's too much arithmetic @PieterVH

[Bart Bogaerts]

I added @PieterVH as responsible since this is a bdd+arithmetic issue

[Joachim Jansen]

The XSB option wasn't turned on, that's why it wasn't handled. If XSB is activated, the definition is completely evaluated.

Unless I'm mistaken this means there's no issue for XSB here.

[Bart Bogaerts]

The XSB thing is irrelevant, since XSB is still by default off.

It works well with xsb. Only the bdds are an issue

http://seldon.cs.kuleuven.be/idp/?src=2b33b7c05dfbd494feca

[Bart Bogaerts]

Why is XSB not yet the default?

[Joachim Jansen]

Because I've never been brave enough to put it as default.

Next week I'll start implementing the switch. Some other features need to be addressed as wel (code separation for when XSB is off is not complete yet either. Maybe not even possible with the current tight integration with bootstrapping)

Edit: See issue #844

[Pieter Van Hertum]

Issue is in liftedunitpropagation with >=4 propagationsteps. Any suggestions other then looking trough the whole propagation?

[Bart Bogaerts]

check specificially from querying bdds with modulo?