sambayless
commented
4 years ago Good catch! I've reproduced this locally, thank you for noticing this!
Logic.LessEq/GreaterEq/LessThan/GreaterThan apply to comparisons between lists of literals, not bitvectors (those methods actually predate bitvector support in monosat). Now that MonoSAT also has bitvectors, that behaviour is very unintuitive.
On the subject of bitvectors in monosat: One thing to keep in mind is that in monosat (unlike other SMT solvers), Bitvectors are constrained not to overflow/underflow (this is required to ensure they have monotonic semantics). As a result, the formula will be UNSAT in monosat (but SAT in other SMT solvers)
bv1 = BitVector(4)
assert(Solve())
# 15 is the largest value representable in a 4 bit unsigned bitvector
Assert(bv1==15)
# In MonoSAT, bitvectors cannot overflow
bv2 = bv1 + 1
# so bv2 = 15 + 1 will be UNSAT (whereas in other SMT solvers this might be SAT)
assert(not Solve())Also, all bitvectors in MonoSAT are unsigned.
methods such as LessEq and GreaterEq are not working properly for bitvectors, e.g., LessEq(bv1, bv2) leads to a different result with (bv1 <= bv2), the latter is working as expected.