Fragment supported by `pb2bv` unclear

[bohlender]

When working on a finite-domain problem via tactics (rather than the using the FD-solver directly) I encountered a problem with processing pseudo-boolean constraints.

In particular, the pb2bv-tactic is not applicable to a goal like 4*b0 + 4*b1 + 3*b3 >= 7. The fragment it's in is supposedly unsupported, and probing indeed shows that it is-quasi-pb (rather than is-pb).

The following minimal Python-example highlights the issue:

from z3 import *
print('Using', get_full_version()) # 4.8.9.0

# expr := 4*b!0 + 4*b!1 + 3*b!2 >= 7
consts = [FreshBool() for i in range(3)]
weights = [4, 4, 3]
expr = PbGe([(c, w) for c,w in zip(consts, weights)], 7)

g = Goal()
g.add(expr)
Tactic('pb2bv')(g)

This yields the following exception: z3.z3types.Z3Exception: b'goal is in a fragment unsupported by pb2bv. Offending expression: ((_ pbge 7 4 4 3) b!0 b!1 b!2)'

Why is that the case? Isn't expr the prototypical pseudo-boolean constraint? Maybe this behaviour is by design and I am just missing something?

[bohlender]

I've found that a reduction of pseudo-boolean constraints to plain Booleans (or bit-vectors) is -- somewhat unexpectedly -- possible through an option of the card2bv tactic. When its pb.solver option is set to some encoding, i.e. not to solver, the pb-constraints can be reduced to bit-vectors (or Booleans):

from z3 import *
print('Using', get_full_version()) # 4.8.9.0

# expr := 4*b!0 + 4*b!1 + 3*b!2 >= 7
consts = [FreshBool() for i in range(3)]
weights = [4, 4, 3]
pairs = list(zip(consts, weights))
expr = PbGe(pairs, 7)

g = Goal()
g.add(expr)

# Use the following instead of Tactic('pb2bv')(g)
p = ParamsRef()
p.set('pb.solver', 'sorting') # use any setting but 'solver'
WithParams(Tactic('card2bv'), p)(g)

This solves my issue, but I'm left wondering why the pb.solver option hides in the card2bv tactic rather than being an option of pb2bv. I didn't expect to find it there and, as a result, am unsure what the purpose of pb2bv is. After all pb2bv doesn't seem to be applicable to expr, which I consider to be pseudo-boolean.

Feel free to close the issue, but I'd appreciate a remark regarding the purpose of pb2bv.

[NikolajBjorner]

Correct, it should also be an option to the tactic.

The background for why the option lives currently only with the sat solver core, is that I have been using the tactic from the QF_FD solver, which targets the SAT solver core.