3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Commit graph

13871 commits

Author SHA1 Message Date
Nikolaj Bjorner fcd2bc605c try to make template parsing work
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:17:36 -07:00
Nikolaj Bjorner 323a752bbf disable maxsat. for a mysterious reason it started failing on a single macos build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:16:32 -07:00
Nikolaj Bjorner 55225824ee remove std::mutex, replace by util/mutex.h in api_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:15:11 -07:00
Nikolaj Bjorner 10edee48f3 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:11:59 -07:00
Nikolaj Bjorner 9d6c870e97 remove case with hi = 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:11:35 -07:00
Nikolaj Bjorner f8d328b1fb add nullable, get-head-tail with Caleb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:10:00 -07:00
Nikolaj Bjorner c40c4313a4 parens
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 18:07:40 -07:00
Nikolaj Bjorner 5844964d95 rename temporary macro
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 17:17:51 -07:00
Nikolaj Bjorner 8e8e9be25f st
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 16:49:43 -07:00
Nikolaj Bjorner c2a59a89af thanks to https://github.com/Z3Prover/z3/pull/4382#issuecomment-630468832_
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 15:32:23 -07:00
Nikolaj Bjorner 801eb47fae remove thread dependency in symbol.cpp on single thread #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 15:16:08 -07:00
Nikolaj Bjorner ff10afd226 remove thread dependency in symbol.cpp on single thread #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 15:11:24 -07:00
Nikolaj Bjorner f538ee3fe2 another module level ifdef for #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 15:07:39 -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 d603bd7e3b disable selected functionality in SINGLE_THREAD mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 14:47:33 -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
Nikolaj Bjorner 78a4717c06 fix #4359 and regression to #3270 2020-05-18 12:41:42 -07:00
Murphy Berzish 1c760b04cf
re.range with non-unit arguments is the empty language (#4360) 2020-05-17 19:08:50 -07:00
Murphy Berzish 152d6338f8
fix hex digit radix in unicode escape (#4356) 2020-05-17 19:07:51 -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 30f17b1509 fix #4355
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-17 12:28:30 -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
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