mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
add missing functions to serialize optimize benchmarks for Java #1215
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4b759fd865
commit
43c2ccb29a
|
@ -302,7 +302,7 @@ public class Optimize extends Z3Object {
|
||||||
* Parse an SMT-LIB2 file with optimization objectives and constraints.
|
* Parse an SMT-LIB2 file with optimization objectives and constraints.
|
||||||
* The parsed constraints and objectives are added to the optimization context.
|
* The parsed constraints and objectives are added to the optimization context.
|
||||||
*/
|
*/
|
||||||
public void fromFile(string file)
|
public void fromFile(String file)
|
||||||
{
|
{
|
||||||
Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
|
Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
|
||||||
}
|
}
|
||||||
|
@ -310,7 +310,7 @@ public class Optimize extends Z3Object {
|
||||||
/**
|
/**
|
||||||
* Similar to FromFile. Instead it takes as argument a string.
|
* Similar to FromFile. Instead it takes as argument a string.
|
||||||
*/
|
*/
|
||||||
public void fromString(string s)
|
public void fromString(String s)
|
||||||
{
|
{
|
||||||
Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
|
Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue