Soft Assertions in the DotNet API

0
votes

I did some experiments with the latest unstable versions of 4.4.1 and concluded that soft assertions just work fine for me as in the example below:

    (assert(! ((and ( <= P291 200)( >= P291 100))) :named  R291mm ))
    (assert-soft(! (( = P291 170)) :named  R291d ):weight 7)

P291 has a min and a max value (100, 200) - defined as hard constraints - and a default, which should be chosen if no other constraints are influencing the value.

With Z3 on the command line console I get the expected results, but as soon as I'm using my DotNet application, read the very same file via ParseSMTLIB2File and feed the expressions to the solver with Assert or AssertAndTrack (other methods are not defined) the soft assertions seem to get ignored. A closer look in the debugger shows that only the hard constraints can be found in Args. So ParseSMTLIB2File seems not to be prepared to read soft constraints.

Do I have to set special options with the context or am I just too early?

If I'm too early :are there plans to make soft constraints available via the DotNet API? If the answer is positive, what will be the timeframe?

Thx

Christian J

1
.netz3

1 Answers

0
votes

It's quite possible that the parser functions don't support that yet, and there's a non-zero chance that they never will; those are really legacy functions from the time where each file contained only one problem of type SMT benchmark without handling of command extensions like assert-soft. There is no time-frame for adding extensions to the parse* functions.

Note that the .NET API already contains the optimize object, so it's possible to set up such problems via the API, and that's the preferred approach.