examples/python/rc2.py question

[mmosko]

I am trying to run the rc2.py example against the script below.

(set-logic QF_FD)

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)

(assert (not a))
(assert (and (or a b) (not (and a b))))

(assert-soft b :weight 10)
(assert-soft c :weight 5)
(assert-soft (and (or b c) (not (and b c))) :weight 20)

(check-sat)```

It crashes when setting the assumptions with the error: `only propositional assumptions are supported for finite domains (and (or b c) (not (and b c)))`.

I assume I need to do something like "(assert (=> bb (and (or b c) (not (and b c))))" and then put bb in the assumptions instead?

[NikolajBjorner]

correct.
You should create a Boolean variable that implies the soft constraint you want to track.