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
Matt Thornton
4e0a2f5968
Dispose of intermediate Z3Objects created in dotnet api. ( #5901 )
...
* Dispose of intermediate Z3Objects created in dotnet api.
* Set C# LangVersion to 8.0.
* Fix build errors.
* Fix warning about empty using statement.
* Fix Xor to only dispose of objects that it creates internally.
2022-03-17 08:08:05 -07:00
Nikolaj Bjorner
40e329fc92
remove push/pop for fixedpoint objects from API #2249
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-04-27 10:13:15 -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
bdd8685146
use params for arguments to Fixedpoint methods
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-13 18:09:30 -07:00
Nikolaj Bjorner
310c0f31a1
use type constrsaints for co-variant subtying to enable .net 3.5
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-08-30 12:07:06 +08:00
Christoph M. Wintersteiger
91352369a9
Added conversion functions to ASTVectors in .NET and Java.
...
Fixes #108
2015-05-26 11:20:19 +01:00
Christoph M. Wintersteiger
d8f6d84217
Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality.
...
Fixes #103
2015-05-23 16:53:47 +01: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
Nikolaj Bjorner
08dcd51594
fix bugs in incremental operation of sat solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-27 12:04:54 -07:00
Ken McMillan
c007a5e5bd
merged with unstable
2014-08-06 11:16:06 -07:00
Nikolaj Bjorner
19050d1c4c
merge Fixedpoint.cs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-28 12:20:48 -07:00
Nikolaj Bjorner
44751c0ef8
Add missing .NET API functions for parsing rules into fixedpoint object
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-23 15:27:24 -07:00
Nikolaj Bjorner
330120e406
update documentation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-03-24 03:37:02 -07:00
Nikolaj Bjorner
ff1543d700
fix APIs, add python API
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-03-23 21:28:11 -07:00
Christoph M. Wintersteiger
5fe58c2f2d
Java API: renamed assert_(...) to add(...)
...
.NET API: added alias Add(...) for Assert(...)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-02-26 19:13:48 +00: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
Christoph M. Wintersteiger
c702454f6c
Formatting
...
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-23 00:45:48 +00:00
Nikolaj Bjorner
a935c64e15
expose assertions that are pushed to the context
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-20 21:00:02 -08:00
Nikolaj Bjorner
50385e7e29
add option to validate result of PDR. Add PDR tactic. Add fixedpoint parsing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-17 20:47:49 +01:00
Leonardo de Moura
a274cac2a0
bindings --> api; and moved nlsat/sat/subpaving tactics
2012-10-31 13:25:36 -07:00
