Nikolaj Bjorner
edeeded4ea
remove DecRefQueue, use Z3_enable_concurrent_dec_ref ( #6332 )
...
The notion of reference counted contexts never worked.
The reference count to a context only ends up being 0 if the GC kicks in and disposes the various z3 objects. A call to Dispose on Context should free up all resources associated with that context. In exchange none of the resources are allowed any other operation than DecRef. The invocations of DecRef are protected by a lock and test on the context that the native pointer associated with the context is non-zero. Dispose sets the native pointer to zero.
Z3_enable_concurrent_dec_ref ensures that:
- calls to decref are thread safe. Other threads can operate on the context without interference.
The Z3_context ensures that
- z3objects allocated, but not disposed during the lifetime of Z3_context are freed when Z3_context is deleted (it triggers a debug warning, but this is now benign).
2022-09-11 18:59:00 -07:00
Nikolaj Bjorner
3d37060fa9
remove dependencies on contracts
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 10:24:36 -07:00
Nikolaj Bjorner
0d4b4b30b1
change storage layout of .Net binding Z3_bool to byte to deal with uninitialized memory reads on larger allocation sizes. Bug introduced when switching from defining Z3_bool as int to the bool type from stdbool
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-02 02:58:06 -07:00
Nikolaj Bjorner
f1d27cd487
workaround non-deterministic behavior of is_irrational_numeral test
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-29 18:16:32 -07:00
Nikolaj Bjorner
ef31b27d5e
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-30 14:36:45 -07:00
Nikolaj Bjorner
c513f3ca09
merge with master
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Nikolaj Bjorner
5ee30a3cd9
include special functionality in parsers for solvers and opt for additional file formats
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-12-03 20:00:24 +01:00
Nikolaj Bjorner
38e4fb307c
add useful shorthands to Solver interface
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-13 00:00:06 -08:00
Nikolaj Bjorner
52619b9dbb
pull unstable
...
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-04-01 14:57:11 -07:00
Christoph M. Wintersteiger
4bed5183f8
Made DRQ objects public in Java and .NET APIs.
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-30 21:58:43 -06:00
Christoph M. Wintersteiger
3b78509d0a
Improved memory use of the .NET API
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-30 20:45:16 -06:00
Christoph M. Wintersteiger
fc227e3c96
.NET API documentation bugfixes
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 15:49:16 +00:00
Nikolaj Bjorner
ce18421a7a
fix box
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-15 14:29:39 -07:00
Christoph M. Wintersteiger
0e4e72b1bc
Added new params.Add functions to the .NET and Java APIs.
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-14 13:22:12 +01:00
Nikolaj Bjorner
a0cdeb2cfe
add useful API for parameter setting
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-13 14:20:53 -07:00
Christoph M. Wintersteiger
7defd469bb
Managed API: Refactoring and formatting.
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-23 18:30:51 +00:00
Leonardo de Moura
a274cac2a0
bindings --> api; and moved nlsat/sat/subpaving tactics
2012-10-31 13:25:36 -07:00
