We use a custom datatype to encode nullable types and define functions (in SMT) do lift the normal logical operators (not included in the below example). Besides finding satisfiable models (which works nicely) we would also like to minimize and maximize numeric values. However, I don't always get the optimal values when doing this.
A bit more background. We optimize on 'simple' Sorts (Int and Reals). To do this, we introduce new variables of the underlying numeric sort and add constraints to enforce that if the Optional variable holds a value, it must be equal to the value of the 'basic' variable. We continue by adding constraints on the numeric domain to the basic variable and finally we minimize or maximize on these basic variables. This, like stated earlier, does not always yield the expected optimal result.
I have tried to construct a small example. It does need some wiring.
(set-option :opt.priority lex))
; custom Optional datatype to encode nillable types
(declare-datatypes ((Optional 1)) ((par (T) ((nil) (value (val T))))))
(declare-const d (Optional Int))
(declare-const e (Optional Int))
; The basic variable used to constraint the domain and to express optimization criteria
(declare-const d__basic Int)
(assert (or (= d (as nil (Optional Int))) (= d (value d__basic))))
; Assert the domain [0..1000]
(assert (and (>= d__basic 0) (<= d__basic 1000)))
; The basic variable used to constraint the domain and to express optimization criteria
(declare-const e__basic Int)
(assert (or (= e (as nil (Optional Int))) (= e (value e__basic))))
; Assert the domain [0..1000]
(assert (and (>= e__basic 0) (<= e__basic 1000)))
; The actual constraint expressed on the optional type (d <= e && e = 1000)
(assert (match d (
(nil false)
((value lhs) (match e (
(nil false)
((value rhs) (and (<= lhs rhs) (= rhs 1000)) )) )))))
(maximize d__basic)
(maximize e__basic)
(check-sat)
(eval d)
(eval e)
When I run the above example (on Z3 4.13) I get the following output:
sat
(value 253)
(value 1000)
This is unexpected. I expect d to evaluate to (value 1000).
When I add the same constraint directly on the basic variables, (assert (and (<= d__basic e__basic) (= e__basic 1000))), I do get the expected result:
sat
(value 1000)
(value 1000)
Am I doing something wrong or does this trigger a bug in the Optimizer?
We use a custom datatype to encode nullable types and define functions (in SMT) do lift the normal logical operators (not included in the below example). Besides finding satisfiable models (which works nicely) we would also like to minimize and maximize numeric values. However, I don't always get the optimal values when doing this.
A bit more background. We optimize on 'simple' Sorts (Int and Reals). To do this, we introduce new variables of the underlying numeric sort and add constraints to enforce that if the Optional variable holds a value, it must be equal to the value of the 'basic' variable. We continue by adding constraints on the numeric domain to the basic variable and finally we minimize or maximize on these basic variables. This, like stated earlier, does not always yield the expected optimal result.
I have tried to construct a small example. It does need some wiring.
When I run the above example (on Z3 4.13) I get the following output:
This is unexpected. I expect
dto evaluate to(value 1000). When I add the same constraint directly on the basic variables,(assert (and (<= d__basic e__basic) (= e__basic 1000))), I do get the expected result:Am I doing something wrong or does this trigger a bug in the Optimizer?