mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity
17534 commits 23 branches 48 tags 157 MiB
Commit graph

14843 commits

Author SHA1 Message Date
Jakob Rath
d9a63ce786 fix 2022-08-22 15:05:29 +02:00
Jakob Rath
9fcea37625 remove constructor 2022-08-22 15:00:35 +02:00
Jakob Rath
28ddd4ad56 Implement unilinear subsumption as clause simplification 2022-08-22 14:55:02 +02:00
Jakob Rath
c1e2ea80f5 make explicit that we compare the concrete values 2022-08-22 14:17:47 +02:00
Jakob Rath
3a759c1a28 move fi_record 2022-08-22 14:14:30 +02:00
Jakob Rath
26fcfc6ecd Add default constructor to fi_entry 2022-08-22 14:03:43 +02:00
Jakob Rath
3c093e03cf log 2022-08-22 12:46:47 +02:00
Jakob Rath
53f276d225 apply 2022-08-22 12:44:56 +02:00
Jakob Rath
bf1a7914cd Add clause simplification stub 2022-08-22 12:36:05 +02:00
Jakob Rath
3e99828c3c start make_asserting for non-unit coeff 2022-08-19 17:06:28 +02:00
Jakob Rath
ee208efdc5 fix 2022-08-19 16:18:13 +02:00
Jakob Rath
c3e7bd34d0 make_asserting for unit coefficients 2022-08-19 16:02:56 +02:00
Jakob Rath
9766ad00b1 Revert "remove overcomplicated search_iterator" 
This reverts commit 309473edad.
 2022-08-19 14:12:57 +02:00
Nikolaj Bjorner
31ffe89480 normalize more pretty printing 2022-08-17 08:24:41 -07:00
Jakob Rath
309473edad remove overcomplicated search_iterator 2022-08-17 09:37:43 +02:00
Jakob Rath
201d841a90 lit_pp with extra information 2022-08-17 09:29:00 +02:00
Jakob Rath
618b3945c1 log 2022-08-05 11:23:02 +02:00
Jakob Rath
abed6fa6e1 Print polysat variable mapping in debug mode 2022-08-04 14:50:31 +02:00
Jakob Rath
bab8d817ef Remove decisions on lemmas 2022-08-04 14:24:20 +02:00
Jakob Rath
d5f20dcf0e No more boolean decisions 2022-08-04 14:12:12 +02:00
Jakob Rath
c67024d88b unused for now 2022-08-04 13:52:29 +02:00
Jakob Rath
a3e8124245 comments; move a section 2022-08-04 11:52:34 +02:00
Jakob Rath
4282cfa148 Remove unused variable 2022-08-04 08:55:04 +02:00
Jakob Rath
d7f0181c46 Merge branch 'master' into polysat 2022-08-04 08:53:34 +02:00
Jakob Rath
014fe4e3fd fallback stats 2022-08-04 08:51:24 +02:00
Bruce Mitchener
8a3556e5ba cmake: Remove dep on mk_util.py for update_api.py calls. 
update_api.py doesn't depend on mk_util.py any longer, so these
dependencies can go away.
 2022-08-04 07:54:26 +03:00
Saloed
d908ebec4c fix memory_high_watermark parameter according to documentation 2022-08-03 18:50:54 +03:00
Jakob Rath
b9588af07a fix output 2022-08-03 10:01:54 +02:00
Bruce Mitchener
d8c99480c6 test/lp: Replace if linux with if not windows. 
This is stuff that works on posix, so we can flip the check.
 2022-08-03 08:22:54 +03:00
Bruce Mitchener
112dba559f Remove unused private member from smaller_pattern. 2022-08-03 08:21:32 +03:00
Nikolaj Bjorner
774ce3d7ab create special case for osx arm 
shortcut when store/select are distinct

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-03 07:56:02 +03:00
Bruce Mitchener
42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL. 
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
 2022-08-02 17:39:10 +03:00
Bruce Mitchener
8313282cda Use char version of find_last_of when possible. 2022-08-02 17:38:11 +03:00
Jakob Rath
a76f977f85 Change univariate fallback solver to one-shot mode for now 2022-08-02 12:42:34 +02:00
Jakob Rath
6c4d60c5af Basic support for non-copyable types in map 2022-08-02 12:31:29 +02:00
Jakob Rath
e105a91d4a Merge branch 'master' into polysat 2022-08-02 11:31:01 +02:00
Bruce Mitchener
886c3abec1 Remove remnants of _MP_MSBIGNUM checks. 2022-08-02 09:28:57 +03:00
Bruce Mitchener
9a99c78ffb Enable thread_local code more broadly. 
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)

`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
 2022-08-02 09:24:51 +03:00
Bruce Mitchener
82d853e5f8 Use = delete to delete special methods. 
This provides a better experience than just marking them as
private and leaving them as undefined symbols.
 2022-08-02 09:23:14 +03:00
Jakob Rath
2c2ab0d57a Additional BV matchers 2022-08-01 18:37:11 +03:00
Jakob Rath
5d858da58a union_find::reserve 2022-08-01 18:37:11 +03:00
Jakob Rath
e8e64d3098 dlist::insert_before/after 2022-08-01 18:37:11 +03:00
Jakob Rath
de6a0ab1a7 PDD operations 2022-08-01 18:37:11 +03:00
Jakob Rath
42233ab5c8 Additional BDD operations; BDD vectors and finite domain abstraction 2022-08-01 18:37:11 +03:00
Jakob Rath
9275d1e57a sparse_matrix iterators 2022-08-01 18:37:11 +03:00
Jakob Rath
6eae27ffad numeral helper functions 2022-08-01 18:37:11 +03:00
Jakob Rath
e31926d132 var_queue display 2022-08-01 18:37:11 +03:00
Jakob Rath
6a929f91c8 scoped_ptr_vector usability 2022-08-01 18:37:11 +03:00
Jakob Rath
d2fe174320 Add SASSERT_EQ and VERIFY_EQ 2022-08-01 18:37:11 +03:00
Jakob Rath
79ee543d25 Move tbv to util 2022-08-01 18:37:11 +03:00