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

14495 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b2bfb1faea fix nla_monotone lemmas again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 17:26:54 -07:00
Murphy Berzish
3147be66fe
z3str3: fix up regex heuristics (#4342) 
fixes #4308, partially fixes #4309
 2020-05-16 17:17:32 -07:00
Nikolaj Bjorner
bfb38451d1 add unicode encoding back 2020-05-16 17:11:47 -07:00
Nikolaj Bjorner
cd64967706 fix #4317 2020-05-16 17:11:47 -07:00
Lev Nachmanson
aaf05f18ab fix a bug in an simplifying interval expressions with terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-16 15:19:32 -07:00
Nikolaj Bjorner
363690791a update TBD 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 14:34:39 -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
21c4d451d8 parse RegLan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 14:26:53 -07:00
Lev Nachmanson
d3c00ca2c3 change mode to executable to some py files 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-16 14:12:16 -07:00
Nikolaj Bjorner
4753d93bb7 add some of the SMTLIB2.6 conventions and features to strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 14:00:02 -07:00
Nikolaj Bjorner
1ab2ad07be outline of unicode parsing #4333 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 13:36:43 -07:00
Nikolaj Bjorner
937afbf95b draft rewrite 2020-05-16 12:43:26 -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
Nikolaj Bjorner
a3f56f0d95 revert 'fix' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 12:43:26 -07:00
Nuno Lopes
e6ee58b628 restore exec bit on a few more script; trying to unbreak buildbots 2020-05-16 20:15:10 +01:00
Nuno Lopes
0313cf6d4c restore exec bit on configure & scripts/*.sh 2020-05-16 20:07:36 +01:00
Nikolaj Bjorner
2822922d36 fix regression with mainintaing signs for monotonicity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 11:17:40 -07:00
Nikolaj Bjorner
d352c61e01 fix regression with mainintaing signs for monotonicity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 11:17:39 -07:00
Lev Nachmanson
cd833e892f avoid iterations on std::unordered_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-16 08:55:15 -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
Nikolaj Bjorner
ccda9d56d7 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 15:57:38 -07:00
Nikolaj Bjorner
90f5595067 fix order lemma bug see 30ce6f20f2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 15:38:55 -07:00
Nikolaj Bjorner
31a96b3afa review of monotonicity lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 15:16:46 -07:00
Lev Nachmanson
30ce6f20f2 move nla stats to nla_core 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 13:03:18 -07: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
Lev Nachmanson
08940cff8f comment out the call to nra_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 11:26:40 -07:00
Nikolaj Bjorner
9c9fe712ad disable nra in master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 10:36:53 -07:00
Nikolaj Bjorner
7e4b232ac4 fix comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 10:36:21 -07:00
Lev Nachmanson
6a4062809d
Nra add term (#4331) 
* n

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

* do not create assumptions

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

* disable nra_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 10:35:42 -07:00
Nikolaj Bjorner
0c91109577 order lemmas on also rationals 2020-05-15 10:12:06 -07:00
Nikolaj Bjorner
146fd77e0f pretty print 2020-05-15 10:12:06 -07:00
Nikolaj Bjorner
c4204d3365 fix #4330 2020-05-15 10:12:06 -07:00
Alexey Vishnyakov
6d96f96cc3
Fix single threaded azure pipeline (#4329) 2020-05-15 08:50:47 -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
Nikolaj Bjorner
73fa5995d4 fix #4316 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 19:35:17 -07:00
Nikolaj Bjorner
4e51633e6f adding monomial bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 18:45:47 -07:00
Lev Nachmanson
bdecbe4ed7 remove a duplicate method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-13 15:38:20 -07:00
Nikolaj Bjorner
fff1426556 remove unreferenced label 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:54:47 -07: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
Nikolaj Bjorner
16aec328f1 add comments, fix mixup between lower/upper 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:42:50 -07:00
Nikolaj Bjorner
33042268b5 bounds propagation functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:36:22 -07:00
Murphy Berzish
5e7806c4a4 z3str3: use rational in place of unsigned during model construction 2020-05-13 14:32:44 -04:00
Nikolaj Bjorner
bda29ca26a outline for monomial bound propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 10:37:46 -07:00
Murphy Berzish
3c606ea9b2 z3str3: disable compute_contains() and get_grounded_concats() checks 2020-05-13 11:53:26 -04:00
Nikolaj Bjorner
127ef59ce4 push explanation to where it is used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 19:55:07 -07:00