mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
19294 commits 49 branches 53 tags 182 MiB
Commit graph

4330 commits

Author SHA1 Message Date
Lev Nachmanson
52fdb4d291 fix issue https://github.com/Z3Prover/z3/issues/4438 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-26 12:44:47 -07:00
Lev Nachmanson
caa384f6c9 make m_inf_set private and cosmetic improvements in nla patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-26 12:44:47 -07:00
Nuno Lopes
d8cea7c8d5 fix a few warnings & simplify debug.h header 2020-05-26 13:49:13 +01:00
Nikolaj Bjorner
a97bc65af4 hoist co-factors eagerly without adding axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-25 15:10:45 -07:00
Nikolaj Bjorner
4e01d5b5c1 tune axioms for derivatives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-25 14:11:59 -07:00
Lev Nachmanson
97b480ded3
Expl (#4462) 
* cleaner API for explanation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove an unnecessery check

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* expl

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-24 17:06:39 -07:00
Nikolaj Bjorner
d6ad371934 avoid div/mod axioms on 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-23 16:37:40 -07:00
Nikolaj Bjorner
24df35a83e guard derivative code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-23 16:02:10 -07:00
Nikolaj Bjorner
eb3f20832e initial pass at using derivatives in regex unfolding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-23 11:53:07 -07:00
Nuno Lopes
903725314c fix gcc 9/10 warnings 2020-05-23 16:39:09 +01:00
Nikolaj Bjorner
131dfc2101 na 2020-05-21 21:04:48 -07:00
Nikolaj Bjorner
698d300511 na 2020-05-21 21:04:48 -07:00
Nikolaj Bjorner
5307797c32 #4424 2020-05-21 21:04:48 -07:00
Nikolaj Bjorner
4c9517260c #4427 2020-05-21 21:04:48 -07:00
Lev Nachmanson
bfd2407e0f
Debug (#4415) 
* fix it explanation.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix explanation.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add options to run bound propagation on monomials etc.

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-21 09:55:01 -07:00
Nikolaj Bjorner
1729232254 fix #4414 2020-05-20 14:28:41 -07:00
Nikolaj Bjorner
f2d3160181 try different field order for Mac build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-20 01:06:56 -07:00
Nikolaj Bjorner
1dcbde4ecb fix #4401 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 19:55:39 -07:00
Nikolaj Bjorner
1ce63363ba fix #4400 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 15:56:08 -07:00
Nikolaj Bjorner
72d129eb75 #4396 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 13:13:09 -07:00
Lev Nachmanson
af2f74c05f
smarter explanation.h (#4385) 
* smarter explanation.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* clean explanation API

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* suppress warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* disable the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-19 12:38:44 -07:00
Nikolaj Bjorner
7f22eb594e don't pretend to handle new operators #4387 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 20:04:43 -07:00
Nikolaj Bjorner
c40c4313a4 parens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 18:07:40 -07:00
Nikolaj Bjorner
fd57faee7c another module level ifdef for #4382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 15:03:58 -07:00
Nikolaj Bjorner
c8c02060ee another module level ifdef for #4382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 15:01:27 -07:00
Nikolaj Bjorner
1072bf1536 deal with unsigned / bignum #4361 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 14:42:06 -07:00
Murphy Berzish
1c760b04cf
re.range with non-unit arguments is the empty language (#4360) 2020-05-17 19:08:50 -07:00
Nikolaj Bjorner
1def58bc9f optional unicode mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-17 19:06:34 -07:00
Nikolaj Bjorner
951c769fc9 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-17 12:20:33 -07:00
Nikolaj Bjorner
1bfc12d6e6 initial stab at independent unicode module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-17 11:42:39 -07:00
Nikolaj Bjorner
fc8dfe3e40 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-17 05:35:32 -07:00
Nikolaj Bjorner
34cc60410f additional str/re operators, remove encoding option from zstring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-17 05:08:36 -07:00
Murphy Berzish
3147be66fe
z3str3: fix up regex heuristics (#4342) 
fixes #4308, partially fixes #4309
 2020-05-16 17:17:32 -07:00
Murphy Berzish
6f0a367357
add SMTLIB2.6 names for QF_SLIA and string-int conversion operators (#4341) 2020-05-16 14:31:47 -07:00
Nikolaj Bjorner
843b6cf149 fix #4336 - check return values of eval, they can be null due to cancelation 2020-05-16 12:43:26 -07:00
Murphy Berzish
ce07138008
Merge pull request #4325 from mtrberzi/issue4322 
ignore true/false/null literals during theory case split propagation
 2020-05-15 20:42:33 -05:00
Murphy Berzish
fcbcad6c10
Merge pull request #4320 from mtrberzi/mc-rational 
z3str3: use rational in place of unsigned during model construction
 2020-05-15 20:42:19 -05:00
Murphy Berzish
ba40b36176
Merge pull request #4319 from mtrberzi/disable-get-grounded-concats 
Z3str3: disable compute_contains() and get_grounded_concats() checks
 2020-05-15 20:42:07 -05:00
Murphy Berzish
8b4929ccda
Merge pull request #4313 from mtrberzi/issue2111 
Z3str3: address crashes and timeouts related to int.to.str
 2020-05-15 20:41:51 -05:00
Lev Nachmanson
01279582ff move nla stats to nla_core 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 12:58:34 -07:00
Lev Nachmanson
82fd2a062d make calling nra from nla optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 12:16:40 -07:00
Nikolaj Bjorner
c4204d3365 fix #4330 2020-05-15 10:12:06 -07:00
Nikolaj Bjorner
b43ed70874 extend monomial bounds to handle powers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-14 19:13:17 -07:00
Murphy Berzish
ae18150d87 ignore true/false/null literals during theory case split propagation 2020-05-14 12:51:20 -04:00
Lev Nachmanson
6b28973799
nla review (#4321) 
* simplify the nla_solver interface

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more simplifications

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* init m_use_nra_model

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* work on NSB comments

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* work on NSB comments

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:52:42 -07:00
Murphy Berzish
5e7806c4a4 z3str3: use rational in place of unsigned during model construction 2020-05-13 14:32:44 -04:00
Murphy Berzish
3c606ea9b2 z3str3: disable compute_contains() and get_grounded_concats() checks 2020-05-13 11:53:26 -04:00
Lev Nachmanson
b2dc21b107
simplify the nla_solver interface (#4312) 
* simplify the nla_solver interface

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more simplifications

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* init m_use_nra_model

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 19:34:03 -07:00
Murphy Berzish
51beeec92f z3str3: heuristics for predicates over int-to-string terms 2020-05-12 21:35:24 -04:00
Nikolaj Bjorner
7a6c66a085 add stubs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 17:38:16 -07:00