mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Expose optimize.assertAndTrack to Java (#5387)

Browse source 
Co-authored-by: Marc Mosko <mmosko@parc.com>
This commit is contained in:
Marc Mosko 2021-07-06 01:22:00 -07:00 committed by GitHub
parent 0c7625cd26
commit 8a33391708
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -73,6 +73,28 @@ public class Optimize extends Z3Object {
Assert(constraints);
}
/**
* Assert a constraint into the optimizer, and track it (in the unsat) core
* using the Boolean constant p.
*
* Remarks:
* This API is an alternative to {@link #check} with assumptions for
* extracting unsat cores.
* Both APIs can be used in the same solver. The unsat core will contain a
* combination
* of the Boolean variables provided using {@link #assertAndTrack}
* and the Boolean literals
* provided using {@link #check} with assumptions.
*/
public void AssertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
{
getContext().checkContextMatch(constraint);
getContext().checkContextMatch(p);
Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
constraint.getNativeObject(), p.getNativeObject());
}
/**
* Handle to objectives returned by objective functions.
**/