fix wrong example and its wrong documentation.
Z3 seems to have a bug for optimization,
such that the returned `handle` contains a wrong optimal value.
The model seems to be correct.
The bug is reported at .
Thus currently the output of the running example and the `ideal solution` do not match.
@@ -82,7 +82,7 @@ public class OptimizationFormulaWeights {
bmgr.ifThenElse(imgr.lessOrEquals(x, four), scoreHigh, scoreBasic), // important
bmgr.ifThenElse(imgr.lessOrEquals(y, zero), scoreMedium, scoreBasic), // less important
bmgr.ifThenElse(imgr.lessOrEquals(y, four), scoreMedium, scoreBasic), // less important
- bmgr.ifThenElse(imgr.lessOrEquals(x, zero), scoreLow, scoreBasic), // not important
+ bmgr.ifThenElse(imgr.lessOrEquals(z, zero), scoreLow, scoreBasic), // not important
bmgr.ifThenElse(imgr.lessOrEquals(z, four), scoreHigh, scoreBasic) // important
);
@@ -93,7 +93,7 @@ public class OptimizationFormulaWeights {
assert response == OptStatus.OPT;
// for integer theory we get the optimal solution directly as model.
- // ideal solution: sum=30 with e.g. x=0,y=6,z=4
+ // ideal solution: sum=32 with e.g. x=0,y=6,z=4 or x=0,y=7,z=3 or x=0,y=8,z=2 ...
logger.log(
Level.INFO,
"maximal sum ",
