mirror of
https://github.com/Z3Prover/z3
synced 2025-06-11 00:23:25 +00:00
add note to Context documentation about scoped uses of contexts #1077
This commit is contained in:
parent
1fee5fd94e
commit
2d49119d2a
1 changed files with 6 additions and 0 deletions
|
@ -25,6 +25,12 @@ import java.util.Map;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* The main interaction with Z3 happens via the Context.
|
* The main interaction with Z3 happens via the Context.
|
||||||
|
* For applications that spawn an unbounded number of contexts,
|
||||||
|
* the proper use is within a try-with-resources
|
||||||
|
* scope so that the Context object gets garbage collected in
|
||||||
|
* a predictable way. Contexts maintain all data-structures
|
||||||
|
* related to terms and formulas that are created relative
|
||||||
|
* to them.
|
||||||
**/
|
**/
|
||||||
public class Context implements AutoCloseable {
|
public class Context implements AutoCloseable {
|
||||||
private final long m_ctx;
|
private final long m_ctx;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue