diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 5e4535ac4..0b0a5bdaf 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -298,6 +298,24 @@ public class Optimize extends Z3Object { return Native.optimizeToString(getContext().nCtx(), getNativeObject()); } + /** + * Parse an SMT-LIB2 file with optimization objectives and constraints. + * The parsed constraints and objectives are added to the optimization context. + */ + public void fromFile(string file) + { + Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file); + } + + /** + * Similar to FromFile. Instead it takes as argument a string. + */ + public void fromString(string s) + { + Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s); + } + + /** * Optimize statistics. **/