mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Add AssertSoft String overload for Java Api (#5475)

Browse source 
This adds a String overload for AssertSoft.
Previously only integer weights could have been used,
limiting the user. With Strings the user can now use
e.g. Java's BigInteger class converted to a String instead.
This commit is contained in:
intrigus-lgtm 2021-08-12 18:18:18 +02:00 committed by GitHub
parent b016465ad2
commit 35698c650d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/api/java/Optimize.java
View file

@ -173,10 +173,21 @@ public class Optimize extends Z3Object {
* *
**/ **/
public Handle<?> AssertSoft(Expr<BoolSort> constraint, int weight, String group) public Handle<?> AssertSoft(Expr<BoolSort> constraint, int weight, String group)
{
return AssertSoft(constraint, Integer.toString(weight), group);
}
/**
* Assert soft constraint
*
* Return an objective which associates with the group of constraints.
*
**/
public Handle<?> AssertSoft(Expr<BoolSort> constraint, String weight, String group)
{ {
getContext().checkContextMatch(constraint); getContext().checkContextMatch(constraint);
Symbol s = getContext().mkSymbol(group); Symbol s = getContext().mkSymbol(group);
return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject())); return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), weight, s.getNativeObject()));
} }
/** /**