- edited description
unsat when LUP is active
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 }
}
Comments (11)
-
-
reporter - edited description
-
I see two issues
- This should be handled by xsb @jjansen
- BDDS are wrong when there's too much arithmetic @PieterVH
-
- edited description
-
assigned issue to
-
I added @PieterVH as responsible since this is a bdd+arithmetic issue
-
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.
-
The XSB thing is irrelevant, since XSB is still by default off.
It works well with xsb. Only the bdds are an issue
-
Why is XSB not yet the default?
-
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 -
Issue is in liftedunitpropagation with >=4 propagationsteps. Any suggestions other then looking trough the whole propagation?
-
check specificially from querying bdds with modulo?
- Log in to comment