mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity
18579 commits 24 branches 48 tags 158 MiB
Commit graph

583 commits

Author SHA1 Message Date
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
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
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
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
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
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
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
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
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
c3c7aad1a8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-06 11:18:37 -08:00
Andy Wright
34e0e26e3d
Fixed model translate method in Python API (#4753) 2020-10-25 15:42:17 -07:00
Nikolaj Bjorner
367e5fdd52
delay internalize (#4714) 
* adding array solver

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

* use default in model construction

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

* debug delay internalization

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

* bv

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

* arrays

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

* get rid of implied values and bounds

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

* redo egraph

* remove out

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

* remove files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-28 19:24:16 -07:00
Nikolaj Bjorner
b992f59aad expose name inclusion as optional 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 10:32:17 -07:00
Nikolaj Bjorner
c722962124 fix regressions in python API for user-propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 10:55:43 -07:00
Nikolaj Bjorner
96f10b8c1c user propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-22 19:01:04 -07:00
Nikolaj Bjorner
a58b8ceced na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 19:48:12 -07:00
Nikolaj Bjorner
2d5b749745 extend solver callbacks with methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 19:24:59 -07:00
Nikolaj Bjorner
080be7a2af merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 12:14:28 -07:00
Nikolaj Bjorner
79aa3457c1 prop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-19 10:39:51 -07:00
Nikolaj Bjorner
4857d60c99 user propagator over the API 2020-08-18 21:53:02 -07:00
Nikolaj Bjorner
747a8ff72a initial sketch of python bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-18 10:41:47 -07:00
Nikolaj Bjorner
59d8895d15 add accessors for implied values to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-28 19:46:39 -07:00
Nikolaj Bjorner
e1d2b88a82 access polynomial expressions from algebraic numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-23 15:08:11 -07:00
Nuno Lopes
44ec259c4c fix python test 2020-07-11 22:33:47 +01:00
Nikolaj Bjorner
4b346ef693 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:58:42 -07:00
Nikolaj Bjorner
4a8533e41f enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:17:54 -07:00
pinzaghi
aec8000bda
in check method, as_ast() call fails when True passed as assumption (#4550) 2020-06-29 09:59:10 -07:00
Nikolaj Bjorner
9bc5552ca2 add vcrunime pattern to distribution directive #4542 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-25 08:56:13 -07:00