mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity
16765 commits 23 branches 48 tags 157 MiB
Commit graph

2319 commits

Author SHA1 Message Date
Nikolaj Bjorner 8a84cacfea add tuple support for __getitem__ #5815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-06 04:02:12 +02:00
Nikolaj Bjorner e9dad84b85 update documentation comments 2022-02-06 03:35:32 +02:00
Nikolaj Bjorner a189ca8b60 truncation directive #5805 2022-01-31 10:50:46 -08:00
Nikolaj Bjorner a621041308 fix #5795 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:45:38 -08:00
Hennadii Chernyshchyk 85f6456655
Add missing constness (#5787) 2022-01-21 15:32:25 +01:00
Nikolaj Bjorner 36cfb88f5f add preliminary stub to handle closure types 2022-01-17 22:01:31 -08:00
Nikolaj Bjorner dfe2b27f9a #5773 2022-01-12 13:28:15 -08:00
Nikolaj Bjorner 08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner 2bcc814031 add macro to track closures declared in z3_api 
This is to ease integration with external API wrappers that rely on accessing
information about type names that are used.
#5762
 2022-01-12 02:47:39 -08:00
Nikolaj Bjorner d3bc11dd3a bvs have to be expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-10 12:38:25 -08:00
Nikolaj Bjorner 21feefeac5 Add character access functions #5764 2022-01-10 12:33:58 -08: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
Nikolaj Bjorner 6013d5da47 #5755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 14:05:06 -08:00
Nikolaj Bjorner 199daead50 remove Z3_bool_opt #5757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:52:10 -08:00
Nikolaj Bjorner e943bee625 apply delcypher's todo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:25:14 -08:00
Nikolaj Bjorner cf08cdff9c #5747 2022-01-03 08:54:54 -08:00
Nikolaj Bjorner e84ddb0d9a more #5746 2022-01-02 11:33:21 -08:00
Nikolaj Bjorner 88707f37e7 Better error reporting #5746 2022-01-02 11:31:50 -08:00
Nikolaj Bjorner fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
Nikolaj Bjorner 95e26aaad9 #5742 
expose access to constructors/accessors/recognizers given datatype sort
 2021-12-28 11:00:34 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00
Anton Kochkov f3af2193d0
Use Stdlib. instead of Pervasives. due to deprecation (#5730) 2021-12-22 07:53:47 -08:00
Nikolaj Bjorner e0d6e04493 fix c++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-20 16:09:39 -08:00
Nikolaj Bjorner 7a6070506d #5727 
Expose diff function,
expose allchar in Java API
expose op codes for replace/re/all
 2021-12-20 10:17:06 -08:00
Nikolaj Bjorner 6a039c2700 Update z3++.h 
simplify definition
 2021-12-19 11:53:01 -08:00
Nikolaj Bjorner bee742111a na 2021-12-19 11:05:19 -08:00
Nikolaj Bjorner 7441bd706b na 2021-12-19 10:57:42 -08:00
Nikolaj Bjorner 85e362277c Update z3++.h 
with bindings for user propagate functions
 2021-12-18 11:56:05 -08:00
Nikolaj Bjorner f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner 4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner 8ca023d541 expose propagate created 2021-12-17 16:12:47 -08:00
Nikolaj Bjorner 2caa7e6e45 remove EnumToNative as it drops reference counts, fixes #5713 2021-12-16 03:22:54 -08:00
Nikolaj Bjorner b85f2f7e86 #5704 2021-12-12 21:10:07 -08:00
Calvin Loncaric 0405a597d4
Fix return type of as_int64 (#5703) 2021-12-09 14:39:38 -08:00
Nikolaj Bjorner 773a2ae7bc na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 15:08:43 -08:00
Nikolaj Bjorner 1e95fb44d1 add ability to register expressions during callback 2021-12-07 09:47:05 -08:00
Nikolaj Bjorner 0d055b83eb update input for doxygen #5400 2021-12-05 09:04:18 -08:00
Nikolaj Bjorner 41aa7d7b60 stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 09:00:51 -08:00
Nikolaj Bjorner c6a5aa0cc4 try th_lemma, update documentation of api functions for creating strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 09:21:02 -08:00
Nikolaj Bjorner 3c1aedf219 fixing #5473 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 17:08:28 -08:00
Nikolaj Bjorner 5857236f2f introducing base namespace for user propagator 2021-11-29 19:41:30 -08:00
Nikolaj Bjorner 833dd62623 fix #5681 2021-11-24 13:24:31 +01:00
Nikolaj Bjorner fee4821106 include thread 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 21:06:07 +01:00
Nikolaj Bjorner a7d24788c3 wasm build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 20:45:36 +01:00
Nikolaj Bjorner 741c5f43f4 Merge branch 'master' of https://github.com/z3prover/z3 2021-11-19 11:03:08 -08:00
Nikolaj Bjorner ca2c2bb802 ensure smt2log works with multi-threaded consumers, ease scenarios around #5655 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 11:02:50 -08:00
Nikolaj Bjorner 99d5215956 revert use of f format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 00:01:19 -08:00
Nikolaj Bjorner f83367a11e mac builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 22:39:30 -08:00
Nikolaj Bjorner 518ef9f916 fix #5674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 21:14:50 -08:00
Nikolaj Bjorner 3a9656bc59 fixing issues with user propagator from python 
"fresh" remains broken (not working yet).
 2021-11-07 17:04:11 -08:00
Nikolaj Bjorner f2fcbc7cb7 capture values not reference 2021-11-07 13:43:56 -08:00
Clemens Eisenhofer 091079e58c
Added user propagator example (#5625) 
* Added user propagator example

* User propagator example code refactoring
(+ removed unused parameter warning)

* Moved user-propagator example to its own directory
 2021-11-02 15:03:02 -07:00
Henrich Lauko 96671cfc73
Add and fix a few general compiler warnings. (#5628) 
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
 2021-10-29 15:42:32 +02:00
Alexander Traud f5f35f87d0
fix grouping for latest doxygen (#5626) 
Since doxygen 1.8.16, opening and closing a group must not be done as
C comment but as doxygen command. In other words, not one but two
asterisk characters are required so that doxygen finds a group.
 2021-10-27 23:46:31 +02:00
Nikolaj Bjorner 075769c4c0 try get_string contents again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-25 16:03:40 +02:00
Nikolaj Bjorner 45681b4c6e update API type annotation to make it OCaml friendly 2021-10-25 13:43:15 +02:00
Nikolaj Bjorner 3a3cef8fce #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-23 18:21:51 +02:00
Nikolaj Bjorner 7f41d6140f use some suggestions from #5615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-22 12:39:55 -04:00
Nikolaj Bjorner 051616385f remove deprecated escape string from Julia bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-21 19:14:12 -04:00
Nikolaj Bjorner f05ac8a429 updated C++ API for escaped and unescaped strings #5615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-21 14:52:59 -04:00
Nikolaj Bjorner 05e7ed9637 add API to access unescaped strings, update documentation of Z3_get_lstring, #5615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-21 11:30:03 -04:00
CEisenhofer 3557e0b0c5
Added eq/fixed/final functions in C++ user propagator as methods (#5607) 2021-10-19 10:48:31 -04:00
Simon Cruanes 6302b864c8
tweak GC in OCaml bindings (#5600) 
* feat(api/ml): use custom block hints to guide the GC

this forces the GC to collect garbage when a few _large_ objects
(solver, etc.) are dead. The current code would let arbitrarily many
such objects die and not trigger a GC (which would have to come from
OCaml code instead)

* tuning

* try to use caml_alloc_custom_mem with fake sizes

* try to fix leak by explicitly finalizing OCaml context

* chore: use more recent ubuntu for azure CI

* remove finalizer causing segfault in example
 2021-10-14 12:46:14 -07:00
Nikolaj Bjorner ff723f15ff Update z3++.h 2021-09-29 12:19:02 -07:00
Nikolaj Bjorner 3abecc3428 add extra commands to API parser 2021-09-27 14:19:43 -07:00
Jamey Sharp 426306376f
CNF conversion refactoring (#5547) 
* split sat2goal out of goal2sat

These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.

I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.

* limit solver_core methods to those needed by goal2sat

And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.

I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
 2021-09-20 08:53:10 -07:00
CEisenhofer c58b2f4a9c
Added character functions to API (#5549) 
* Added character functions to API

* Changed names of c++ functions
 2021-09-15 13:34:58 +01:00
Nikolaj Bjorner 55285b2193 make it easier to iterate over arguments of an application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:51:59 -07:00
Nikolaj Bjorner ba68fba419 build 2021-09-01 17:10:23 -07:00
Nikolaj Bjorner 0c53c139da add to_string method to make it easier to use without << 2021-09-01 15:37:58 -07:00
Nikolaj Bjorner f91c3d9fd6 round-tripping escapes, again #5519 2021-08-31 20:36:38 -07:00
Nikolaj Bjorner 90f98d5791 fix part of #5519 
generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right.
 2021-08-31 20:06:06 -07:00
pcarbonn cd2701da0c
fix the use of ctx in Q() (#5521) 
* fix #4956

* fix: use ctx in Q()
 2021-08-31 10:01:47 -07:00
Nuno Lopes 9b5ec6d004 logging cleanup 
move everything out-of-line as common path doesn't log
fix some race conditions on file ptr vs enable_logging vars
 2021-08-29 12:24:19 +01:00
Nuno Lopes 9a172939e0 fix logging in Z3_fpa_get_[es]bits 2021-08-29 10:58:54 +01:00
Nikolaj Bjorner b1bc890992 fix #5515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 18:05:51 -07:00
Nuno Lopes e5a2f08cc9 fix logging of Z3_mk_lambda and Z3_mk_lambda_const 
In preparation of a bug report just for you @NikolajBjorner
 2021-08-29 00:37:45 +01:00
Nikolaj Bjorner 828fc72754 types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 18:55:53 -07:00
Nikolaj Bjorner d6848175eb re-add API for creating propagator from a context for "fresh" 2021-08-26 18:12:40 -07:00
Nikolaj Bjorner f7c1ed8273 missing this 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-26 10:41:37 -07:00
Nikolaj Bjorner 4d39af3d7b #5507 missing init 2021-08-26 09:37:06 -07:00
Nikolaj Bjorner 5fa1b0b09f update project description #5503 2021-08-24 09:48:33 -07:00
Nikolaj Bjorner 592c53e46d char sort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 20:45:26 -07:00
Nikolaj Bjorner 170ef1dcca add character sort to Python API and allchar function to API for ease. #5500 2021-08-23 20:02:50 -07:00
Nikolaj Bjorner 15e3e81cb5 remove likely culprit for #5493 
@zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in #5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes #5493
 2021-08-19 21:08:20 -07:00
Nikolaj Bjorner d980ee0533 fix regression in FPNumRef sign 2021-08-18 10:00:22 -07:00
Nikolaj Bjorner 7f88cfe727 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 10:10:20 -07:00
Nikolaj Bjorner 1884ad5b2f expose method for updating python model for constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 09:09:04 -07:00
Nikolaj Bjorner c8a83749dd #5484 2021-08-16 11:19:22 -07:00
Nikolaj Bjorner 2704fb5fd5 expose n-ary xor 2021-08-14 10:52:09 -07:00
intrigus-lgtm 35698c650d
Add AssertSoft String overload for Java Api (#5475) 
This adds a String overload for AssertSoft.
Previously only integer weights could have been used,
limiting the user. With Strings the user can now use
e.g. Java's BigInteger class converted to a String instead.
 2021-08-12 09:18:18 -07:00
Nikolaj Bjorner 38250fc304 re-move #5442 2021-07-29 15:33:30 -07:00
Nikolaj Bjorner 79296d8dfc proviso for different life-time of objects allocated in arguments. 2021-07-27 09:09:21 -07:00
Nikolaj Bjorner 5964b26ca2 err 2021-07-27 09:07:34 -07:00
Nikolaj Bjorner 7cb4932ae8 fix #5435 2021-07-27 09:04:29 -07:00
Nikolaj Bjorner 0ba518b0c0 avoid perf abyss for macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-20 20:07:06 -07:00
CEisenhofer 0fa4b63d26
Added sbv2s (#5413) 
* Added sbv2s

* Fixed indention

Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
 2021-07-16 17:58:28 +02:00
Nikolaj Bjorner 79c261736b charsort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 19:50:41 +02:00
Nikolaj Bjorner 97a035fd6d add char sort to .net 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 19:43:12 +02:00
Nikolaj Bjorner 1b648437b7 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 17:42:34 +02:00
Nikolaj Bjorner a3010c8875 version inc, bvsort->bitvecsort 2021-07-13 17:14:47 +02:00
Nikolaj Bjorner 7ae78da850 adding access to characters over API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 15:56:08 +02:00
Marc Mosko 8a33391708
Expose optimize.assertAndTrack to Java (#5387) 
Co-authored-by: Marc Mosko <mmosko@parc.com>
 2021-07-06 01:22:00 -07:00
Gabriel Radanne 0c7625cd26
Remove size argument in OCaml's Z3.mk_re_intersect (#5383) 
* Remove size argument in OCaml's `Z3.mk_re_intersect`

Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.

* Enable the ocaml documentation in Seq.

Turn all the comments into proper documentation comments.
 2021-07-06 01:21:04 -07:00
Nikolaj Bjorner 7255a2afd1 fix #5379 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 18:43:11 +02:00
Nikolaj Bjorner f3737f6831 #5361 2021-06-21 14:58:00 -07:00
Gram 589f99eea9
Fix Flake8 violations in Python API (#5332) 
* Fix flake8 violations in z3.py

* Fix flake8 violations in z3printer.py

* Fix flake8 violations in z3rcf.py and z3util.py

* do not allocate list on every call to set_default_rounding_mode
 2021-06-16 10:49:47 -05:00
Nikolaj Bjorner 9c6b29164d #5337 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-15 12:31:40 -05:00
Nikolaj Bjorner 3e773fba5e get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:07:48 -07:00
Gram 3d8865d925
Fix some PEP-8 violations in Python code (#5295) 
* reformat python code using autopep8

* manually wrap some too long lines and adjust some checks

* run autopep8 in aggressive mode

* run autopep8 in very aggressive mode

* manually reformat z3types.py

* unify: use double quotes

* use sys.version_info instead of sys.version

* drop accidentally commited src/util/z3_version.h
 2021-05-23 10:27:55 -07:00
Nuno Lopes f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nikolaj Bjorner 8ba0fb5b58 rounding mode sort removed for incompatibility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 16:18:43 -07:00
Nikolaj Bjorner e63e4587a4 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 15:41:12 -07:00
Mikhail R. Gadelha ed59c838bf
Implemented missing methods to the C++ API (#5242) 
* Add method to print Sort to an ostream

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Added new FP check methods and clarify documentation

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Added missing fp conversion calls to C++ API

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Added method to convert a bv (in ieee format) to fp

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Added bv reduction methods to C++ API

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Add fp equality method

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Added methods to creates fpa nan and fpa inf

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Changed default rounding mode of the C++ API to RNE (see issue #4673)

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>

* Added methods to generate rounding mode sorts and rounding mode numerals

Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
 2021-05-21 14:10:09 -07:00
Matt Thornton 9cc1549dbe
Use osx-x64 for mac rid rather than macos. (#5288) 2021-05-20 15:19:31 -07:00
Nikolaj Bjorner ec034679ce #5215 
memory leaks
 2021-05-19 12:42:38 -07:00
Zachary Wimer f942c3df91
operator= checks this equality before moving (#5265) 2021-05-12 13:10:14 -07:00
Philipp Schröer 7373946d67
julia: fix duplicate method (#5251) 
Resulted in "Double registration for method" errors when loading Z3.jl
with a current build of Z3.
 2021-05-07 14:00:33 -07:00
Zachary Wimer 77dea18f54
Added missing fp conversion methods to C++ API (#5234) 2021-04-30 18:45:28 -07:00
Zachary Wimer e4b660321f
Cpp api string const (#5228) 
* string_const added

* typo fixed
 2021-04-29 16:16:48 -07:00
Nikolaj Bjorner a8ccbd7103 fix #5226 2021-04-29 13:36:25 -07:00
Nikolaj Bjorner d731ec7cba
Revert "Cpp api fp to bv (#5218)" (#5221) 
This reverts commit fa2d593739.
 2021-04-27 08:44:15 -07:00
Zachary Wimer fa2d593739
Cpp api fp to bv (#5218) 
* fpa_to_ubv and fpa_to_sbv added to C++ API

* Bug fix

* fpa_fp method added to API

* Adjust types to prefer sort over expr and bug fix
 2021-04-26 17:00:05 -07:00
Nikolaj Bjorner 0422b59123 build 2021-04-24 16:37:03 -07:00
Nikolaj Bjorner 385109d484 regarding #5206 2021-04-24 14:25:26 -07:00
Nikolaj Bjorner 44d77a978a cw review comments #5200 2021-04-20 09:27:59 -07:00
Zachary Wimer 831afa8124
Cpp api add missing fp methods (return type correction) (#5200) 
* added is_nan and is_inf to API

* added support to to_ieee_bv

* bug fix
 2021-04-19 17:55:23 -07:00
Zachary Wimer 10e9345cd7
C++ API add missing FP methods (#5199) 
* added is_nan and is_inf to API

* added support to to_ieee_bv
 2021-04-19 15:24:09 -07:00
Zachary Wimer 542878dea3
Add sge and sgt to API; now has sge,sgt,sle,slt, and unsigned counterparts (#5194) 2021-04-19 08:53:43 -07:00
Zachary Wimer f8228ff50e
[c++ api] add const (#5195) 2021-04-19 10:24:12 +01:00
Zachary Wimer a1741e0e16
z3 c++ api: delete implicit constructor (#5191) 2021-04-16 10:46:03 +01:00
Zachary Wimer 239ace4353
expr move semantics supported via ast (#5190) 2021-04-15 13:37:31 -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 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nuno Lopes 49906a5a58 api_context: remove basic&arith fids fields 
these are now constant,s o we can save some space
the remaining ones need to be made constant as well..
 2021-04-13 17:42:42 +01:00
Nuno Lopes afdf80509a remove api_context::m_search as it's always constant (false) 2021-04-13 17:32:17 +01:00
Nuno Lopes 853ce099ec api_context: consolidate ast trail vectors 
a context never changes between user rc/non-user rc, so we can reuse the trail for both options
and save memory & smallish speedup
 2021-04-13 17:21:42 +01:00
Zachary Wimer f4127bd6f3
Remove function arg names for deleted functions (#5176) 2021-04-12 14:37:44 -07:00
Zachary Wimer 8e6ab5b1bf
prefer parent operator= to manually copying parent data for extensibi… (#5177) 
* prefer parent operator= to manually copying parent data for extensibility reasons

* typos fixed
 2021-04-12 14:37:27 -07:00
Zachary Wimer dd3be32b98
Cpp api general minor improvements (#5175) 
* Added noexcepts, deleted trivial copy functions that can be implcit, small things

* Add back in virtual destructor. This has rule of 5 side effects, but move semantics are not supported yet so it is *mostly* ok. The move PR will address this.
 2021-04-12 14:03:20 -07:00
Zachary Wimer 70604a6856
Explicitly delete private constructors (#5174) 2021-04-12 13:46:55 -07:00
Zachary Wimer 973f79dc4d
rename final to register_final since final is a specifier in C++11+ (#5172) 2021-04-12 13:38:03 -07:00
Zachary Wimer 4625454a38
Fix fixedpoint rc bug and fix optimize non-const bug (#5173) 
* Fix fixedpoint rc bug and fix optimize non-const bug

* Fix indentation
 2021-04-12 13:37:05 -07:00
Zachary Wimer d73b883b38
array uses unique_ptr (#5171) 
* array uses unique_ptr

* Constructor initalize m_array over set it

* prefer arr.get() to &arr[0]
 2021-04-12 13:01:24 -07:00
Nikolaj Bjorner 54f04a5751 being deliberate non-null #5156 2021-04-10 16:10:35 -07:00
Nikolaj Bjorner d91eac24b7 more missing nullptr flexibility #5156 2021-04-08 10:34:09 -07:00
Nikolaj Bjorner b1f5933c7d fix missing nullptr check for #5156 2021-04-08 10:30:33 -07:00
Nikolaj Bjorner d9af8ea9fb fix #5113 2021-04-07 12:20:12 -07:00
Nikolaj Bjorner 94b4d1b442 fix travis build for python doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-29 15:30:31 -07:00
Zachary Wimer 531a828c57
Update setup.py to use cmake build system (#5128) 2021-03-28 14:17:33 -07:00
Alexander Kreuzer dc5fa89de3
Mixing Integers and Rational in the new Java API #5085 (#5098) 
* Added covariance to arithmetic operations

* Added distillSort

* Update JavaGenericExample.java

Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 05:24:23 -07:00
Nikolaj Bjorner d03fdf5fed more descriptive naming convention 2021-03-15 15:48:33 -07:00
Nikolaj Bjorner 4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner 8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Graydon Hoare e8b3c90e14
Fix unintentional re-import of package z3 in z3printer, in python3. (#5082) 2021-03-06 10:44:07 -08:00
Nikolaj Bjorner e804f7743a
Revert "Adjust imports so z3.z3 is still available in python3 (#5079)" (#5081) 
This reverts commit 957d7bfe35.
 2021-03-05 15:26:00 -08:00
Graydon Hoare 957d7bfe35
Adjust imports so z3.z3 is still available in python3 (#5079) 2021-03-04 17:18:39 -08:00
Nikolaj Bjorner f7b1469462 Try freeing context in dispose method and not wait for finalizer #5043 2021-02-27 11:02:58 -08:00
Nikolaj Bjorner 08f55f9d1f start wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-26 11:13:44 -08:00
Nikolaj Bjorner be68456c06 java compilation? 2021-02-26 05:04:46 -08:00
Nikolaj Bjorner 06caf57a86 fix #5033 2021-02-26 03:42:13 -08:00
Nuno Lopes 5e034e495f fix compiler warnings 2021-02-19 10:33:41 +00:00
Nuno Lopes bcad4d9435 revert my mess with the ast hashtable 
will share results form the experiments later
 2021-02-17 14:29:07 +00:00
Nikolaj Bjorner 1da7522893 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-14 17:47:19 -08:00
Nikolaj Bjorner 04a1d4245c fix #4801 2021-02-12 20:20:00 -08:00
Nikolaj Bjorner c808f74591 fix multiplier base for #5022 
add also some C++ API shorthands for retrieving numerals
 2021-02-12 11:53:40 -08:00
Nikolaj Bjorner 2e648e2f02 glibc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 13:19:23 -08:00
Nikolaj Bjorner 98eae28fca try to update setup.py to libc naming 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:52:05 -08:00
Nikolaj Bjorner 692f159af8 try without format 2021-02-09 12:49:55 -08:00
Nikolaj Bjorner e722589810 address some of the ugliness pointed out by abandoned pull request #5008 2021-02-09 11:23:16 -08:00
Nikolaj Bjorner 0f29fff836 remove bit-vector dependencies in seq theory 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 43d1ef2fee iterable is a Python 3 thingy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-07 18:22:57 -08:00
Nuno Lopes 682b947ad3 the documentation of Z3_model_get_func_interp() says it returns NULL if there's no interpretation 
so let's honour that instead of throwing an exception
 2021-02-07 12:46:36 +00:00
Nuno Lopes e1572096ca delete some dead code 2021-02-07 12:14:52 +00:00
Julius Marozas 01d5f3259c
Fix show parameter in prove, solve, and solve_using (#5001) 
* Fix show parameter in prove function

* Fix show in solve & solve_using

* Use Python 2 compatible syntax

* Add default value for show
 2021-02-06 16:42:15 -08:00
Nikolaj Bjorner e856cfc458 coercions 2021-02-06 10:35:28 -08:00
Nikolaj Bjorner 16448104eb add new model event handler for incremental optimization 2021-02-05 17:11:04 -08:00
Nikolaj Bjorner 2c472aaa10 #4999 
use typing Iterable
 2021-02-05 12:09:24 -08:00
Nikolaj Bjorner a582014854 #4999 2021-02-05 12:01:30 -08:00
Malte Mues 5d8d42b1fa
Update the mkConstant parameter type (#4996) 2021-02-04 16:17:49 -08:00
Nikolaj Bjorner dfb7c87448 #4997 2021-02-04 15:46:34 -08:00
Nikolaj Bjorner cc39cf037e build again 2021-02-04 12:36:44 -08:00
Nikolaj Bjorner b3144a534d remove string conversion causing regression 2021-02-03 21:40:45 -08:00
Nikolaj Bjorner abcabba9fe fix python build 2021-02-03 09:57:16 -08:00
Nikolaj Bjorner 8f577d3943 remove ast_manager get_sort method entirely 2021-02-02 13:57:01 -08:00
Nikolaj Bjorner 3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner cfcd7f18a9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 17:09:12 -08:00
Nikolaj Bjorner 5414030875 #4939 escape character 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 11:57:00 -08:00
Nikolaj Bjorner 49aebdbb02 adding unicode fixup base on #4939 discussion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 20:21:46 -08:00
Nikolaj Bjorner e61949059d compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 19:50:34 -08:00
Nikolaj Bjorner e26e38b654 add error generation for #4977 2021-01-26 14:55:42 -08:00
Nikolaj Bjorner a0b7879dd9 handle signed characters convertions into unsigned numbers 2021-01-26 11:20:28 -08:00
Nikolaj Bjorner 7dd7d83a36 make it easier to use string literals 2021-01-26 11:01:03 -08:00
Nikolaj Bjorner dccfecb488 generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-25 19:18:55 -08:00
Nikolaj Bjorner 2646e0a1c0 have add_soft accept an interable of Booleans. 2021-01-25 12:17:35 -08:00
Nikolaj Bjorner 2ead209d40 indentation and updated links to default landing pages 2021-01-11 13:21:52 -08:00
Nikolaj Bjorner bcbda45298 updates to doc 2021-01-11 13:03:55 -08:00
Nikolaj Bjorner 396bfa05f3 fix grouping error 2021-01-11 12:25:53 -08:00
Nikolaj Bjorner 1a71dfac6f play nicebox #4918 2021-01-09 01:39:29 -08:00
Nikolaj Bjorner 26af694d2c add overloads to != and == based on #4906 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:04:01 -08:00