mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity
6331 commits 23 branches 48 tags 157 MiB
Commit graph

6331 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 7cb0237ab2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-05 10:59:58 -04:00
Nikolaj Bjorner 7e1fae418a fix #1005, disable expansion of regular expression range to union as it degrades performance significantly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-05 10:59:47 -04:00
Christoph M. Wintersteiger 79dcf03a42 Enabled C++11 in GCC and Clang 2017-05-05 15:01:10 +01:00
Christoph M. Wintersteiger 00ce3f8172 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-05 14:22:49 +01:00
Christoph M. Wintersteiger 0ebce66c57 Fixed bug with .NET keyfile path containing spaces. Fixes #1003. 2017-05-05 14:22:40 +01:00
Nikolaj Bjorner 9499fa62ac Merge pull request #1004 from delcypher/cmake_doxygen_fixes 
[CMake] Doxygen fixes
 2017-05-04 12:08:10 -07:00
Dan Liew 1db07f1189 [CMake] Remove BYPRODUCTS declaration for api_docs target. 
This breaks the `clean` rule when using Ninja as the CMake
generator. Unfortunately this means `clean` doesn't try to
remove the generated documentation anymore when using Ninja.
 2017-05-04 15:29:47 +01:00
Dan Liew 6261a5c27b Fix bug in mk_api_doc.py where the Z3 python package path would be 
checked when building the Z3 python package documentation was disabled.
 2017-05-04 15:28:20 +01:00
Nikolaj Bjorner a9d6ef68f0 Merge pull request #1002 from mtrberzi/obj_pair_set 
add iterator accessors to obj_pair_set
 2017-05-03 16:18:05 -07:00
Murphy Berzish ede6d7bb2b add iterator accessors to obj_pair_set 2017-05-03 14:55:22 -04:00
Nikolaj Bjorner 1177be6391 add common utility to set up seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 20:52:39 -07:00
Nikolaj Bjorner 52dfdedb9b Merge pull request #1000 from mtrberzi/theory_str-smt-setup 
smt_setup for strings/sequences
 2017-05-02 20:44:23 -07:00
Nikolaj Bjorner cc7a176c89 update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:32:03 -07:00
Nikolaj Bjorner eeb79e1c3c update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:30:54 -07:00
Nikolaj Bjorner 561a4331a8 add back use of all variables for tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 16:36:05 -07:00
Nikolaj Bjorner cec6ced457 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-02 15:57:41 -07:00
Nikolaj Bjorner 21cda27f5e fix quadratic behavior of extract_assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 15:57:31 -07:00
Nikolaj Bjorner 5b0286001b Merge pull request #999 from mtrberzi/theory-aware-branching 
Theory-aware branching heuristic
 2017-05-02 15:32:37 -07:00
Murphy Berzish 92755b0185 smt_setup framework, all hooks to theory_str are redirected to theory_seq 2017-05-02 17:16:35 -04:00
Nikolaj Bjorner ed0b2be618 fix bug in tracking levels of variables: levels are not cleared, only truth assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 14:10:07 -07:00
Murphy Berzish 15cb2d7dba cleanup 2017-05-02 14:08:48 -04:00
Murphy Berzish a8d069ba46 refactor: add asserts, use case split strategy param 2017-05-02 13:06:08 -04:00
Murphy Berzish 5b4792955d theory-aware branching heuristic 2017-05-02 10:43:40 -04:00
Murphy Berzish 6cd1f877b8 params for theory aware branching 2017-05-02 10:39:32 -04:00
Nikolaj Bjorner 48e37b0e16 pass qhead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 16:54:22 -07:00
Nikolaj Bjorner 8ba78081ec fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 16:41:17 -07:00
Nikolaj Bjorner 61e0fc9099 Merge pull request #995 from mtrberzi/theory-case-split 
Theory case split heuristic (for theory_str)
 2017-05-01 15:27:45 -07:00
Murphy Berzish 16a5e944d7 use reference for case split sets 2017-05-01 18:25:54 -04:00
Nikolaj Bjorner f9105edb14 revert to native chunker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:52 -07:00
Murphy Berzish b86d472eaf simplify theory case split handling 2017-05-01 18:22:49 -04:00
Nikolaj Bjorner d14f2af5ae deal with subtraction that manages to sneak in. Issue #996 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:06 -07:00
Murphy Berzish 3bce61e0d4 fix warning 2017-05-01 10:43:33 -04:00
Murphy Berzish 2f56d128b0 add theory case split support to smt_context 2017-05-01 10:34:43 -04:00
Murphy Berzish f655e1976e add params for theory case split 2017-05-01 10:18:38 -04:00
Nikolaj Bjorner aceee3fac8 renmae to opt_stream_buffer to avoid clash with dimacs stream buffer. #994 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 12:54:29 -07:00
Nikolaj Bjorner 0693a413b6 augment #955 to handle hyphen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 12:50:56 -07:00
Nikolaj Bjorner 86f3526110 update get-value to also respect parameter model_index, #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 11:48:06 -07:00
Nikolaj Bjorner d6e2e1f28f Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 11:28:26 -07:00
Nikolaj Bjorner aff02ca905 include 'stopwatch.h' to avoid ODR warnings, #994 2017-04-30 11:28:11 -07:00
Nikolaj Bjorner bd1b930d7a swap argument order of chunk with file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 11:00:03 -07:00
Nikolaj Bjorner 5fcbf55216 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 10:23:05 -07:00
Nikolaj Bjorner 2c208e1d10 Sat update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 10:23:00 -07:00
Nikolaj Bjorner 4468816d32 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 19:00:15 -07:00
Nikolaj Bjorner b3f720c2bf fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:58:34 -07:00
Nikolaj Bjorner 3152833893 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:55:47 -07:00
Nikolaj Bjorner 944dfbc6ef Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-29 17:39:20 -07:00
Nikolaj Bjorner fa868e058e fix bound bug #991 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 17:39:02 -07:00
Nikolaj Bjorner d3f9e4874a Merge pull request #993 from delcypher/cmake_fix_setting_flags 
[CMake] Make MSVC flags much more similar to python/Makefile build system.
 2017-04-29 11:35:37 -07:00
Dan Liew 6e07d6dd2d [CMake] Override CMake's default flags for GCC/Clang as we were doing 
before 4cc2b292c0.

It's useful to be able to control the defaults and CMake's internal
logic for GCC/Clang is simple enough that doing this makes sense.

It would be nice to do the same for MSVC but CMake's internal
logic is more complicated so for now it's better that we just use
CMake's default.
 2017-04-29 17:45:02 +01:00
Dan Liew 2a919cf16e [CMake] Duplicate the remaining linker flags from the old build system. 2017-04-29 16:22:46 +01:00