mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (#5832)

Browse source 
* Add mkLinearOrder

* reorder arguments to match definition, add short comment

* add partial order

* add comments
This commit is contained in:
mbergen 2022-02-16 22:37:20 +01:00 • committed by GitHub
parent 9cf50766a6
commit 2e15e2aa4d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 31 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/api/java/Context.java
View file

@ -4038,6 +4038,37 @@ public class Context implements AutoCloseable {
return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
}
/**
* Creates or a linear order.
* @param index The index of the order.
* @param sort The sort of the order.
*/
public <R extends Sort> FuncDecl<BoolSort> mkLinearOrder(R sort, int index) {
return (FuncDecl<BoolSort>) FuncDecl.create(
this,
Native.mkLinearOrder(
nCtx(),
sort.getNativeObject(),
index
)
);
}
/**
* Creates or a partial order.
* @param index The index of the order.
* @param sort The sort of the order.
*/
public <R extends Sort> FuncDecl<BoolSort> mkPartialOrder(R sort, int index) {
return (FuncDecl<BoolSort>) FuncDecl.create(
this,
Native.mkPartialOrder(
nCtx(),
sort.getNativeObject(),
index
)
);
}
/**
* Wraps an AST.