mirror of
https://github.com/Z3Prover/z3
synced 2025-06-08 15:13:23 +00:00
parent
92b6a3e134
commit
7e2783c6a2
1 changed files with 7 additions and 7 deletions
|
@ -127,13 +127,13 @@ public class Solver extends Z3Object
|
||||||
* using the Boolean constants in ps.
|
* using the Boolean constants in ps.
|
||||||
*
|
*
|
||||||
* Remarks:
|
* Remarks:
|
||||||
* This API is an alternative to <see cref="Check"/> with assumptions for
|
* This API is an alternative to {@link check} with assumptions for
|
||||||
* extracting unsat cores.
|
* extracting unsat cores.
|
||||||
* Both APIs can be used in the same solver. The unsat core will contain a
|
* Both APIs can be used in the same solver. The unsat core will contain a
|
||||||
* combination
|
* combination
|
||||||
* of the Boolean variables provided using <see cref="AssertAndTrack"/>
|
* of the Boolean variables provided using {@link assertAndTrack}
|
||||||
* and the Boolean literals
|
* and the Boolean literals
|
||||||
* provided using <see cref="Check"/> with assumptions.
|
* provided using {@link check} with assumptions.
|
||||||
**/
|
**/
|
||||||
public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
|
public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
|
||||||
{
|
{
|
||||||
|
@ -152,13 +152,13 @@ public class Solver extends Z3Object
|
||||||
* using the Boolean constant p.
|
* using the Boolean constant p.
|
||||||
*
|
*
|
||||||
* Remarks:
|
* Remarks:
|
||||||
* This API is an alternative to <see cref="Check"/> with assumptions for
|
* This API is an alternative to {@link check} with assumptions for
|
||||||
* extracting unsat cores.
|
* extracting unsat cores.
|
||||||
* Both APIs can be used in the same solver. The unsat core will contain a
|
* Both APIs can be used in the same solver. The unsat core will contain a
|
||||||
* combination
|
* combination
|
||||||
* of the Boolean variables provided using <see cref="AssertAndTrack"/>
|
* of the Boolean variables provided using {@link assertAndTrack}
|
||||||
* and the Boolean literals
|
* and the Boolean literals
|
||||||
* provided using <see cref="Check"/> with assumptions.
|
* provided using {@link check} with assumptions.
|
||||||
*/
|
*/
|
||||||
public void assertAndTrack(BoolExpr constraint, BoolExpr p)
|
public void assertAndTrack(BoolExpr constraint, BoolExpr p)
|
||||||
{
|
{
|
||||||
|
@ -294,7 +294,7 @@ public class Solver extends Z3Object
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Create a clone of the current solver with respect to <c>ctx</c>.
|
* Create a clone of the current solver with respect to{@code ctx}.
|
||||||
*/
|
*/
|
||||||
public Solver translate(Context ctx)
|
public Solver translate(Context ctx)
|
||||||
{
|
{
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue