3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Commit graph

49 commits

Author SHA1 Message Date
Nikolaj Bjorner 9b7c66ea7b revert update to netcoreapp version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-12 08:41:43 -07:00
Nikolaj Bjorner ff679e0fce increment version number 2022-09-11 19:02:44 -07:00
Rolf Eike Beer 7f8e2a9f75
clean up CMake code (#5182)
* CMake: simplify FindGMP.cmake

Remove printing of all the different variables, and let FPHSA output the library
name. Add an imported target, which bundles the library and the include
directories for easier usage.

* fix build: vector::c_ptr() now is vector::data()

* CMake: use Threads::Threads imported module

Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect.

* CMake: remove needless policy setting

The minimum required version is CMake 3.4, where these policies are already set
to new because they were introduced earlier.

* CMake: remove needless variable expansion
2021-04-14 10:29:15 -07:00
Nikolaj Bjorner 2d4e9a0f67 update managed APIs for lambda-based array models #2400
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-13 16:20:36 -04:00
Charlie Barto 167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
Nikolaj Bjorner 785fe2f6f7 add main remaining updates from #1815
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-20 12:43:05 -08:00
Nikolaj Bjorner cabe0ee447 integrating additional changes from @yatli pull request #1815
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-20 10:51:44 -08:00
Nikolaj Bjorner 37d9e6d811 incrementally adding files from dotnet core pull request from @yatli
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-20 10:40:11 -08:00
Nikolaj Bjorner 038971c029
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." 2019-01-16 10:21:56 -08:00
Yatao Li 43ee345f01 dotnet deps hack for test 2019-01-15 03:06:36 +09:00
Yatao Li 209ebecb86 cmake: dotnet: example: dotnet.csproj is NETCOREAPP 2019-01-14 00:51:44 +08:00
Yatao Li f0f9a16f85 cmake: dotnet: example: program -> Program 2019-01-14 00:22:51 +08:00
Yatao Li 08adc1bf97 ... 2019-01-13 23:15:40 +08:00
Yatao Li 8ebde41f35 dotnet: example: copy to binary dir before build 2019-01-13 22:45:05 +08:00
Yatao Li 5e79dba3d6 dotnet: move example project build to cmake 2019-01-13 00:03:37 +08:00
Yatao Li f5b874e0a3 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-12-29 16:27:00 +08:00
Nikolaj Bjorner c802a0ac96 fix crash exposed by examples/dotnet/Program.cs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 14:32:59 -07:00
Nikolaj Bjorner 3ba2aa2672 regressions in examples/dotnet/Program.cs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 14:01:43 -07:00
Yatao Li aae28bd0eb CI: update dotnet example to coreclr 2.0 2018-09-12 14:26:21 +08:00
Nikolaj Bjorner 648a531950 update java example to bypass bit-rot
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-02 09:50:29 -07:00
Nikolaj Bjorner e98c808f47 fixing compilation errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-03 03:18:29 -07:00
Nikolaj Bjorner 14d780fb2b fix dotnet example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-02 13:21:42 -07:00
Nikolaj Bjorner 9e59bba80e fix dotnet example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-02 13:20:51 -07:00
Bruce Mitchener 73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner 60af4a5820 deal with ambiguity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-12-04 19:12:51 +05:30
Nikolaj Bjorner 0bfea99cff fix issues found in parsing examples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-12-01 14:43:52 -08:00
Nikolaj Bjorner ab58723ffc fix dotnet example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-29 20:52:19 -08:00
Christoph M. Wintersteiger d8a02bc040 Fixed AST translation functions in .NET and Java APIs. Fixes #1073. 2017-06-14 13:24:54 +01:00
Christoph M. Wintersteiger a334020f2c Added .NET 3.5 solution/project files 2017-01-18 12:32:02 +00:00
Christoph M. Wintersteiger 3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Christoph M. Wintersteiger cbda38ee80 Added finite domain expressions and numerals to the .NET, Java, and Python APIs.
Relates to #318
2015-12-02 17:01:52 +00:00
Christoph M. Wintersteiger 52bbd67cd3 Whitespace 2015-12-02 14:40:47 +00:00
Nikolaj Bjorner 21201371ed add reference equality to Symbols for .NET
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-11 00:53:13 -07: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 9b137d54d3 Bugfix and new examples for implicit assumptions in Z3_solver_assert_and_track. Thanks to Amir Ebrahimi for reporting this issue!
(See http://stackoverflow.com/questions/28558683/modeling-constraints-in-z3-and-unsat-core-cases)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-02-18 16:25:27 +00:00
Christoph M. Wintersteiger b96551a1a2 .NET/Java/ML: Moved toggle_warning_messages to Global, added en/disable_trace.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-02-07 14:17:39 +00:00
Christoph M. Wintersteiger ee2c9095c6 .NET FPA API overhaul
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-08 17:21:29 +00:00
Christoph M. Wintersteiger 0faf329054 FPA API: bugfixes and examples for .NET and Java
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-03 17:26:58 +00:00
Nikolaj Bjorner e180cfe256 optimizing pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-02-25 12:24:48 -08:00
Nikolaj Bjorner e2db1418f9 debugging simplex/pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-02-21 14:39:54 -08:00
Christoph M. Wintersteiger 092dfa396a Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-08-07 15:22:06 +01:00
Christoph M. Wintersteiger 210bca8f45 .NET Example: Sudoku example bugfix. Many thanks to Ilya Mironov for reporting this issue.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-07-02 12:57:54 +01:00
Christoph M. Wintersteiger f50016d8a1 bugfix in .NET example
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-06-14 13:18:33 +01:00
Christoph M. Wintersteiger 8e497fbbaf Extended FPA dotnet example
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-06-14 13:13:14 +01:00
Christoph M. Wintersteiger a9840b291f FPA API: Tied into rest of the API;
added numeral/value handling through existing functions;
added trivial .NET example.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2013-06-10 19:06:45 +01:00
Christoph M. Wintersteiger 4d1d784a1c Java+.Net Examples: refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-12-04 19:32:20 +00:00
Christoph M. Wintersteiger 1ed4e7c480 Managed API: bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-28 22:20:02 +00:00
Leonardo de Moura 4278b2dd51 dotnet example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-28 10:50:36 -07:00
Leonardo de Moura 93fbfd5f94 dotnet example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-28 10:48:11 -07:00