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

46 commits

Author SHA1 Message Date
Victor Paléologue 8b29f40152
Fix build on Mac (#6146)
* Fix finding Python on Mac

On Mac you have to specify the version.
It also works well on other platforms this way.

* Ignore CMake build directories from index

* Fix warning about unused variable in release

The variable is used in debug only,
but it's legit that the compiler does not warn us for that in release.
2022-07-11 09:46:23 -07:00
Olaf Tomalka 7fdcbbaee9
Add high level bindings for js (#6048)
* [Draft] Added unfinished code for high level bindings for js

* * Rewrote structure of js api files
* Added more high level apis

* Minor fixes

* Fixed wasm github action

* Fix JS test

* Removed ContextOptions type

* * Added Ints to JS Api
* Added tests to JS Api

* Added run-time checks for contexts

* Removed default contexts

* Merged Context and createContext so that the api behaves the sames as in other constructors

* Added a test for Solver

* Added Reals

* Added classes for IntVals and RealVals

* Added abillity to specify logic for solver

* Try to make CI tests not fail

* Changed APIs after a round of review

* Fix test

* Added BitVectors

* Made sort into getter

* Added initial JS docs

* Added more coercible types

* Removed done TODOs
2022-06-14 09:55:58 -07:00
Nikolaj Bjorner 9011100df2 Update .gitignore 2022-03-21 15:25:35 -07:00
Kevin Gibbons 2b934b601d
Add WebAssembly/TypeScript bindings (#5762)
* Add TypeScript bindings

* mark Z3_eval_smtlib2_string as async
2022-01-09 17:16:38 -08:00
Zachary Wimer 531a828c57
Update setup.py to use cmake build system (#5128) 2021-03-28 14:17:33 -07:00
Nikolaj Bjorner 26b4ab20db Update .gitignore 2020-12-14 17:34:02 -08:00
Nikolaj Bjorner 2953d3ed30 ignore my shortcut
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-12 09:10:40 -07:00
Nikolaj Bjorner 95a78b2450
updates to seq and bug fixes (#4056)
* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4037

* nicer output for skolem functions

* more overhaul of seq, some bug fixes

* na

* added offset_eq file

* na

* fix #4044

* fix #4040

* fix #4045

* updated ignore

* new rewrites for indexof based on #4036

* add shortcuts

* updated ne solver for seq, fix #4025

* use pair vectors for equalities that are reduced by seq_rewriter

* use erase_and_swap

* remove unit-walk

* na

* add check for #3200

* nits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* name a type

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove fp check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unsound axiom instantiation for non-contains

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix rewrites

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4053

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4052

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-22 13:18:55 -07: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 53eaab4709 dotnet: update build scripts 2019-01-12 17:38:24 +08:00
Yatao Li ffd26e5a56 .net: remove net35 related build props; drop src/api/dotnet/core 2019-01-12 15:01:05 +08:00
Nuno Lopes 178e5b31e8 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 22:49:06 +00:00
Dan Liew 4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Andrew Dutcher 0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Dan Liew 20d3bf4d0c [CMake] Implement support for building the .NET bindings.
When using Mono support for installing/uninstalling the bindings
is also implemented. For Windows install/uninstall is not implemented
because the python build system does not implement it and Microsoft's
documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx)
says that the gacutil should only be used for development and not for
production.

For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS``
is enabled and the .NET toolchain is native Windows. Someone with
better knowledge of how to correctly install assemblies under Windows
should implement this or remove this message.

A notable difference from the Python build system is the
``/linkresource:`` flag is not passed to the C# compiler. This means
a user of the .NET bindings will have to copy the Z3 library (i.e.
``libz3.dll``) to their application directory manually. The reason
for this difference is that using this flag requires the working
directory to be the directory containing the Z3 library (i.e.
``libz3.dll``) but setting this up with multi-configuration generators
doesn't currently seem possible.
2016-03-27 15:04:04 +01:00
Dan Liew a5f8ceaa48 Add globbing patterns to `.gitignore` so the files copied
over by the ``contrib/cmake/bootstrap.py`` script are ignored
and so don't get accidently commited.
2016-03-04 15:26:09 +00: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 e754aa1c11 Minor adjustments after rebasing ml-ng onto unstable.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:17:58 +00:00
Christoph M. Wintersteiger ec0b12ecd1 ML API refactoring (z3native.c -> z3native_stubs.c)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:12:48 +00:00
Christoph M. Wintersteiger e2ac8c73d9 ML API temp files added to .gitignore
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:51:26 +00:00
Christoph M. Wintersteiger dcd6f1f697 More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:49:26 +00:00
Christoph M. Wintersteiger a40433aae8 More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:13:58 +00:00
Christoph M. Wintersteiger 1579da02b0 More new ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:13:30 +00:00
Christoph M. Wintersteiger 4f0e8a1057 ML API refactoring (z3native.c -> z3native_stubs.c)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:06:08 +00:00
Christoph M. Wintersteiger a965d65901 ML API temp files added to .gitignore
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 15:41:17 +00:00
Christoph M. Wintersteiger 65ddf2be49 More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 15:40:39 +00:00
Christoph M. Wintersteiger f5a0520b83 More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 15:40:37 +00:00
Christoph M. Wintersteiger 03a5c88ded More new ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 15:40:10 +00:00
Nikolaj Bjorner 08cb8b8de8 address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-09 16:04:25 +01:00
Christoph M. Wintersteiger 0713535fa6 Documentation website fixes.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-24 21:00:23 +01:00
Christoph M. Wintersteiger 7d196201dc fixed warnings
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-24 12:33:20 +01:00
Christoph M. Wintersteiger c3b7c738f8 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt
Conflicts:
	scripts/mk_project.py
	src/duality/duality.h
	src/duality/duality_solver.cpp
	src/duality/duality_wrapper.h
	src/interp/iz3hash.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-25 22:18:41 +01:00
Christoph M. Wintersteiger aa006fa237 added dotnet generated files to .gitignore
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-09 11:31:44 +01:00
Anh-Dung Phan 5921628f53 Dump opt_solver checksat calls for profiling 2013-11-13 18:46:18 -08:00
Leonardo de Moura 349c21d4de Add configure script that is just a wrapper for python 'src/mk_make.py'. It makes the build more user friendly for users familiar with ./configure + make idiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-13 11:34:05 -08:00
Leonardo de Moura 71aec11a04 Ignore callgrind files and Python pyo files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-26 15:50:09 -08:00
Leonardo de Moura 4f9442864a auto generation of parameter helper
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 15:31:40 -08:00
Leonardo de Moura cf28cbab0a saved params work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 17:19:12 -08:00
Christoph M. Wintersteiger 00ebabcc6e Ignoring more common build directories
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-28 21:30:22 +00:00
Christoph M. Wintersteiger 9b9b7a6980 Java API: .gitignore updated
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-27 19:02:15 +00:00
Christoph M. Wintersteiger 3f548c7610 Java API: .gitignored auto-generated files and java class files.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-27 19:01:30 +00:00
Leonardo de Moura badb81998d updated .gitignore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-22 10:11:39 -08:00
Leonardo de Moura 6c11a78e61 fixed .gitignore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-20 08:41:45 -08:00
Leonardo de Moura 051e84de20 Updated .gitignore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-20 08:40:05 -08:00
Leonardo de Moura 92b6a257ef Added .gitignore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-20 08:37:46 -08:00