3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Commit graph

13911 commits

Author SHA1 Message Date
Nuno Lopes b7b8ed23fb remove support for decade old ubuntu 14. keep support for 16, 18, 20 LTS 2020-05-23 18:02:34 +01:00
Nuno Lopes 903725314c fix gcc 9/10 warnings 2020-05-23 16:39:09 +01:00
Nikolaj Bjorner d1d14111cb turn on Unicode parsing when they fit in 8 bits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-22 10:41:19 -07:00
Hari Govind V K b7d7ff38cb
bug fix. Handle unknown without model (#4443) 2020-05-22 10:12:42 -07:00
Nikolaj Bjorner 9eedd4ecd6 gate mk_bool_app by existence of regex
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-22 10:09:16 -07:00
Nikolaj Bjorner 82fb7573d7 more rewrites for emptiness
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-22 09:56:21 -07:00
Margus Veanes 5d6be3f17f
adding regex simplification rewriter (#4440) 2020-05-22 09:55:29 -07:00
Nikolaj Bjorner 18bb90f93d fix #4426
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-21 21:27:26 -07:00
Nikolaj Bjorner 9da0b61d30 na 2020-05-21 21:04:48 -07:00
Nikolaj Bjorner 131dfc2101 na 2020-05-21 21:04:48 -07:00
Nikolaj Bjorner ce1fd26b19 #4424 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
Hari Govind V K ed92b8437c
fix #4054 (#4277)
* flag when quantified lemmas are added to smt_context

* When solver returns unknown but cannot create child, return unknown

* handle unknowns when qlemmas and weak_abs are turned on
2020-05-21 09:58:09 -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
Anton Kochkov 7e84a48069
Add pkg-config file (#4368)
* Add pkg-config file

* Copy z3.cmake.in to the Docker for CI
2020-05-21 09:10:41 -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 6381cfdc05 remove old functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 16:34:21 -07:00
Nikolaj Bjorner 209f6a9e2e regression free behavior
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 16:21:19 -07:00
Nikolaj Bjorner 287bccde30 disable new incomplete functionality for master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 15:56:57 -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 7756e2c6d5
in progress (#4386)
* initial work on replacing str in regex check

* finish rewriter for empty string in regex

* remove unnecessary argument in mk_regexp_contains_emptystr; initial template for eval_regexp_derivative

* progress on string in regexp general check using derivatives

* added recursive nullable and derivative funcitons, partially working

* remove tests from z3test

* fix rewriting infinite loop and some failing simplify checks

* several fixes addressing comments for z3 main branch PR #4386

* redo derivative to return an expr_ref, and null on failure

Co-authored-by: calebstanford-msr <t-casta@microsoft.com>
2020-05-19 15:55:19 -07:00
Nikolaj Bjorner b3366bae5a remove test-examples from MacOS build, re-add maxsat example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 13:52:44 -07:00
Nikolaj Bjorner fca44ff3f2 fix #4394
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 13:40:03 -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
Alexey Vishnyakov 3b0c40044f
SINGLE_THREAD: do not use pthread if possible (#4382) 2020-05-19 09:45:41 -07:00
Nikolaj Bjorner 5fe0eeda63 disable regressions in ST mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-19 09:37:06 -07:00
Nuno Lopes 232f1b5fbe fix a gcc 10 warning 2020-05-19 14:44:14 +01:00
Nikolaj Bjorner 0f8f886389 use single return pattern
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 20:27:50 -07:00
Nikolaj Bjorner bc03ffb800 typing error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 20:19:33 -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 e525543bd0 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:47:13 -07:00
Nikolaj Bjorner d26ef08c69 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:41:37 -07:00
Nikolaj Bjorner ff34d84b35 ranges are never nullable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:41:04 -07:00
Nikolaj Bjorner 6e55880601 constant folding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:38:21 -07:00
Nikolaj Bjorner 5bbf05c93c kleene
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-18 19:35:31 -07:00
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