optimizeAssertSoft=undefined

[owestphal]

I was trying to encode some MaxSAT Problems, but optimizeAssertSoft is not defined in src/Z3/Monad.hs or rather it is "defined" as undefined.

Is this simply an oversight and fixed in the way I did, or is there a deeper reason behind this?

Some quick tests seem to work as expected.

[maurobringolf]

Thanks for the PR, looks good to me :+1:

Ideally we could directly use one of your examples for the testsuite, covering this function? I can implement the actual test if you don't have time/interest but are willing to share an example (API code or SMT-LIB, doesn't matter).

Is this simply an oversight and fixed in the way I did, or is there a deeper reason behind this?

No deeper reason, the Z3 API consists of a multiple hundreds of functions and is constantly changing and expanding. We try to cover as much as possible and are always open to covering more functions needed by users. It's a process, but undefined is probably not a good idea for uncovered functions. Maybe we should make a systematic effort in removing the undefineds. (EDIT: I think this was just a single case, grep tells me that there are no more undefineds in our code).

[owestphal]

This should be a nice example. Maybe also with varying weights.

(declare-const x1 Int)
(declare-const x2 Int)
(declare-const x3 Int)
(declare-const x4 Int)
(assert (not (= 0 (+ x1 x2))))
(assert (not (= 0 (+ x2 x3))))
(assert (= 0 (+ x3 x4)))
(assert-soft (= x1 2) :weight 1 :id default)
(assert-soft (= x2 4) :weight 1 :id default)
(assert-soft (= x3 6) :weight 1 :id default)
(assert-soft (= x4 8) :weight 1 :id default)
(check-sat)
(get-model)

[maurobringolf]

Thanks a lot!