From 4b759fd865ab45643b404bff9270463ef1ef3d4b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Aug 2017 16:18:19 -0700 Subject: [PATCH] add missing functions to serialize optimize benchmarks for Java #1215 Signed-off-by: Nikolaj Bjorner --- src/api/java/Optimize.java | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) 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. **/